Advertisement

Temporal Logic for Scenario-Based Specifications

  • Hillel Kugler
  • David Harel
  • Amir Pnueli
  • Yuan Lu
  • Yves Bontemps
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

Abstract

We provide semantics for the powerful scenario-based language of live sequence charts (LSCs). We show how the semantics of live sequence charts can be captured using temporal logic. This is done by studying various subsets of the LSC language and providing an explicit translation into temporal logic. We show how a kernel subset of the LSC language (which omits variables, for example) can be embedded within the temporal logic CTL*. For this kernel subset the embedding is a strict inclusion. We show that existential charts can be expressed using the branching temporal logic CTL while universal charts are in the intersection of linear temporal logic and branching temporal logic LTL ∩ CTL. Since our translations are efficient, the work described here may be used in the development of tools for analyzing and executing scenario-based requirements and for verifying systems against such requirements.

Keywords

Temporal Logic Linear Temporal Logic Linear Temporal Logic Formula Message Sequence Chart Temporal Logic Formula 
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.
    Alur, R., Holzmann, G.J., Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools 17(2), 70–77 (1996)Google Scholar
  2. 2.
    Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 114–129. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  3. 3.
    Bontemps, Y.: Automated verification of state-based specifications against scenarios (a step toward relating inter-object to intra-object specifications). Master’s thesis. University of Namur, Belgium (June 2001)Google Scholar
  4. 4.
    Bunker, A., Gopalakrishnan, G.: Verifying a VCI Bus Interface Model Using an LSC-based Specification. In: Proceedings of the Sixth Biennial World Conference on Integrated Design and Process Technology, pp. 1–12 (2002)Google Scholar
  5. 5.
    Bunker, A., Slind, K.: Property Generation for Live Sequence Charts. Technical report. University of Utah (2003)Google Scholar
  6. 6.
    Clarke, E.M., Draghicescu, I.A.: Expressibility results for linear-time and branching-time logics. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol. 354, pp. 428–437. Springer, Heidelberg (1988)CrossRefGoogle Scholar
  7. 7.
    Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001)zbMATHCrossRefGoogle Scholar
  8. 8.
    Damm, W., Klose, J.: Verification of a radio-based signalling system using the statemate verification environment. Formal Methods in System Design 19(2), 121–141 (2001)zbMATHCrossRefGoogle Scholar
  9. 9.
    Emerson, E.A.: Temporal and modal logics. In: van Leeuwen, J. (ed.) Handbook of theoretical computer science, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)Google Scholar
  10. 10.
    Gabbay, D.: The declarative past and imperative future. In: Temporal Logic in Specification. LNCS, vol. 398, pp. 407–448. Springer, Heidelberg (1987)Google Scholar
  11. 11.
    Gunter, E.L., Muscholl, A., Peled, D.: Compositional message sequence charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 496–511. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  12. 12.
    Harel, D., Kugler, H.: Synthesizing state-based object systems from LSC specifications. Int. J. of Foundations of Computer Science (IJFCS), 13(1), 5–51, (Febuary 2002) Also In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 5–51. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 13.
    Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behavioral requirements. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 378–398. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  14. 14.
    Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)Google Scholar
  15. 15.
    Harel, D., Marelly, R.: Specifying and Executing Behavioral Requirements: The Play In/Play-Out Approach. Software and System Modeling (SoSyM) 2(2), 82–107 (2003)CrossRefGoogle Scholar
  16. 16.
    Henriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: On message sequence graphs and finitely generated regular MSC languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 675–686. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  17. 17.
    Henriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: Regular collections of Message Sequence Charts. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 675–686. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  18. 18.
    Rhapsody. I-Logix, Inc., products web page, http://www.ilogix.com/products/
  19. 19.
    Klose, J., Wittke, H.: An automata based interpretation of live sequence charts. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 512. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  20. 20.
    Lettrari, M., Klose, J.: Scenario-based monitoring and testing of real-time UML models. In: 4th Int. Conf. on the Unified Modeling Language, Toronto (October 2001)Google Scholar
  21. 21.
    Maidl, M.: The common fragment of CTL and LTL. In: Proc. 41st IEEE Symp. Found. of Comp. Sci., pp. 643–652 (2000)Google Scholar
  22. 22.
    Muscholl, A., Peled, D., Su, Z.: Deciding properties for message sequence charts. In: Nivat, M. (ed.) FOSSACS 1998. LNCS, vol. 1378, pp. 226–242. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  23. 23.
    Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. Found. of Comp. Sci., pp. 46–57 (1977)Google Scholar
  24. 24.
    Sengupta, B., Cleaveland, R.: Triggered message sequence charts. In: Proceedings of the tenth ACM SIGSOFT symposium on Foundations of software engineering, pp. 167–176. ACM Press, New York (2002)CrossRefGoogle Scholar
  25. 25.
    UML. Documentation of the unified modeling language (UML). Available from the Object Management Group (OMG), http://www.omg.org
  26. 26.
    Z.120 ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Hillel Kugler
    • 1
  • David Harel
    • 2
  • Amir Pnueli
    • 1
    • 2
  • Yuan Lu
    • 3
  • Yves Bontemps
    • 4
  1. 1.New York UniversityNew YorkUSA
  2. 2.The Weizmann Institute of ScienceRehovotIsrael
  3. 3.Broadcom Corp.San JoseUSA
  4. 4.University of NamurNamurBelgium

Personalised recommendations