Advertisement

A Mechanized Semantic Framework for Real-Time Systems

  • Manuel Garnacho
  • Jean-Paul Bodeveix
  • Mamoun Filali-Amine
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8053)

Abstract

Concurrent systems consist of many components which may execute in parallel and are complex to design, to analyze, to verify, and to implement. The complexity increases if the systems have real-time constraints, which are very useful in avionic, spatial and other kind of embedded applications. In this paper we present a logical framework for defining and validating real-time formalisms as well as reasoning methods over them. For this purpose, we have implemented in the Coq proof assistant well known semantic domains for real-time systems based on labelled transitions systems and timed runs. We experiment our framework by considering the real-time CSP-based language fiacre, which has been defined as a pivot formalism for modeling languages (aadl, sdl, ...) used in the TOPCASED project. Thus, we define an extension to the formal semantic models mentioned above that facilitates the modeling of fine-grained time constraints of fiacre. Finally, we implement this extension in our framework and provide a proof method environment to deal with real-time system in order to achieve their formal certification.

Keywords

Transition System Semantic Model Linear Temporal Logic Label Transition System Semantic Interpretation 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abid, N., Zilio, S.D., Botlan, D.L.: A Verified Approach for Checking Real-Time Specification Patterns. In: Proceedings of VeCos (2012)Google Scholar
  2. 2.
    Arnold, A.: Finite Transition Systems - Semantics of Communicating Systems. Prentice Hall international series in computer science. Prentice Hall (1994)Google Scholar
  3. 3.
    Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Components in BIP. In: SEFM, pp. 3–12 (2006)Google Scholar
  4. 4.
    Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of Different Semantics for Time Petri Nets. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 293–307. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H.: Comparison of the Expressiveness of Timed Automata and Time Petri Nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 211–225. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Berthomieu, B., Bodeveix, J.-P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F.: Fiacre: an Intermediate Language for Model Verification in the Topcased Environment. In: ERTS 2008 (2008)Google Scholar
  7. 7.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development (Coq’Art: The Calculus of Inductive Constructions). Texts in Theoretical Computer Science. Springer (2004)Google Scholar
  8. 8.
    Bodeveix, J.-P., Filali, M., Garnacho, M., Spadotti, R., Yang, Z.: On the Mechanization of an AADL Subset. Science of Computer Programming: special issue on Architecture Design Language (submitted, 2013)Google Scholar
  9. 9.
    Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/Event-Based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  10. 10.
    Emerson, E.A., Halpern, J.Y.: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. In: STOC, pp. 169–180 (1982)Google Scholar
  11. 11.
    The FIACRE Specification Language for Real-Time Concurrent Systems, http://projects.laas.fr/fiacre/
  12. 12.
    Garnacho, M., Bodeveix, J.-P., Filali, M.: Mechanized Semantics of Concurrent Systems with Priorities. IRIT Research Report–2013-16–FR (2013), http://www.irit.fr/~Manuel.Garnacho/Publications/MechPrio.pdf
  13. 13.
    Geuvers, H., Koprowski, A., Synek, D., van der Weegen, E.: Automated Machine-Checked Hybrid System Safety Proofs. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 259–274. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  14. 14.
    Hale, R., Cardell-Oliver, R., Herbert, J.: An Embedding of Timed Transition Systems in HOL. FMSD 3(1/2), 151–174 (1993)zbMATHGoogle Scholar
  15. 15.
    Henzinger, T.A., Manna, Z., Pnueli, A.: Temporal Proof Methodologies for Real-time Systems. In: POPL, pp. 353–366 (1991)Google Scholar
  16. 16.
    Henzinger, T.A., Manna, Z., Pnueli, A.: Timed Transition Systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 226–251. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  17. 17.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)Google Scholar
  18. 18.
    The ISABELLE System, http://isabelle.in.tum.de/
  19. 19.
    Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, pp. 42–54. ACM Press (2006)Google Scholar
  20. 20.
    Paulin-Mohring, C.: Modelisation of Timed Automata in Coq. In: Kobayashi, N., Babu, C. S. (eds.) TACS 2001. LNCS, vol. 2215, pp. 298–315. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  21. 21.
    Pnueli, A.: The Temporal Logic of Programs. In: FOCS, pp. 46–57 (1977)Google Scholar
  22. 22.
    Rushby, J.: Mechanized Formal Methods: Progress and Prospects. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180, pp. 43–51. Springer, Heidelberg (1996)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Manuel Garnacho
    • 1
  • Jean-Paul Bodeveix
    • 1
  • Mamoun Filali-Amine
    • 1
  1. 1.IRIT - CNRSUniversité de ToulouseFrance

Personalised recommendations