Advertisement

Interactive Verification of Statecharts

  • Andreas Thums
  • Gerhard Schellhorn
  • Frank Ortmeier
  • Wolfgang Reif
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3147)

Abstract

In this paper, we present an approach to the interactive verification of statecharts. We use STATEMATE statecharts for the formal specification of safety critical systems and Interval Temporal Logic to formalize the proof conditions. To handle infinite data, complex functions and predicates, we use algebraic specifications.

Our verification approach is a basis for the aim of the project ForMoSA to put safety analysis techniques on formal grounds. As part of this approach, fault tree analysis (FTA) has been formalized yielding conditions that can be verified using the calculus defined in this paper. Verification conditions resulting from the formal FTA of the radio-based level crossing control have been successfully verified.

Keywords

Temporal Logic Sequential Program Sequent Calculus Dynamic Logic Symbolic Execution 
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. [Bal04]
    Balser, M.: Verifying Concurrent System with Symbolic Execution – Temporal Reasoning is Symbolic Execution with a Little Induction. PhD thesis, University of Augsburg, Augsburg, Gemany (2004) (to appear)Google Scholar
  2. [BDRS02]
    Balser, M., Duelli, C., Reif, W., Schellhorn, G.: Verifying concurrent systems with symbolic execution. Journal of Logic and Computation 12(4), 549–560 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  3. [BRS+00]
    Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 363–366. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  4. [CMZ02]
    Cau, A., Moszkowski, B., Zedan, H.: ITL – Interval Temporal Logic. Software Technology Research Laboratory, SERCentre, De Montfort University, The Gateway, Leicester LE1 9BH, UK (2002), www.cms.dmu.ac.uk/~cau/itlhomepage
  5. [DJHP98]
    Damm, W., Josko, B., Hungar, H., Pnueli, A.: A compositional real-time semantics of STATEMATE designs. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 186–238. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  6. [FFB96]
    Betriebliches Lastenheft für FunkFahrBetrieb (1996), Stand 1.10.1996Google Scholar
  7. [Har84]
    Harel, D.: Dynamic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, vol. 2, pp. 496–604. Reidel, Dordrecht (1984)Google Scholar
  8. [HLN+90]
    Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M.: Statemate: A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering 16(4) (1990)Google Scholar
  9. [HN96]
    Harel, D., Naamad, A.: The statemate semantics of statecharts. ACM Transactions on Software Engineering and Methodology 5(4), 293–333 (1996)CrossRefGoogle Scholar
  10. [HRS88]
    Heisel, M., Reif, W., Stephan, W.: Program Verification Using Dynamic Logic. In: Börger, E., Kleine Büning, H., Richter, M. (eds.) Proceedings of 1st Workshop on Computer Science Logic. LNCS, vol. 329, Springer, Heidelberg (1988)Google Scholar
  11. [KT02]
    Klose, J., Thums, A.: The STATEMATE reference model of the reference case study ‘Verkehrsleittechnik’. Technical Report 2002-01, Universit ät Augsburg (2002)Google Scholar
  12. [Mos85]
    Moszkowski, B.: A temporal logic for multilevel reasoning about hardware. IEEE Computer 18(2), 10–19 (1985)Google Scholar
  13. [OT02]
    Ortmeier, F., Thums, A.: Formale Methoden und Sicherheitsanalyse. Technical Report 15, Universität Augsburg (2002) (in German)Google Scholar
  14. [OTSW04]
    Ortmeier, F., Thums, A., Schellhorn, G., Reif, W.: Combining formal methods and safety analysis - the ForMoSA approach. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 474–493. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  15. [RST00]
    Reif, W., Schellhorn, G., Thums, A.: Formale Sicherheitsanalyse einer funkbasierten Bahnübergangsteuerung. In: Schnieder, E. (ed.) Forms 2000 – Formale Techniken für die Eisenbahnsicherung. Fortschritt-Bericht VDI, vol. Reihe 12(441) (2000)Google Scholar
  16. [SA91]
    Sperschneider, V., Antoniou, G.: Logic: A Foundation for Computer Science. Addison-Wesley, Reading (1991)zbMATHGoogle Scholar
  17. [STR02]
    Schellhorn, G., Thums, A., Reif, W.: Formal fault tree semantics. In: Proceedings of The Sixth World Conference on Integrated Design & Process Technology, Pasadena, CA (2002)Google Scholar
  18. [Thu04]
    Thums, A.: Formale Fehlerbaumanalyse. PhD thesis, Universität Augsburg, Augsburg, Germany (2004) (in German)Google Scholar
  19. [TO03]
    Thums, A., Ortmeier, F.: Formal safety analysis in transportation control. In: Schnieder, E. (ed.) International Workshop on Software Specification of Safety Relevant Transportation Control Tasks. VDI Fortschritt-Berichte, vol. 12(535), VDI Verlag GmbH (2003)Google Scholar
  20. [VGRH81]
    Vesely, W.E., Goldberg, F.F., Roberts, N.H., Haasl, D.F.: Fault Tree Handbook. Washington, D.C., NUREG-0492 (1981)Google Scholar
  21. [Wir90]
    Wirsing, M.: Algebraic Specification. Handbook of Theoretical Computer Science, vol. B, ch. 13, pp. 675–788. Elsevier, Oxford (1990)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Andreas Thums
    • 1
  • Gerhard Schellhorn
    • 1
  • Frank Ortmeier
    • 1
  • Wolfgang Reif
    • 1
  1. 1.Lehrstuhl SoftwaretechnikUniversität AugsburgAugsburgGermany

Personalised recommendations