Abstract
Verification is critical to the design of large and complex systems. SPIN is a well-known and extensively used verification tool. In this paper, we consider two tool chains, one existing, WSAT, and one introduced here, that support using SPIN to model check systems specified as Simulink Stateflow models. We present algorithms for doing the necessary translations and present empirical results that show the chain using tools introduced in this paper performs better than the one using the existing WSAT tool. We also show that these tools allow SPIN to be used for model checking nondeterministic Stateflow models in addition to deterministic ones.
Article PDF
Similar content being viewed by others
References
J. E. M. Clarke, O. Grumberg, Peled, and D. A., Model Checking. Cambridge, MA, USA: MIT Press, 1999.
K. Nermin, P. Christopher, H. Andrea, and K. Christian, “On design-time modelling and verification of safety-critical component-based systems,” International Journal of Networked and Distributed Computing (IJNDC), vol. 2–3, pp. 175–188, July2014.
H. Jun, W. Tao, G. Quan, and S. Gang, “Query integrity verification based-on mac chain in cloud storage,” International Journal of Networked and Distributed Computing (IJNDC), vol. 2–4, pp. 241–249, November 2014.
“Spin web site,”http://www.spinroot.com.
“Simulink@ documentation center (the mathworks, inc.),” http://www.mathworks.com/help/simulink/.
X. Fu, T. Bultan, and J. Su, “Wsat: A tool for formal analysis of web services.” in CAV, ser. Lecture Notes in Computer Science, vol. 3114. Springer, 2004, pp. 510–514.
“Simulink@ design verifier documentation center (the mathworks, inc.),” http://www.mathworks.com/help/sldv/.
F. Leitner, “Evaluation of the matlab simulink design verifier versus the model checker SPIN,” Bachelor Thesis, University of Konstanz, 2008.
“Extensible markup language (xml),” http://www.w3.org/XML/.
A. Brown, M. Fuchs, J. Robie, and P. Wadler, “Msl — a model for w3c xml schema,” in Proceedings of the 10th International Conference on World Wide Web, ser. WWW ‘01. New York, NY, USA: ACM, 2001, pp.191–200.
X. Fu, T. Bultan, and J. Su, “Model checking xml manipulating software,” in Proceedings of the 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis, ser. ISSTA ‘04. ACM, 2004, pp. 252–262.
——, “Analysis of interacting bpel web services,” in Proceedings of the 13th International Conference on World Wide Web, ser. WWW ‘04. ACM, 2004, pp. 621–630.
G. Holzmann, Spin Model Checker, the: Primer and Reference Manual, 1st ed. Addison-Wesley Professional, 2003.
A. Agrawal, G. Simon, and G. Karsai, “Semantic translation of simulink/stateflow models to hybridautomata using graph transformations,” Electron. Notes Theor. Comput. Sci., vol. 109, pp. 43–56, Dec. 2004.
A. Joshi and M. P. E. Heimdahl, “Model-based safety analysis of simulink models using scade design verifier,” in Proceedings of the 24th International Conference on Computer Safety, Reliability, and Security, ser. SAFECOMP’05. Springer-Verlag, 2005, pp. 122–135.
N. Rouquette, J. Dunphy, and M. S. Feather, “A flexible statechart-to-model-checker translator,” in IEEE, International Symposium on Requirements Engineering, 1999.
D. Latella, I. Majzik, and M. Massink, “Automatic verification of a behavioural subset of uml statechart diagrams using the spin model-checker,” Formal Aspects of Computing, vol. 11, no. 6, pp. 637–664, 1999.
K. Jiang and B. Jonsson, “Using spin to model check concurrent algorithm, using a translation from c to promela,” in Proc. 2nd Swedish Workshop on Multi-Core Computing. Department of Information Technology, Uppsala University, 2009, pp. 67–69.
P. de la Cámara, M. M. Gallardo, P. Merino, and D. Sanán, “Model checking software with welldefined apis: The socket case,” in Proceedings of the 10th International Workshop on Formal Methods for Industrial Critical Systems, ser. FMICS ‘05. ACM, 2005, pp. 17–26.
P. de la Cámara, M. Gallardo, and P. Merino, “Abstract matching for software model checking,” in Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30 - April 1, 2006, Proceedings, 2006, pp. 182–200.
“Ply (python lex-yacc),” http://www.dabeaz.com/ply/.
N. Scaife, C. Sofronis, P. Caspi, S. Tripakis, and F. Maraninchi, “Defining and translating a “safe” subset of simulink/stateflow into lustre,” in Proceedings of the 4th ACM International Conference on Embedded Software, ser. EMSOFT ‘04. New York, NY, USA: ACM, 2004, pp.259–268.
“Matlab central,” http://www.mathworks.com/matlabcentral/fileexchange/.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
This is an open access article distributed under the CC BY-NC 4.0 license (https://doi.org/creativecommons.org/licenses/by-nc/4.0/).
About this article
Cite this article
Yamada, C., Miller, D.M. Using SPIN to Check Simulink Stateflow Models. Int J Netw Distrib Comput 4, 193–202 (2016). https://doi.org/10.2991/ijndc.2016.4.3.6
Published:
Issue date:
DOI: https://doi.org/10.2991/ijndc.2016.4.3.6