Abstract
Two fundamental problems related to Scenario-based Software Engineering (SBSE) are presented: model checking and synthesis. The former is to verify that a design model is consistent with a scenario-based specification. The latter is to build a design model implementing correctly a specification. Model checking is computationally expensive and synthesis of distributed system is undecidable. Two lightweight techniques are thus presented that alleviate this intractability. These approaches sacrifice completeness for efficiency, but keep soundness.
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., Etessami, K., Yannakakis, M.: Inference of Message Sequence Charts. In: Proceedings of 22nd International Conference on Software Engineering, pp. 304–313 (2000)
Alur, R., Holzmann, G.J., Peled, D.: An analyser for mesage sequence charts. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055. Springer, Heidelberg (1996)
Abadi, M., Lamport, L.: Martín Abadi and Leslie Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems 14(4), 1–60 (1992)
Ben-Abdallah, H., Leue, S.: Syntactic Detection of Process Divergence and Nonlocal Choice in Message Sequence Charrts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 259–274. Springer, Heidelberg (1997)
Bontemps, Y., Heymans, P., Kugler, H.: Applying LSCs to the specification of an air traffic control system. In: Uchitel, S., Bordeleau, F. (eds.) Proc. of the 2nd Int. Workshop on “Scenarios and State Machines: Models, Algorithms and Tools” (SCESM 2003), at the 25th Int. Conf. on Soft. Eng. (ICSE 2003), Portland, OR, USA, May 2003, IEEE, Los Alamitos (2003)
Bontemps, Y.: Automated Verification of State-based Specifications Against Scenarios (A Step towards Relating Inter-Object to Intra-Object Specifications). Master’s thesis, University of Namur (June 2001)
Bontemps, Y.: Realizability of scenario-based specifications. Diplôme d’études approfondies, University of Namur (September 2003)
Broy, M.: Unifying models and engineering theories of composed software systems. In: Broy, M., Pizka, M. (eds.) Models, Algebras and Logics of Engineering Software. NATO Science Series, III: Computer and Systems Sciences, vol. 191, pp. 1–41. IOS Press, Amsterdam (2003)
Bontemps, Y., Schobbens, P.-Y.: Synthesizing open reactive systems from scenario-based specifications. In: Balarin, F., Lilius, J. (eds.) Proc. of the 3rd Int. Conf. on Applications of Concurrency to System Design (ACSD 2003), Guimarães, Portugal, June 2003, pp. 41–50. IEEE Computer Science Press, Los Alamitos (2003)
Bontemps, Y., Schobbens, P.-Y.: The computational complexity of scenario-based agent verification and design. Technical Report 2004.35, CFV (Centre Fédéré en Vérification) (October 2004), http://www.ulb.ac.be/di/ssd/cfv/publications.html
Cobben, J.M.H., Engels, A., Mauw, S., Michel Reniers, A.: Formal Semantics of Message Sequence Charts (ITU-T Recommendation Z.120 Annex B). In: International Telecommunication Union, Eindhoven, The Netherlands (April 1998), http://www.itu.int
Caillaud, B., Muscholl, A.: VISS 2002: Validation and Implementation of Scenario-based Specifications (ETAPS 2002) (April 2002), http://www.liafa.jussieu.fr/~anca/VISS02.html
Damm, W., Harel, D.: LSCs: Breathing life into message sequence charts. Formal Methods in System Design 19(1), 45–80 (2001)
Emerson., E.A.: Temporal and Modal Logic, vol. B.,ch.16, pp. 997–1072. MIT Press and Elsevier Science Publishers, Cambridge (1990) ISBN 0-262-72015-9 (Second Printing, 1998)
Finkbeiner, B., Krüger, I.H.: Using message sequence charts for component-based formal verification. In: Proc. of OOPSLA 2001 Workshop on Specification and Verification of Component-Based Systems, Tampa Bay, FL, USA (October 2001)
Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)
Harel, D.: From play-in scenarios to code: An achievable dream. IEEE Computer 34(1), 53–60 (2001)
Heymans, P.: Animating Albert II Specifications. PhD thesis, University of Namur (2001)
Harel, D., Marelly, R.: Capturing and Analyzing Behavioral Requirements: The Play-In/Play-Out Approach. Technical Report MCS01-15, The Weizmann Institute of Science, Faculty of Mathematics and Computer Science, Rehovot, Israel (September 2001)
Harel, D., Marelly, R.: Come, let’s play! Scenario-based programming using LSCs and the Play-engine. Springer, Heidelberg (2003) ISBN 3-540-00787-3
MSC-2000: ITU-T Recommendation Z.120 : Message Sequence Chart (MSC) (2000), http://www.itu.int/
Jacobson, I.: Object Oriented Software Engineering: a Use-Case Driven Approach. ACM Press/Addison-Wesley (1992)
Kugler, H., Harel, D., Pnueli, A., Yuan, L., Bontemps, Y.: Temporal Logic for Live Sequence Charts. Unpublished draft (January 2001)
Krüger, I.H.: Distributed System Design with Message Sequence Charts. PhD thesis, Technische Universität München (July 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)
Leue, S., Mehrmann, L., Rezai, M.: Synthesizing ROOM models from message sequence charts specifications. In: Proc. of 13th IEEE Conference on Automated Software Engineering, Honolulu, Hawaii (October 1998)
Lynch, N.A., Tuttle, M.R.: An introduction to input/output automata. CWI Quarterly 2(3), 219–246 (1989)
Object Management Group (UML Revision Task Force). OMG UML Specification (2.0) (September 2003), http://www.omg.org/uml
Ryser, J., Glinz, M.: SCENT: A Method Employing Scenarios to Systematically Derive Test Cases for System Test. Technical Report 2000/3, Institut für Informatik - Universität Zurich, Winterthurerstrasse 190, 8057 Zurich, Switzerland (2000)
Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, The Weizmann Institute of Science, Rehovot, Israel (April 1992)
Uchitel, S.: Elaboration of Behaviour Models and Scenario-based Specifications using Implied Scenarios. PhD thesis, Imperial College London (January 2003)
Uchitel, S., Kramer, J., Magee, J.: Detecting implied scenarios in message sequence chart specifications. In: Gruhn, V. (ed.) Proceedings of the Joint 8th European Software Engeneering Conference and 9th ACM SIGSOFT Symposium on the Foundation of Software Engeneering (ESEC/FSE-2001), Software Engineering Notes, New York, September 10–14, vol. 26(5), pp. 74–82. ACM Press, New York (2001)
Weidenhaupt, K., Pohl, K., Jarke, M., Haumer, P.: Scenario Usage in System Development: A Report on Current practice. IEEE Software 15(2), 34–45 (1998)
Whittle, J., Schumann, J.: Statechart Synthesis from Scenarios: an Air Traffic Control Case Study. In: Proc. of ”Scenarios and State-Machines: models, algorithms and tools” workshop at the 24th Int. Conf. on Software Engineering (ICSE 2002), Orlando, FL, May 20, 2002. ACM, New York (2002)
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
Bontemps, Y., Heymans, P., Schobbens, PY. (2005). Lightweight Formal Methods for Scenario-Based Software Engineering. In: Leue, S., Systä, T.J. (eds) Scenarios: Models, Transformations and Tools. Lecture Notes in Computer Science, vol 3466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11495628_10
Download citation
DOI: https://doi.org/10.1007/11495628_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26189-6
Online ISBN: 978-3-540-32032-6
eBook Packages: Computer ScienceComputer Science (R0)