DefinePK

Abstract

Exhaustively exploring all states of the system and to do extensive system verification is acrucial task in real-time systems. Consequently, model checking techniques result in moreprecise and accurate analysis than that of numerical methods and simulation for verificationand analysis. Domain specific abstraction techniques are used in model checking to get theexhaustive state space of the system to reveal all possible behaviors of the system to bemodeled. Despite an excellent potential, model checking techniques are not extensively used inthe real-time systems. Lack of technical knowledge related to temporal logics and modelchecker usage is the main reason for not using it. Software Modeling and Verification in RealTime Systems is a safety critical task which requires efficient automation to achieve an errorfreestate of the system. Efficient exhaustive testing of safety critical systems is not possiblethrough manual techniques. Standard practice is to compose the model of the system's sourcecode for verifying the system's behavior and doing it manually, which generates an open area oferrors and biases. This research provides the transformation rule set for automating C++ codein UPPAAL xml file and results are compared with the related researches published in NASASymposium on Formal Methods.