Abstract
Keywords:
Model driven engineering, observers, timed automata, model-checking
Abstract:
Number of avionics systems are designed with formal specification languages, in order to get a clear, unambiguous and complete description of the system. The ATC module, designed with SDL, is a ground/onboard communication system. The SDL description of the system is so rigorous that automatic code generation is used in the system production process. Verifications based on tests are realized on the SDL model, through execution simulation. But SDL mathematical grounds can be exploited in formal verification too, in order to obtain ever earlier the highest level of confidence in the system.
The verification of real-time systems by modelchecking has been extensively studied in the last years, leading to important theoritical results. Tools have been applied to verification of real sized systems. The usual approach relies on a model, specifications or properties (requirements) and a model-checking technique to verify the properties on the model.
The common work between CS and ENSIETA, reported in this paper, is one of these works. It deals with industrial challenges related to the adoption of formal verification: theoritical remaining problems, tools integration, industrial constraints recognition. In the experiment reported here, we use the observer automata operational formalism for verifying dynamic properties of SDL models. Intuitively, the observers monitor the behaviour of the system looking for violation of properties (for example, safety property). They receive events generated by the system. The observers are executed in parallel with the model in a weak synchronous composition. To ease this composition and therefore support the properties verification of an SDL model, we took the option to translate it in a timed automata based on IF language from Verimag laboratory (observers are also specified in IF).
Our first experimentation on avionics case studies was an opportunity to evaluate this technique to verify some behavioural properties. We found that observers are adequate to specify the model behaviour. An appropriate methodology has still to be identified to help user to manipulate them in software design process.