Advertisement

Requirements Validation for Hybrid Systems

  • Alessandro Cimatti
  • Marco Roveri
  • Stefano Tonetta
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

The importance of requirements for the whole development flow calls for strong validation techniques based on formal methods. In the case of discrete systems, some approaches based on temporal logic satisfiability are gaining increasing momentum. However, in many real-world domains (e.g. railways signaling), the requirements constrain the temporal evolution of both discrete and continuous variables. These hybrid domains pose substantial problems: on one side, a continuous domain requires very expressive formal languages; on the other side, the resulting expressiveness results in highly intractable problems.

In this paper, we address the problem of requirements validation for real-world hybrid domains, and present two main contributions. First, we propose the HRELTL logic, that extends the Linear-time Temporal Logic with Regular Expressions (RELTL) with hybrid aspects. Second, we show that the satisfiability problem for the linear fragment can be reduced to an equi-satisfiable problem for RELTL. This makes it possible to use automatic (albeit incomplete) techniques based on Bounded Model Checking and on Satisfiability Modulo Theory.

The choice of the language is inspired by and validated within a project funded by the European Railway Agency, on the formalization and validation of the European Train Control System specifications. The activity showed that most of requirements can be formalized into HRELTL, and an experimental evaluation confirmed the practicality of the analyses.

Keywords

Hybrid System Temporal Logic Regular Expression Linear Temporal Logic Hybrid Automaton 
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.

References

  1. 1.
    The PROSYD project on property-based system design (2007), http://www.prosyd.org
  2. 2.
    Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In: Hybrid Systems, pp. 209–229 (1992)Google Scholar
  3. 3.
    Alur, R., Henzinger, T.A.: Logics and Models of Real Time: A Survey (1992)Google Scholar
  4. 4.
    Alur, R., Henzinger, T.A.: Real-Time Logics: Complexity and Expressiveness. Inf. Comput. 104(1), 35–77 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 6.
    Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191–206. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Chaochen, Z., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Hybrid Systems, pp. 36–59 (1992)Google Scholar
  9. 9.
    Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Cimatti, A., Roveri, M., Susi, A., Tonetta, S.: Object models with temporal constraints. In: SEFM 2008, pp. 249–258. IEEE Press, Los Alamitos (2008)Google Scholar
  11. 11.
    Cimatti, A., Roveri, M., Tonetta, S.: Symbolic Compilation of PSL. IEEE Trans. on CAD of Integrated Circuits and Systems 27(10), 1737–1750 (2008)CrossRefGoogle Scholar
  12. 12.
    Cimatti, A., Roveri, M., Tonetta, S.: Requirements Validation for Hybrid Systems. Technical Report 200904002, FBK, Extended version of CAV 2009 (2009)Google Scholar
  13. 13.
    Claessen, K.: A coverage analysis for safety property lists. In: FMCAD, pp. 139–145. IEEE, Los Alamitos (2007)Google Scholar
  14. 14.
    de Alfaro, L., Manna, Z.: Verification in Continuous Time by Discrete Reasoning. In: Alagar, V.S., Nivat, M. (eds.) AMAST 1995. LNCS, vol. 936, pp. 292–306. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  15. 15.
    ERTMS/ETCS — Baseline 3: System Requirements Specifications. SUBSET-026-1, i3.0.0 (2008), http://www.era.europa.eu/core/ertms/Pages/FirstETCSSRS300.aspx
  16. 16.
    Eveking, H., Braun, M., Schickel, M., Schweikert, M., Nimbler, V.: Multi-level assertion-based design. In: MEMOCODE, pp. 85–86. IEEE, Los Alamitos (2007)Google Scholar
  17. 17.
    Faber, J., Meyer, R.: Model checking data-dependent real-time properties of the european train control system. In: FMCAD, pp. 76–77 (2006)Google Scholar
  18. 18.
    Furia, C.A., Pradella, M., Rossi, M.: Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 132–147. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  19. 19.
    Heitmeyer, C.L.: Requirements Specifications for Hybrid Systems. In: Hybrid Systems, pp. 304–314 (1995)Google Scholar
  20. 20.
    Henzinger, T.A.: The Theory of Hybrid Automata. In: LICS, pp. 278–292 (1996)Google Scholar
  21. 21.
    Henzinger, T.A., Manna, Z., Pnueli, A.: Towards refining temporal specifications into hybrid systems. In: Hybrid systems, pp. 60–76 (1992)Google Scholar
  22. 22.
    Henzinger, T.A., Manna, Z., Pnueli, A.: What Good Are Digital Clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  23. 23.
    Kapur, A.: Interval and point-based approaches to hybrid system verification. PhD thesis, Stanford, CA, USA (1998)Google Scholar
  24. 24.
    Maler, O., Manna, Z., Pnueli, A.: From Timed to Hybrid Systems. In: REX Workshop, pp. 447–484 (1991)Google Scholar
  25. 25.
    Maler, O., Nickovic, D., Pnueli, A.: Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. In: Pillars of Computer Science, pp. 475–505 (2008)Google Scholar
  26. 26.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)CrossRefzbMATHGoogle Scholar
  27. 27.
    Manna, Z., Pnueli, A.: Verifying Hybrid Systems. In: Hybrid Systems, pp. 4–35 (1992)Google Scholar
  28. 28.
    Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: DAC, pp. 821–826 (2006)Google Scholar
  29. 29.
    Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS, vol. 4548, pp. 216–232. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  30. 30.
    Tiwari, A.: Abstractions for hybrid systems. Formal Methods in System Design 32(1), 57–83 (2008)CrossRefzbMATHGoogle Scholar
  31. 31.
    Wang, F.: Time-Progress Evaluation for Dense-Time Automata with Concave Path Conditions. In: ATVA, pp. 258–273 (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Alessandro Cimatti
    • 1
  • Marco Roveri
    • 1
  • Stefano Tonetta
    • 1
  1. 1.Fondazione Bruno Kessler (FBK-irst)TrentoItaly

Personalised recommendations