Formal Composition of Distributed Scenarios

  • Aziz Salah
  • Rabeb Mizouni
  • Rachida Dssouli
  • Benoît Parreaux
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3235)


Eliciting, modeling, and analyzing the requirements are the main challenges to face up when you want to produce a formal specification for distributed systems. The distribution and the race conditions between events make it difficult to include all the possible scenario combinations and thus to get a complete specification. Most research about formal methods dealt with languages and neglected the process of how getting a formal specification. This paper describes a scenario-based process to synthesize a formal specification in the case of a distributed system. The requirements are represented by a set of use cases where each one is composed of a collection of distributed scenarios. The architectural assumptions about the communication between the objects of the distributed system imply some completions and reorganizations in the use cases. Then, the latter are composed into a global finite state machine (FSM) from which we derive a communicating FSM per object in the distributed system.


Use case Scenario-based approach Scenario composition Formal specification Distributed systems FSM 


  1. 1.
    Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: principles, techniques, and tools. Addison Wesley, Reading (1986)zbMATHGoogle Scholar
  2. 2.
    Alur, R., Etessami, K., Yannakakis, M.: Inference of message sequence charts. Presented at 22nd International Conference on Software Engineering (2000)Google Scholar
  3. 3.
    Alur, R., Holzmann, G., Peled, D.: An Analyzer for Message Sequence Charts. Software: Concepts and Tools 17, 70–77 (1996)Google Scholar
  4. 4.
    Ben-Abdallah, H., Leue, S.: Syntactic Detection of Process Divergence and Nonlocal Choice in Message Sequence Charts. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 259–274. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  5. 5.
    Fikes, R., Nilsson, N.J.: STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artif. Intell. 2, 189–208 (1971)CrossRefzbMATHGoogle Scholar
  6. 6.
    Giese, H.: Towards Scenario-Based Synthesis for Parametric Timed Automata. Presented at the 2nd International Workshop on Scenarios and State Machines: Models, Algorithms, and Tools, ICSE, Portland, USA (2003)Google Scholar
  7. 7.
    Harel, D.: From Play-In Scenarios To Code: An Achievable Dream. IEEE Computer 34, 53–60 (2001)CrossRefGoogle Scholar
  8. 8.
    Harel, D., Kugler, H.: Synthesizing State-Based Object Systems from LSC Specifications. Int. J. of Foundations of Computer Science 13, 5–51 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    ITU, Recommendation Z.120: Message Sequence Chart, MSC (1999)Google Scholar
  10. 10.
    Koskimies, K., Mäkinen, E.: Automatic Synthesis of State Machines from Trace Diagrams. Software-Practice and Experience 24, 643–658 (1994)CrossRefGoogle Scholar
  11. 11.
    Krüger, I., Grosu, R., Scholz, P., Broy, M.: From MSCs to Statecharts, presented at Distributed and Parallel Embedded Systems (1998)Google Scholar
  12. 12.
    Lynch, N.: I/O Automata: A model for discrete event systems, presented at 22nd Annual Conference on Information Sciences and Systems, Princeton University, Princeton, N.J. (1988)Google Scholar
  13. 13.
    Mäkinen, E., Systä, T.: MAS – An Interactive Synthesizer to Support Behavioral Modeling in UML. In: presented at ICSE 2001, Toronto, Canada (2001)Google Scholar
  14. 14.
    Muccini, H.: Detecting Implied Scenarios analyzing non-local Branching Choices. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 372–386. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  15. 15.
    Mukund, M., Kumar, K.N., Sohoni, M.A.: Synthesizing distributed finite-state systems from MSCs. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, p. 521. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    OMG, Unified Modeling Language (UML) specification v1.5, OMG document ad/2003-03-01 (March 2003)Google Scholar
  17. 17.
    Salah, A., Dssouli, R., Lapalme, G.: Compiling real-time scenarios into a Timed Automaton, presented at FORTE XIV/PSTV XXI (2001)Google Scholar
  18. 18.
    Somé, S., Dssouli, R., Vaucher, J.: Toward an Automation of Requirements Engineering using Scenarios. Journal of Computing and Information 2, 1110–1132 (1996)Google Scholar
  19. 19.
    Uchitel, S., Kramer, J., Magee, J.: Synthesis of behavioral models from scenarios. IEEE Transactions on Software Engineering 29, 99–115 (2003)CrossRefGoogle Scholar
  20. 20.
    Whittle, J., Schumann, J.: Generating statechart designs from scenarios, presented at 22nd International Conference on Software (2000)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2004

Authors and Affiliations

  • Aziz Salah
    • 1
  • Rabeb Mizouni
    • 2
  • Rachida Dssouli
    • 3
  • Benoît Parreaux
    • 4
  1. 1.Department of C.S.University of Quebec at MontrealCanada
  2. 2.Electrical & Computer EngineeringConcordia UniversityUSA
  3. 3.Institute For Information System EngineeringConcordia UniversityUSA
  4. 4.France Telecom R&DLannionFrance

Personalised recommendations