Scenario based methods for System Design

Title: Scenario based methods for system design
Presenters:     Abhik Roychoudhury and P. S. Thiagarajan,
                            School of Computing,
                            National University of Singapore.
Date: 20th June, 2005

Outline:

Message Sequence Charts (MSCs) are an appealing visual notation for specifying patterns of interactions between processes. This notation has found its way into many design methodologies. A variant of MSCs called sequence diagrams is a part of the UML notational framework.

One main role of MSCs is to capture system requirements in terms of "good" scenarios the implementation should exhibit and "bad" scenarios it must avoid. A good part of research on MSCs, driven by this use, focuses on mechanisms for specifying collections of MSCs, ways of analyzing such collections and relating them to implementation models.

On the other hand, a broad extension of MSCs called Live Sequence Charts (LSCs) have been proposed by David Harel and Werner Damm to serve as a full specification language. Further, David Harel and co-workers have developed a powerful execution engine called the Play-Engine to support system designs based on LSCs. From a conceptual standpoint, the models called netcharts, Communicating Transaction Processes (CTPs) and Object CTPs (OCTPs) also falls within this framework.

In our tutorial, we will survey the theory, modelling examples, tools and applications covering both these themes.

Schedule:

Time	Topic(s) Covered	References
9:00am - 10:30am	Message Sequence Charts (MSCs) Hierarchical Message Sequence Charts (HMSCs) MSCs in Telecom setting	ITU Telecommunication Standardization Sector (ITU-T). Annex B to Z.120. Formal Semantics of Message Sequence Charts, 2000. Message Sequence Charts. D. Harel and P.S. Thiagarajan. In: UML for Real: Design of Embedded Real-time Systems, Eds.: Luciano Lavagno, Grant Martin and Bran Selic, Kluwer Academic Publishers, 2003. An analyzer for Message Sequence Charts. Rajeev Alur, Gerard J. Holzmann, and Doron Peled. Software - Concepts and Tools, 17(2):70-77, 1996. Model Checking of Message Sequence Charts. Rajeev Alur and Mihalis Yannakakis. CONCUR, pages 114-129, 1999.
11:00am - 12:30pm	Live Sequence Charts (LSCs)	LSCs: Breathing life into message sequence charts. Werner Damm and David Harel. Formal Methods in System Design, 19(1):45-80, 2001. Synthesizing State-Based Object Systems from LSC Specifications. D. Harel and H. Kugler. Intl. Jnl. on Foundations of Computer Science (IJFCS), 13, 2002. Multiple Instances and Symbolic Variables in Executable Sequence Charts. R. Marelly, D. Harel and H. Kugler. Intl. Conf. on Object Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 83-100, 2002. Symbolic Execution of Behavioral Requirements. T. Wang, A. Roychoudhury, R.H.C. Yap and S.C. Choudhary. Practical Applications of Declarative Languages (PADL), LNCS 3057, 2004 .
1:30pm - 3:30pm	Combining intra-component and inter-component descriptions: -- Communicating Transaction Processes (CTP) -- Netcharts -- Object CTP (OCTP)	Communicating Transaction Processes. A. Roychoudhury and P.S. Thiagarajan. Proc. of the 3rd IEEE International Conference on Application of Concurrency in System Design (ACSD'03), IEEE Press, 2003. Netcharts: Bridging the gap between HMSCs and executable specifications. M. Mukund, K Narayan Kumar and P.S. Thiagarajan: Proc. of the 14th International Conference on Concurrency Theory (CONCUR'03), Springer Lecture Notes in Computer Science 2761, Springer-Verlag, 2003.

Acknowledgments:

Some of our works have been partially supported by research grants from Agency of Science Technology and Research (A*STAR) Singapore.