Abstract
An approach to integrating PVS executable specifications and Stateflow models is presented that uses web services to enable a seamless exchange of simulation events and data between PVS and Stateflow. Thus, it allows the wide range of applications developed in Stateflow to benefit from the rigor of PVS verification. The effectiveness of the approach is demonstrated on a medical device prototype, which consists of a user interface developed in PVS and a software controller implemented in Stateflow. Simulation on the prototype shows that simulation data produced is exchanged smoothly between in PVSio and Stateflow.
The rights of this work are transferred to the extent transferable according to title 17 U.S.C. 105.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
GPCA project, http://rtg.cis.upenn.edu/medical/gpca/gpca.html
Mathworks Simulink, http://www.mathworks.com/products/simulink
Mathworks Stateflow, http://www.mathworks.com/products/stateflow
Chen, C., Dong, J.S., Sun, J.: A formal framework for modeling and validating Simulink diagrams. Formal Aspects of Computing 21(5), 451–483 (2009)
Hamon, G., Rushby, J.: An operational semantics for Stateflow. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 229–243. Springer, Heidelberg (2004)
Masci, P., Ayoub, A., Curzon, P., Lee, I., Sokolsky, O., Thimbleby, H.: Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS. In: Bitsch, F., Guiochet, J., Kaâniche, M. (eds.) SAFECOMP. LNCS, vol. 8153, pp. 228–240. Springer, Heidelberg (2013)
Muñoz, C.: Rapid prototyping in PVS. Technical Report NIA Report No. 2003-03, NASA/CR-2003-212418, National Institute of Aerospace (2003)
Oladimeji, P., Masci, P., Curzon, P., Thimbleby, H.: PVSio-web: A tool for rapid prototyping device user interfaces in PVS. In: 5th International Workshop on Formal Methods for Interactive Systems, FMIS 2013 (2013), Tool and application examples available at http://www.pvsioweb.org
Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Roy, P., Shankar, N.: SimCheck: a contract type system for Simulink. Innovations in Systems and Software Engineering 7(2), 73–83 (2011)
Satpathy, M., Ramesh, S., Snook, C., Singh, N.K., Butler, M.: A mixed approach to rigorous development of control designs. In: IEEE Multi-Conference on Systems and Control (MSC 2013) (August 2013)
Scaife, N., Sofronis, C., Caspi, P., Tripakis, S., Maraninchi, F.: Defining and translating a safe subset of Simulink/Stateflow into Lustre. In: 4th ACM International Conference on Embedded Software. ACM (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Masci, P. et al. (2014). Combining PVSio with Stateflow. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_16
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)