Abstract
Message Sequence Charts (MSC) have traditionally been used as a weak form of behavioral requirements in software design; they denote scenarios which may happen. Live Sequence Charts (LSC) extend Message Sequence Charts by also allowing the designer to specify scenarios which must happen. Live Sequence Chart specifications are executable; their simulation allows the designer to play out potentially aberrant scenarios prior to software construction. In this paper, we propose the use of Constraint Logic Programming (CLP) for symbolic execution of requirements described as Live Sequence Charts. The utility of CLP stems from its ability to execute in the presence of uninstantiated variables. This allows us to simulate multiple scenarios at one go. For example, several scenarios which only differ from each other in the value of a variable may be executed as a single scenario where the variable is left uninstantiated. Similarly, we can simulate scenarios with an unbounded number of processes. We use the power of CLP to also simulate charts with non-trivial timing constraints. Current works on MSC/LSCs use data/control variables mainly for ease of specification; they are instantiated to concrete values during simulation. Thus, our work advances the state-of-the-art in simulation and checking of MSC based software requirements.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Holzmann, G.J., Peled, D.A.: An analyzer for message sequence charts. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, Springer, Heidelberg (1996)
Alur, R., Yannakakis, M.: Model checking of message sequence charts. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, p. 114. Springer, Heidelberg (1999)
Booch, G., Jacobsen, I., Rumbaugh, J.: Unified Modeling Language for Objectoriented development. Rational Software Corporation (1996)
Butler, M., Leuschel, M.: ProB: A model checker for B. In Formal Methods in Europe (FME). In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, Springer, Heidelberg (2003)
Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1) (2001)
Delzanno, G., Podelski, A.: Model checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, p. 223. Springer, Heidelberg (1999)
ECLiPSe. The ECLiPSe Constraint Logic Programming System (2003), Available from http://www-icparc.doc.ic.ac.uk/eclipse/
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, Springer, Heidelberg (2002)
Harel, D., Marelly, R.: Playing with time: On the specification and execution of time-enriched LSCs. In: IEEE/ACM Intl. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, MASCOTS (2002)
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Hendriksen, J.G., Mukund, M., Kumar, K.N., Thiagarajan, P.S.: Message sequence graphs and finitely generated regular MSC languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, p. 675. Springer, Heidelberg (2000)
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)
Marelly, R., Harel, D., Kugler, H.: Multiple instances and symbolic variables in executable sequence charts. In: Intl. Conf. on Object Oriented Programming, Systems, Languages and Applications, OOPSLA (2002)
Narain, S., Chadha, R.: Symbolic discrete event simulation. In: Discrete Event Systems, Manufacturing Systems and Communication Networks (1994)
Roychoudhury, A., Thiagarajan, P.S.: Communicating transaction processes. In: IEEE Intl. Conf. on Appl. of Concurrency in System Design, ACSD (2003)
Z.120. Message Sequence Charts (MSC 1996) (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, T., Roychoudhury, A., Yap, R.H.C., Choudhary, S.C. (2004). Symbolic Execution of Behavioral Requirements. In: Jayaraman, B. (eds) Practical Aspects of Declarative Languages. PADL 2004. Lecture Notes in Computer Science, vol 3057. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24836-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-24836-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22253-8
Online ISBN: 978-3-540-24836-1
eBook Packages: Springer Book Archive