Abstract
Live Sequence Charts (LSCs) are an established visual formalism for requirements in formal, model-based development, in particular aiming at formal verification of the model. The model-checking problem for LSCs is principally long solved as each LSC has an equivalent LTL formula, but even for moderate sized LSCs the formulae grow prohibitively large. In this paper we elaborate on practically relevant sub-classes of LSCs, namely bonded and time bounded, which don’t require the full power of LTL model-checking. For bonded LSCs, a combination of observer automaton and fixed small liveness property and for additionally time bounded LSCs reachability checking is sufficient.
Partly supported by DFG, grants SFB/TR 14 AVACS and DA 206/7-3, SPP 1064.
Chapter PDF
Similar content being viewed by others
Keywords
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
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design 19, 45–80 (2001)
Westphal, B., Toben, T.: The good, the bad and the ugly: Well-formedness of Live Sequence Charts. In: Baresi, L., Heckel, R. (eds.) FASE 2006 and ETAPS 2006. LNCS, vol. 3922, pp. 230–246. Springer, Heidelberg (2006)
Toben, T., Westphal, B.: On the expressive power of LSCs. In: Wiedermann, J., Tel, G., Pokorný, J., Bieliková, M., Štuller, J. (eds.) SOFSEM 2006. LNCS, vol. 3831, pp. 33–43. Springer, Heidelberg (2006)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of theor. comp. sc (vol. B): Formal Models And Semantics, pp. 133–191. MIT Press, Cambridge (1990)
Klose, J.: Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior. PhD thesis, C.v.O. Universität Oldenburg (2003)
Bohn, J., Damm, W., Wittke, H., Klose, J., Moik, A.: Modelling and validating train system applications using statemate and live sequence charts. In: Proc. IDPT 2002, Society for Design and Process Science (2002)
Schinz, I., Toben, T., Mrugalla, C., Westphal, B.: The Rhapsody UML Verification Environment. In: Cuellar, J.R., Liu, Z. (eds.) Proc. SEFM 2004, pp. 174–183 (2004)
Westphal, B.: LSC verification for UML models with unbounded creation and destruction. In: Cook, B., Scott Stoller, W.V. (eds.) Proc. SoftMC 2005. ENTCS, vol. 144:3, pp. 133–145. Elsevier, Amsterdam (2005)
Toben, T., Westphal, B.: Concurrent LSC verification. In: Lazic, R. (ed.) Proc. AVoCS 2005. ENTCS, vol. 145, pp. 95–111. Elsevier, Amsterdam (2006)
Bunker, A., Gopalakrishnan, G., Slink, K.: Live sequence charts applied to hardware requirements specification and verification: A VCI bus interface model. Software Tools for Technology Transfer 7(4), 341–350 (2004)
Harel, D., Kugler, H., Marelly, R., Pnueli, A.: Smart play-out of behvioral 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. Springer, Heidelberg (2003)
Sun, J., Dong, J.S.: Model checking Live Sequence Charts. In: ICECCS, pp. 529–538. IEEE Computer Society, Los Alamitos (2005)
Grégoire, B.: Automata oriented program verification. Master’s thesis, Facultés Universitaires Notre-Dame de la Paix, Namur (2002)
Wittke, H.: A Framework for Specification Verification for Complex Embedded Systems. PhD thesis, C.v.O. Universität Oldenburg (2005)
Schlör, R.C.: Symbolic Timing Diagrams: A Visual Formalism for Model Verification. PhD thesis, C.v.O. Universität Oldenburg (2000)
Kugler, H., et al.: Temporal logic for scenario-based specifications. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 445–460. Springer, Heidelberg (2005)
Brill, M., et al.: Formal verification of LSCs in the development process. 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. 494–516. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Klose, J., Toben, T., Westphal, B., Wittke, H. (2006). Check It Out: On the Efficient Formal Verification of Live Sequence Charts. In: Ball, T., Jones, R.B. (eds) Computer Aided Verification. CAV 2006. Lecture Notes in Computer Science, vol 4144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817963_22
Download citation
DOI: https://doi.org/10.1007/11817963_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37406-0
Online ISBN: 978-3-540-37411-4
eBook Packages: Computer ScienceComputer Science (R0)