Statistical Automaton for Verifying Temporal Properties and Computing Information on Traces


  • Antoine Ferlin Ifsttar, 20 rue Elisée reclus BP 70317, 59666 Villeneuve d'Ascq Cedex, France
  • Virginie Wiels Onéra/DTIM, 2 Avenue E. Belin BP74025,31055 Toulouse France
  • Philippe Bon Ifsttar, 20 rue Elisée reclus BP 70317, 59666 Villeneuve d'Ascq Cedex, France


Statistical Büchi Automaton, Information Computation, Runtime Verification, Dynamic analysis, Linear Temporal Logic


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 Büchi 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.


Runtime verification, 2001-2009.

H. Barringer, A. Goldberg, K. Havelund, and K. Sen (2004); Rule-based runtime verification. In B. Steffen and G. Levi, eds., Verification, Model Checking, and Abstract Interpretation, vol. 2937 of LNCS. Springer.

Howard Barringer, Allen Goldberg, Klaus Havelund, and Koushik Sen (2003); Eagle does space efficient ltl monitoring. Technical report, Nasa.

Andreas Bauer, Martin Leucker, and Christian Schallhart (2011); Runtime verification for ltl and tltl. ACM Trans. Softw. Eng. Methodol., 20(4):14:1-14:64.

J.Richard Büchi (1990); On a decision method in restricted second order arithmetic. In Saunders Mac Lane and Dirk Siefkes, editors, The Collected Works of J. Richard Büchi, Springer New York., 425-435.

Marcelo d'Amorim and Grigore Rosu (2005); Efficient monitoring of omega-languages. In CAV'05, 364-378.

Doron Drusinsky. The temporal rover and the atg rover. In K. Havelund, J. Penix, and W. Visser, editors, SPIN Model Checking and Software Verification, volume 1885 of Lecture Notes in Computer Science. Springer, 2000.

A. Ferlin and V. Wiels (2012); Combination of static and dynamic analyses for the certification of avionics software. In Software Reliability Engineering Workshops (ISSREW), 2012 IEEE 23rd International Symposium on, 331-336.

Antoine Ferlin (2013); Verification de propriétés temporelles sur des logiciels avioniques par analyse dynamique formelle. PhD thesis, Thèe de doctorat dirigée par Wiels, Virginie Sureté de logiciel et calcul de haute performance Toulouse, ISAE 2013.

P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV'01), vol. 2102 of LNCS. Springer, 2001.

D. Giannakopoulou and K. Havelund. Automata-based verification of temporal properties on running programs. In Automated Software Engineering, 2001.

K. Havelund and G. Rosu (2001), Monitoring programs using rewriting. In Automated Software Engineering, 135 - 143.

Klaus Havelund, Grigore Rosu (2002), A rewriting-based approach to trace analysis. Automated Software Engineering, 1-21.

S C Kleene (1956), Representation of events in nerve nets and finite automata. In In Automata Studies. Princeton University Press: Princeton.

Martin Leucker, Christian Schallhart (2009), A brief account of runtime verification. The Journal of Logic and Algebraic Programming, 78(5):293 - 303, The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS07).

Patrick O'Neil Meredith, Dongyun Jin, Dennis Griffith, Feng Chen, Grigore Rosu (2012), An overview of the mop runtime verification framework. International Journal on Software Tools for Technology Transfer, 14:249-289.

A. Pnueli, A. Zaks (2006), Psl model checking and run-time verification via testers. In FM 2006: Formal Methods, vol. 4085 of LNCS. Springer.

Jean Souyris, Virginie Wiels, David Delmas, Hervé Delseny (2009), Formal verification of avionics software products. In Formal Methods, Lecture Notes in Computer Science, 5850: 32-546.

Volker Stolz and Eric Bodden (2006), Temporal assertions using aspectJ, Proceedings of the Fifth Workshop on Runtime Verification (RV 2005), Electronic Notes in Theoretical Computer Science, 144(4):109 -124.



Most read articles by the same author(s)

Obs.: This plugin requires at least one statistics/report plugin to be enabled. If your statistics plugins provide more than one metric then please also select a main metric on the admin's site settings page and/or on the journal manager's settings pages.