Statistical Automaton for Verifying Temporal Properties and Computing Information on Traces
Keywords:
Statistical Büchi Automaton, Information Computation, Runtime Verification, Dynamic analysis, Linear Temporal LogicAbstract
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.References
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. http://dx.doi.org/10.1145/2000799.2000800
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. http://dx.doi.org/10.1007/978-1-4613-8928-6_23
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. http://dx.doi.org/10.1007/10722468_19
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. http://dx.doi.org/10.1109/ISSREW.2012.100
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. http://dx.doi.org/10.1007/3-540-44585-4_6
D. Giannakopoulou and K. Havelund. Automata-based verification of temporal properties on running programs. In Automated Software Engineering, 2001. http://dx.doi.org/10.1109/ase.2001.989841
K. Havelund and G. Rosu (2001), Monitoring programs using rewriting. In Automated Software Engineering, 135 - 143. http://dx.doi.org/10.1109/ase.2001.989799
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. http://dx.doi.org/10.1515/9781400882618-002
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). http://dx.doi.org/10.1016/j.jlap.2008.08.004
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. http://dx.doi.org/10.1007/s10009-011-0198-6
A. Pnueli, A. Zaks (2006), Psl model checking and run-time verification via testers. In FM 2006: Formal Methods, vol. 4085 of LNCS. Springer. http://dx.doi.org/10.1007/11813040_38
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. http://dx.doi.org/10.1007/978-3-642-05089-3_34
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. http://dx.doi.org/10.1016/j.entcs.2006.02.007
Published
Issue
Section
License
ONLINE OPEN ACCES: Acces to full text of each article and each issue are allowed for free in respect of Attribution-NonCommercial 4.0 International (CC BY-NC 4.0.
You are free to:
-Share: copy and redistribute the material in any medium or format;
-Adapt: remix, transform, and build upon the material.
The licensor cannot revoke these freedoms as long as you follow the license terms.
DISCLAIMER: The author(s) of each article appearing in International Journal of Computers Communications & Control is/are solely responsible for the content thereof; the publication of an article shall not constitute or be deemed to constitute any representation by the Editors or Agora University Press that the data presented therein are original, correct or sufficient to support the conclusions reached or that the experiment design or methodology is adequate.
