Modeling and verification of real-time and hybrid system

Abstract

The graphical modeling languages (UML and SysML) play an important role in designing the system engineeringapplications. In the field of software and system engineering, these languages are considered as the benchmark for modeling industrial applications. Such applications are constitutea large number of components that communicate with oneanother. A lot of timeand effortsare requiredto model such complex and large scale applications. Furthermore, a reliable and accurate software has become a vital part of industrial growth. Producing a reliable application and proving its correctness are real challengesin the industry. An exhaustive review of methodologies for both modeling and verification of real-time and hybrid systems is presented with their limitations and shortcomings (chapter 2). There is no framework to formally specify the industrial requirement, generate an accurate graphical model, and map it to input language of model checking tools. The mapping among formal specification, graphical model, and inputer language of model checking tools are really challenging. To overcome the limitations of SysML, various improvements have been proposed for SysML diagrams (state machine diagram, activity diagram, and sequence diagram)for modeling of such systems. The designing of accurate graphical model is one of the challenges for system and software engineers. The formal specification can beused to modelthe system at abstract as well as lower level (the type of transaction, setting invariants, specifying delay, and constraints of states). It ensures the correctness and reliability of a system. Verifying the reliability and accuracy of such model is another challenge. The model transformation from formal semantics to graphical model; and from the graphical model to input language of model checking tools is really challenging as errors in transformation can result in incorrect model. The Duration Calculus(DC) based formal semantics for specification of requirements of real-time and hybrid systems has been proposed and mapped to SysML diagrams. DC based semantics hasbeen extended for behavioral diagrams. Mapping rules have been proposed, implemented on case studies, and validatingresults using model checking tool. The modeling and verification of such applications are performed in the earlierdesign phase to reduce the chance of failure of the product. The use of model checking tool makes this process easy and motivates the designer to perform analysis in the early design phase. Mapping has been proposed between formal specification and SysML diagrams, and also from SysML diagrams to checking tools for validation of requirements. The mapping procedure transforms accurate behavioral diagrams and a formal model for further verification. The proposed framework automates the whole process that makes it efficient to model and verify a system with less effort, cost, and time. The main objective of this thesis is to provide a practical and formal framework to model and analyze the SysML behavioral diagrams for real-time systems. The main contribution is the formal semantics for behavioral diagram for specification of systems requirement and their mapping with input language of model checking tools. The methodology verifies system’s liveness, deadlock-freeness, real-time, and non-real-time requirements. For implementation of the methodology, two applications softwares have been developed which are named as DC2SYSML and SD2DVE, to specify the requirements and translating them to behavioral diagram. These tools translatesthe specification in input languages of model checking tools for further verification of user requirements. The framework is implemented on embedded and real-time systems: security system, fuel filling station, man machine interface, chemical mixing plant, core flight system. Keywords: SysML, Verification and Validation, Real-time Systems, Hybrid System, Duration Calculus, Formal Semantics