Automation of Software Modeling and Verification

Abstract

Exhaustively exploring all states of the system and to do extensive system verification is a
crucial task in real-time systems. Consequently, model checking techniques result in more
precise and accurate analysis than that of numerical methods and simulation for verification
and analysis. Domain specific abstraction techniques are used in model checking to get the
exhaustive state space of the system to reveal all possible behaviors of the system to be
modeled. Despite an excellent potential, model checking techniques are not extensively used in
the real-time systems. Lack of technical knowledge related to temporal logics and model
checker usage is the main reason for not using it. Software Modeling and Verification in Real
Time Systems is a safety critical task which requires efficient automation to achieve an errorfree
state of the system. Efficient exhaustive testing of safety critical systems is not possible
through manual techniques. Standard practice is to compose the model of the system's source
code for verifying the system's behavior and doing it manually, which generates an open area of
errors and biases. This research provides the transformation rule set for automating C++ code
in UPPAAL xml file and results are compared with the related researches published in NASA
Symposium on Formal Methods.