Automatic Translation from a Subset of C Language to XML supported by UPPAAL

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