Computational Conversion via Translation Rules for Transforming C++ Code Into UPPAAL’s Automata

Abstract

Formal methods help in quantifying the functional and nonfunctional requirements that are later used in the verification process for safety assurance in real-time systems. System formalism is a crucial step in terms of exploring system's behavior and listing the non-functional requirements. In the context of real-time systems, the non-functional requirements refer to the verification properties of the system. Formalism in software development life cycle refines every process, starting from the formalization of system's requirements, analysis of system's behavior and exploring its properties, implementation of the problem's solution under consideration, and verification of safety critical properties. Rule-based expert system helps in inferring unknown on the basis of some known input, that is, knowledge and rule set. Knowledge is comprised of something known by an individual called an expert of that domain. It requires an expert skill set in order to model and verify some system in model checkers like UPPAAL. This research contribution has explored a variation of traffic light system's case study, modeled the system in UPPAAL model checker, and later verified the safety critical properties of the generated system like safety, liveness, fairness, reachability, and deadlock freeness to cross-check the validity of transformation rule set. This research is focused on providing the rule-based expert system for inferring timed automata (input of UPPAAL model checker) on the basis of fact cum input, that is, C++ code. Structural facts are used along with the transformation rule set to get the timed automata that verify safety properties of selected case studies-multiple variations of a traffic light system.

Keywords

• UPPAAL model checker
• verification properties
• automaton
• formalism
• rule-based expert system
• knowledge base