Statistical Automaton For Verifying Temporal Properties And Computing Information On Traces

Verification is decisive for embedded software. The goal of this work is to verify temporal properties on industrial applications, with the help of formal dynamic analysis. The approach presented in this paper is composed of three steps: formalization of temporal properties using an adequate language, generation of execution traces from a given property and verification of this property on execution traces. This paper focuses on the verification step. Use of a new kind of Buchi automaton has been proposed to provide an efficient verification taking into account the industrial needs and constraints. A prototype has been developed and used to carry out experiments on different anonymous real industrial applications.