Formal Verification of Embedded Systems

Abstract

In this thesis, we address the issue of model-based early design verification of systems engineering applications expressed using System Modeling Language (SysML). This thesis describes the formal specification and verification approach for the early design verification of real time embedded systems. The main objective is to assess the design from its functional requirements to ensure the conformance of system requirements at early design phase. Our main contribution is a novel approach to model and verify the hybrid systems using SysML Block Diagram and hybrid automata. A formal verification technique “Model checking” has been used for the formal verification of SysML Block Diagram of real time embedded systems. The PRISM models Probabilistic Timed Automata (PTA) and Continuous Time Markov Chain (CTMC) are taken for the formalization and mapping of SysML Block Diagram. The user requirements are expressed as temporal logics Probabilistic Computational Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) for the properties verification against the PTA and CTMC model. Moreover, we define hybrid automata based formal specification to extend the behavior of SysML Block Diagram. The upgraded SysML Block Diagram has more ability to capture the discrete and continuous behavior of hybrid systems accurately. The SysML block diagram is verified with PRISM in order to show the correctness of system functionality. This thesis presents the effectiveness and validity of proposed approach with the help of four case studies. The discrete and continuous time constraints are considered in case studies along with the system functionality. The discrete and continuous time constraint helps the system and software engineer to verify the real time aspect of system along with its system functionality.