Multiple instances and symbolic variables in executable sequence charts

ABSTRACT

We extend live sequence charts (LSCs), a highly expressive variant of sequence diagrams, and provide the extension with an executable semantics. The extension involves support for instances that can bind to multiple objects and symbolic variables that can bind to arbitrary values. The result is a powerful executable language for expressing behavioral requirements on the level of inter-object interaction. The extension is implemented in full in our play-engine tool, with which one can execute the requirements directly without the need to build or synthesize an intra-object system model. It seems that in addition to many advantages in testing and requirements engineering, for some kinds of systems this could lead to the requirements actually serving as the final implementation.

REFERENCES

• 1: R. Alur, G. Holzmann, and D. Peled. An analyzer for message sequence charts. Software Concepts and Tools, 17(2):70--77, 1996.
• 2: D. Amyot and A. Eberlein. An Evaluation of Scenario Notations for Telecommunication Systems Development. Proc. 9th Int. Conf. on Telecommunication Systems, 2001.
• 3: Hanêne Ben-Abdallah , Stefan Leue, MESA: Support for Scenario-Based Design of Concurrent Systems, Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.118-135, March 28-April 04, 1998
• 4: Hanêne Ben-Abdallah , Stefan Leue, Timing Constraints in Message Sequence Chart Specifications, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE X) and Protocol Specification, Testing and Verification (PSTV XVII), p.91-106, November 18-21, 1997
• 5: Ward Cunningham , Kent Beck, A diagram for object-oriented programs, Conference proceedings on Object-oriented programming systems, languages and applications, p.361-367, September 29-October 02, 1986, Portland, Oregon, United States
• 6: Marko Boger , Toby Baier , Frank Wienberg , Winfried Lamersdorf, Extreme modeling, Extreme programming examined, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2001
• 7: Werner Damm , David Harel, LSCs: Breathing Life into Message Sequence Charts, Proceedings of the IFIP TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), p.451, February 15-18, 1999
• 8: Werner Damm , Jochen Klose, Verification of a Radio-Based Signaling System Using the STATEMATE Verification Environment, Formal Methods in System Design, v.19 n.2, p.121-141, September 2001 [doi>10.1023/A:1011279932612]
• 9: R. Dromey. Genetic Software Engineering. Manuscript, 2001.
• 10: I. Greenwald. Development of the vulva. In: Riddle, DL., Blumenthal, T., Meyer, BJ., and Priess, JR. editors. C. elegans II. Cold Spring Harbor, NY: Cold Spring Harbor Laboratory Press, p 519--541., 1997.
• 11: David Harel , Eran Gery, Executable Object Modeling with Statecharts, Computer, v.30 n.7, p.31-42, July 1997 [doi>10.1109/2.596624]
• 12: David Harel , Hillel Kugler, Synthesizing State-Based Object Systems from LSC Specifications, Revised Papers from the 5th International Conference on Implementation and Application of Automata, p.1-33, July 24-25, 2000
• 13: David Harel , Hillel Kugler , Rami Marelly , Amir Pnueli, Smart Play-out of Behavioral Requirements, Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, p.378-398, November 06-08, 2002
• 14: D. Harel , R. Marelly, Capturing and Executing Behavioral Requirements: The Play-In/Play-Out Approach,, Weizmann Science Press of Israel, Jerusalem, Israel, 2001
• 15: D. Harel , R. Marelly, Playing with Time: On the Specification and Execution of Time-Enriched LSCs, Proceedings of the 10th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS'02), p.193, October 11-16, 2002
• 16: David Harel , Michal Politi, Modeling Reactive Systems with Statecharts: The Statemate Approach, McGraw-Hill, Inc., New York, NY, 1998
• 17: I-Logix,Inc., products web page. http://www.ilogix.com/fs_prod.htm.
• 18: Ivar Jacobson, Object-oriented software engineering, ACM Press, New York, NY, 1991
• 19: J. Klose and B. Westphal. Relating LSC Specifications to UML Models. In Proc. of the Second International Workshop on Integration of Specification Techniques for Applications in Engineering (INT 2002), Grenoble, France, 2002.
• 20: Jochen Klose , Hartmut Wittke, An Automata Based Interpretation of Live Sequence Charts, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.512-527, April 02-06, 2001
• 21: Marc Lettrari , Jochen Klose, Scenario-Based Monitoring and Testing of Real-Time UML Models, Proceedings of the 4th International Conference on The Unified Modeling Language, Modeling Languages, Concepts, and Tools, p.317-328, October 01-05, 2001
• 22: Rational,Inc., web page. http://www.rational.com.
• 23: J. Robinson. Logic: Form and Function, chapter 11, pages 182--198. North-Holland, 1979.
• 24: Bran Selic , Garth Gullekson , Paul T. Ward, Real-time object-oriented modeling, John Wiley & Sons, Inc., New York, NY, 1994
• 25: Documentation of the Unified Modeling Language (UML), available from the Object Management Group(OMG). http://www.omg.org.
• 26: Web page http://www.extremeprogramming.org.
• 27: Z.120 ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva, 1996.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

General Terms:
Design, Languages, Verification