A SYSTEMATIC APPROACH TO FORMAL VERIFICATION AND VALIDATION OF EMBEDDED SYSTEMS: ENHANCING RELIABILITY AND SAFETY

Abstract

This article addresses the problem of model-based early design verification of systems engineering applications expressed using System Modelling 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. My 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, it 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.