A formal approach for safe controllers analysis

Abstract

Formal verification of real-time systems software is a complex and hard task, for several reasons. There are multiple works developed in the domain of formal verification of real-time systems behavior by model-checking, and some software tools were developed for this purpose. One of the most complex problems to be solved in the analysis of real-time controllers is the conversion of controllers programming languages in formal languages, for instance finite timed automata, in order to be used as inputs of the existing model-checkers. If the methodology of programming is well developed and known, this task can be improved in order to improve safety and reliability of the obtained controllers. Moreover, most real-time systems (especially embedded systems that we intend to study) are programmed in C language. This paper aims to establish the methodology of creating C code programs, from SFC specification formalism, taking into account the formal verification of desired properties for the system behavior, using the Model-Checking technique and the model-checker UPPAAL.