Abstract
PeaCE(Ptolemy extension as a Codesign Environment) was developed for the hardware and software codesign framework which allows us to express both data flow and control flow. The fFSM is a model for describing the control flow aspects in PeaCE, but it has difficulties in verifying their specifications due to lack of their formality. Thus we propose the formal semantics of the model based on its execution steps. To verify an fFSM model, it is translated into SMV input language with properties to be checked, automatically. As a result, some important bugs such as race condition, ambiguous transition, and circular transition can be formally detected in the model.
This work was supported in part by IT Leading R&D Support Project funded by Ministry of Information and Communication, Republic of Korea.
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., Ha, S.: Static Analysis and Automatic Code Synthesis of flexible FSM Model. In: ASP-DAC 2005, January 18–21 (2005)
iLogix: http://www.ilogix.com/
Mikk, E., Lakhnech, Y., Siegel, M.: Hierarchical automata as model for statecharts. In: Shyamasundar, R.K. (ed.) ASIAN 1997. LNCS, vol. 1345, pp. 181–196. Springer, Heidelberg (1997)
Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering Methodology 5(4) (October 1996)
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. In: FMSD, pp. 5–23 (2001)
Kim, D.: System-Level Specification and Cosimulation for Multimedia Embedded Systems, Ph.D. Dissertation, Computer Science Department, Seoul National University (2004)
Lind-Nielsen, J.B.: Verification of Large State/Event Systems, Ph.D. Dissertation, Department of Information Technology, Technical University of Denmark (2000)
Chan, W.: Symbolic Model checking for Large software Specification. Dissertation, Computer Science and Engineering at University of Washington, pp. 13–32 (1999)
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
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Park, S., Kwon, G., Ha, S. (2005). Formalization of fFSM Model and Its Verification. In: Yang, L.T., Zhou, X., Zhao, W., Wu, Z., Zhu, Y., Lin, M. (eds) Embedded Software and Systems. ICESS 2005. Lecture Notes in Computer Science, vol 3820. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11599555_35
Download citation
DOI: https://doi.org/10.1007/11599555_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30881-2
Online ISBN: 978-3-540-32297-9
eBook Packages: Computer ScienceComputer Science (R0)