Abstract
This paper presents how a model-based development process can be enhanced by the combination of using Live Sequence Charts (LSC) as the formal language to describe interactions together with automatic formal verification techniques that decide whether communication sequences are exhibitable or adhered to by the system. We exemplify our approach on the V-model, a widely used development process, considering a (Statemate) statecharts design of the reference case study “Funkfahrbetrieb” (FFB) and discuss potential assets and drawbacks. We sketch a set of best practices on the use of LSC features and emphasise the possibilities for re-use of LSCs in the different activities of the development process. To give evidence for feasibility of automatic formal verification of LSCs, as well as its limitations, we present our approaches to the verification of possible and mandatory LSC requirements on Statemate models. We report experimental results we have obtained from formal verification of the FFB and briefly discuss the treatment of Statemate’s different notions of time.
This research was supported by the German Research Council (DFG) within the priority program Integration of Specification Techniques with Engineering Applications under grant DA 206/7 and by the German Department of Education and Research (BMBF), research project ‘ViSEK’, under grant 01ISA02G.
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.
Similar content being viewed by others
References
Jacobson, I., Booch, G., Rumbaugh, J.: The Unified Software Development Process. Addison-Wesley, Reading (1999)
Beck, K.: Extreme Programming Explained. Addison-Wesley, Reading (1999)
EStdIT, B.d.I.: V-Model, Development Standard for IT-Systems of the federal Republic of Germany (1997)
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, 403–414 (1990)
OMG: 1.4-uml-01-09-67 (2001)
Harel, D., Marelly, R.: Come, Let’s Play: Scenario-Based Programming Using LSCs and the Play-Engine. Springer, Heidelberg (2003)
Damm, W., Harel, D.: LSCs: Breathing Life into Message Sequence Charts. Formal Methods in System Design 19, 121–141 (2001)
ITU-T: ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T, Geneva (1999)
Bienmüller, T., Damm, W., Wittke, H.: The statemate verification environment - making it real. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 561–567. Springer, Heidelberg (2000)
Brill, M., Damm, W., Klose, J., Westphal, B., Wittke, H.: Live sequence charts. 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. 374–399. Springer, Heidelberg (2004)
Klose, J., Kropf, T., Ruf, J.: A Visual Approach to Validating System Level Designs. In: Proceedings ISSS 2002, pp. 186–191. ACM Press, New York (2002)
Klose, J., Lettrari, M.: Scenario-based Monitoring and Testing of Real-time UML models. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, p. 317. Springer, Heidelberg (2001)
Hänsel, F., Poliak, J., Slovák, R., Schnieder, E.: Reference case study for comparison and validation of formal specifications using a model demonstrator. 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. 96–118. Springer, Heidelberg (2004)
Jansen, L.: Referenzfallstudie Verkehrsleittechnik (1997) http://www.iva.ing.tubs.de/institut/projekte/Referenzfallstudie_vklt/referenz.html (16.5.2004)
AG, D.B.: Betriebliches Lastenheft für FunkFahrBetrieb (1996) Minimalkonzept, Version 2.0.
Klose, J., Thums, A.: The Statemate Reference Model of the Reference Case Study ’Verkehrsleittechnik’. Technical report, University of Augsburg (2000), http://www.Informatik.Uni-Augsburg.DE/swt/formosa/RefVL/bericht.ps.gz
Klose, J.: Live Sequence Charts: A Graphical Formalism for the Specification of Communication Behavior. PhD thesis, Carl von Ossietzky Universität Oldenburg (2003)
Klose, J., Moik, A.: Modellierung der FORMS-Fallstudien mit Statemate. In: Schnieder, E. (ed.) Proceedings FORMS 2000. Fortschritt-Berichte VDI Reihe 12, vol. 441, VDI Verlag (2000)
Damm, W., Döhmen, G., Klose, J.: Secure Decentralized Control of Railway Crossings. In: Gnesi, S., Latella, D. (eds.) Fourth International ERCIM Workshop on Formal Methods in Industrial Critical Systems (1999)
Harel, D., Naamad, A.: The statemate semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5, 293–333 (1996)
Josko, B.: Modular specification and verification of reactive systems. Carl von Ossietzky Universität Oldenburg, Habilitationsschrift (1993)
Schlör, R.C.: Symbolic Timing Diagrams: A Visual Formalism for Model Verification. PhD thesis, Universität Oldenburg (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)
The VIS Group: VIS: A System for Verification and Synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Sheeran, M., Stålmarck, G.: A tutorial on Stålmarck’s proof procedure for propositional logic. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 82–99. Springer, Heidelberg (1998)
Grégoire, B.: Automata oriented program verification. Master’s thesis, Facultés Universitaires Notre-Dame de la Paix, Namur (2002)
Harel, D., Marelly, R.: Playing with Time: On the Specification and Execution of Time-Enriched LSCs. In: Proceedings MASCOTS 2002 (2002)
Damm, W., Westphal, B.: Live and let die: LSC-based verification of UML-models. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 99–135. Springer, Heidelberg (2003)
McMillan, K.L.: A Methodology for Hardware Verification using Compositional Model Checking. Science of Computer Programming 37, 279–309 (2000)
Xie, F., Browne, J.: Integrated State Space Reduction for Model Checking Executable Object-oriented Software System Designs. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, p. 64. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Brill, M., Buschermöhle, R., Damm, W., Klose, J., Westphal, B., Wittke, H. (2004). Formal Verification of LSCs in the Development Process. In: Ehrig, H., et al. Integration of Software Specification Techniques for Applications in Engineering. Lecture Notes in Computer Science, vol 3147. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27863-4_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-27863-4_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23135-6
Online ISBN: 978-3-540-27863-4
eBook Packages: Springer Book Archive