A formal approach for aerospace systems control considering SFC specification and C programming language

Abstract

The C programming language is one of the most used in critical embedded real-time controllers applied at aerospace systems. Despite its potential, it is a very general language, with many maintenance problems and with a little or without graphical structure. The absence of formal verification techniques - even if it is possible to find some works associated to C programming language formal verification - is a fact. In this paper, it is proposed a methodology, that is divided in two main steps, and has, as main goal, to obtain safe C program code from a SFC specification: in first step some tools and techniques are used in order to assure the quality of the SFC specification and, on the second step, the goal is to translate (in a systematic way) the safe SFC specification to C code considering crucial aspects like taking into account aspects related with time specification.