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.
Chapter PDF
References
Alur, R., Holzmann, G.J., Peled, D.: An analyzer for message sequence charts. Software Concepts and Tools 17(2), 70–77 (1996)
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)
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)
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)
Bunker, A., Slind, K.: Property Generation for Live Sequence Charts. Technical report. University of Utah (2003)
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)
Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001)
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)
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)
Gabbay, D.: The declarative past and imperative future. In: Temporal Logic in Specification. LNCS, vol. 398, pp. 407–448. Springer, Heidelberg (1987)
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)
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)
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)
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
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)
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)
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)
Rhapsody. I-Logix, Inc., products web page, http://www.ilogix.com/products/
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)
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)
Maidl, M.: The common fragment of CTL and LTL. In: Proc. 41st IEEE Symp. Found. of Comp. Sci., pp. 643–652 (2000)
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)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. Found. of Comp. Sci., pp. 46–57 (1977)
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)
UML. Documentation of the unified modeling language (UML). Available from the Object Management Group (OMG), http://www.omg.org
Z.120 ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kugler, H., Harel, D., Pnueli, A., Lu, Y., Bontemps, Y. (2005). Temporal Logic for Scenario-Based Specifications. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)