Automation of software modeling and verification

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 comprises of something known by an individual called as an expert of that domain. It requires an expert skill set (that is, syntax and notations of the Model Checker and Verifier) in order to model and verify some system in Model Checkers like UPPAAL. This research consists of three parts. Firstly, it explores the variations (two case studies) of traffic light systems, models the systems in UPPAAL model checker and later verifies the safety critical properties of the generated systems like safety, live-ness, fairness, reachability and deadlock freeness. Experimental results are recorded for both systems with variety of search options to check the time efficiency. Second part of the research deals with the computational conversion via translation rules for transforming C++ code into UPPAAL’s automata and then cross-checked the validity of transformation rule set. This partfocuses 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 verifies safety properties of selected case studies–multiple variations of Traffic Light System. Last part of the research is related to the reverse engineering of the verification artifact back to the implemented code. Experimental results of the first contribution show thatverification time used by the UPPAAL model checker is worth mentioning for safety and deadlock freeness properties. Kernel responded all properties in no time, but the deadlock property took 0.01seconds. Elapsed time is the one that responds uniquely for all of the verified properties. Safety property took maximum elapsed time i.e., 0.02 seconds and with fractional change deadlock freeness property has 0.018 seconds of elapsed time used. Outcome of the second part that is, translation from C++ code to UPPAAL model is verified successfully. In the proposed methodology, the correctness of the transformation is crosschecked twice. Firstly, the informally mentioned behavior of C++ program is presented in the transformed automata and secondly the interaction among the functions via function call is preserved in UPPAAL’s automata via synchronization of channels. Third part is successfully reverse engineered from UPPAAL’s automata to C++ code.