Abstract
State explosion problem is a major huddle in model checking area. The model described in the temporal model checking is mainly control flow model. The fFSM is a model for describing the control flow aspects in PeaCE(Ptolemy extension as a Codesign Environment), which is a hardware/ software codesign environment to support complex embedded systems. fFSM, like a Statecharts, supports concurrency, hierarchy and global variables. But due to lack of their formality, we defined step semantics for this model and developed its verification tool in the previous work. In this paper, we present the model reduction technique based on dependency analysis to avoid the state explosion problem. As a result, the model, which couldn’t be verified before applying the technique, is verified.
This work was supported by grant No.(R01-2005-000-11120-0) from the Basic Research Program of the Korea Science & Engineering Foundation.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Kim, D.: System-Level Specification and Cosimulation for Multimedia Embedded Systems, Ph.D. Dissertation, Computer Science Department, Seoul National University (2004)
iLogix, http://www.ilogix.com/
Park, S., Kwon, G., Ha, S.: Formalization of fFSM model and its verification. In: Yang, L.T., Zhou, X.-s., Zhao, W., Wu, Z., Zhu, Y., Lin, M. (eds.) ICESS 2005. LNCS, vol. 3820, pp. 361–372. Springer, Heidelberg (2005)
Chan, W.: Symbolic Model checking for Large software Specification. Dissertation, Computer Science and Engineering at University of Washington (1999)
Lind-Nielsen, J.B.: Verification of Large State/Event Systems, Ph.D. Dissertation, Department of Information Technology, Technical University of Denmark (2000)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Lind-Nielsen, J., Andersen, H.R., Hulgaard, H., Behrmann, G., Kristoffersen, K.J., Larsen, K.G.: Verification of Large State/Event Systems Using Compositionality and Dependency Analysis. FMSD, 5–23 (2001)
Clarke, E.M., Heinle, W.: Modular translation of Statecharts to SMV. Technical Report CMU-CS-00-XXX, CMU School of Computer Science (August 2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Park, S., Kwon, G. (2006). Avoidance of State Explosion Using Dependency Analysis in Model Checking Control Flow Model. In: Gavrilova, M.L., et al. Computational Science and Its Applications - ICCSA 2006. ICCSA 2006. Lecture Notes in Computer Science, vol 3984. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11751649_99
Download citation
DOI: https://doi.org/10.1007/11751649_99
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34079-9
Online ISBN: 978-3-540-34080-5
eBook Packages: Computer ScienceComputer Science (R0)