A PVS-Simulink Integrated Environment for Model-Based Analysis of Cyber-Physical Systems
- 1 June 2018
- journal article
- research article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 44 (6), 512-533
- https://doi.org/10.1109/TSE.2017.2694423
Abstract
This paper presents a methodology, with supporting tool, for formal modeling and analysis of software components in cyber-physical systems. Using our approach, developers can integrate a simulation of logic-based specifications of software components and Simulink models of continuous processes. The integrated simulation is useful to validate the characteristics of discrete system components early in the development process. The same logic-based specifications can also be formally verified using the Prototype Verification System (PVS), to gain additional confidence that the software design complies with specific safety requirements. Modeling patterns are defined for generating the logic-based specifications from the more familiar automata-based formalism. The ultimate aim of this work is to facilitate the introduction of formal verification technologies in the software development process of cyber-physical systems, which typically requires the integrated use of different formalisms and tools. A case study from the medical domain is used to illustrate the approach. A PVS model of a pacemaker is interfaced with a Simulink model of the human heart. The overall cyber-physical system is co-simulated to validate design requirements through exploration of relevant test scenarios. Formal verification with the PVS theorem prover is demonstrated for the pacemaker model for specific safety aspects of the pacemaker design.Keywords
Funding Information
- North Portugal Regional Operational Programme (NORTE 2020)
- PORTUGAL 2020 Partnership Agreement, and through the European Regional Development Fund (ERDF) (NORTE-01-0145-FEDER-000016)
This publication has 42 references indexed in Scilit:
- Compositional verification of real-time systems using EcdarInternational Journal on Software Tools for Technology Transfer, 2012
- The overture initiative integrating tools for VDMACM SIGSOFT Software Engineering Notes, 2010
- Translating discrete-time simulink to lustreACM Transactions on Embedded Computing Systems, 2005
- System Modeling and Transformational Design Refinement in ForSyDeIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2004
- An Operational Semantics for StateflowLecture Notes in Computer Science, 2004
- Timed Automata: Semantics, Algorithms and ToolsLecture Notes in Computer Science, 2004
- A framework for comparing models of computationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 1998
- A set-theoretic model for real-time specification and reasoningPublished by Springer Science and Business Media LLC ,1998
- Symbolic Model Checking for Real-Time SystemsInformation and Computation, 1994
- A theory of timed automataTheoretical Computer Science, 1994