000			04412nam a22001697a 4500
003			NUST
082			_a005.1,RAH
100			_aRahim, Muhammad Abdul Basit Ur _9124480
245			_aModeling and Verification of Real Time and Hybrid System / _cMuhammad Abdul Basit Ur Rahim
260			_aRawalpindi, _bMCS (NUST), _cSeptember 2017
300			_axxii, 144 p
505			_aThe graphical modeling languages (UML and SysML) play an important role in designing the system engineering applications. In the field of software and system engineering, these languages are considered as the benchmark for modeling industrial applications. Such applications are constitute a large number of components that communicate with one another. A lot of time and efforts are required to 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 challenges in 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 be used to model the 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 has been extended for behavioral diagrams. Mapping rules have been proposed, implemented on case studies, and validating results using model checking tool. The modeling and verification of such applications are performed in the earlier design 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 translates the 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.
650			_aPhD Computer Software Engineering Thesis _9132801
651			_aPhD CSE Thesis _9132802
700			_aSupervised by Dr. Fahim Arif _9132700
942			_2ddc _cTHE
999			_c615843 _d615843