Abstract:
C language is commonly used to develop embedded systems that are often
being used in domains that have critical safety requirements, like transportation and medicine. These systems require rigorous analysis to ensure safety
and proper functioning of the system due to their safety critical nature. The
commonly used testing and simulation techniques don’t have the ability to
ensure completeness and soundness of the system. Formal verification has
been advocated as the sole analysis technique that allows a rigorous and
sound analysis. However, it involves the development of the formal model
of the given code, which is not a very straightforward task. Modeling lines
and lines of code to formal models is a very tiresome process which is also
very time consuming and owing to the ever changing nature of code it can
become even more troublesome. The Quality assurance teams tend to avoid
formal verification techniques due to the raised level of difficulty. This thesis propose a system that can aid the Quality assurance teams in formally
verifying codes by automatically generating the formal model acceptable by
UPPAAL model checker, thus reducing the level of difficulty, time consumed
and effort applied to formally model a given code.
The proposed approach accepts a C code file, which conforms to a predefined
subset, as an input and returns the corresponding Extensible Markup Lan
guage (XML) file that is acceptable to UPPAAL. The main steps involved
in this process include parsing the C code and creating a Directed graph of
the code, where the graph contains all the data regarding the states of the
corresponding automata and its transition conditions. This graph is parsed
again and translated to XML acceptable the model checker (UPPAAL). For
illustration, the verification of a simple automatic cooling system is presented
in this thesis
