This Article 
 Bibliographic References 
 Add to: 
Design Synthesis from Interaction and State-Based Specifications
June 2006 (vol. 32 no. 6)
pp. 349-364
Interaction-based and state-based modeling are two complementary approaches of behavior modeling. The former focuses on global interactions between system components. The latter concentrates on the internal states of individual components. Both approaches have been proven useful in practice. One challenging and important research objective is to combine the modeling power of both effectively and then use the combination as the basis for automatic design synthesis. We present a combination of interaction-based and state-based modeling, namely, Live Sequence Charts and Z, for system specification. We then propose a way of generating distributed design from the combinations. Our approach handles systems with intensive interactive behaviors as well as complex state structures.

[1] T. Ball, R. Majumdar, T.D. Millstein, and S.K. Rajamani, “Automatic Predicate Abstraction of C Programs,” Proc. SIGPLAN Conf. Programming Language Design and Implementation, pp. 203-213, 2001.
[2] Y. Bontemps, “Relating Inter-Agent and Intra-Agent Specifications (The Case of Live Sequence Charts),” PhD thesis, Institut d'Informatique, University of Namur, Computer Science Dept., 2005.
[3] Y. Bontemps, P. Heymans, and P. Schobbens, “Lightweight Formal Methods for Scenario-Based Software Engineering,” Scenarios, pp. 174-192, 2005.
[4] Y. Bontemps and P. Schobbens, “The Complexity of Live Sequence Charts,” Proc. Int'l Conf. Foundations of Software Science and Computational Structures, pp. 364-378, 2005.
[5] Y. Bontemps, P. Schobbens, and C. Löding, “Synthesis of Open Reactive Systems from Scenario-Based Specifications,” Fundamenta Informaticae, vol. 62, no. 2, pp. 139-169, 2004.
[6] M. Broy, “Message Sequence Charts in the Development Process— Role and Limitations,” Electronic Notes Theories of Computer Science, vol. 65, no. 7, 2002.
[7] M. Broy, “A Semantic and Methodological Essence of Message Sequence Charts,” Science of Computer Programming, vol. 54, nos. 2-3, pp. 213-256, 2005.
[8] A. Cavalcanti and J. Woodcock, “A Weakest Precondition Semantics for Z,” Computer, vol. 31, no. 1, pp. 1-15, Jan. 1998.
[9] W. Damm and D. Harel, “LSCS: Breathing Life into Message Sequence Charts,” Formal Methods in System Design, vol. 19, no. 1, pp. 45-80, 2001.
[10] E.W. Dijkstra, A Discipline of Programming. Prentice-Hall, 1976.
[11] D.L. Dill, A.J. Hu, and H. Wong-Toi, “Checking for Language Inclusion Using Simulation Preorders,” Proc. Int'l Conf. Computer Aided Verification, pp. 255-265, 1991.
[12] R.L. Feldmann, J. Munch, S. Queins, S. Vorwieger, and G. Zimmermann, “Baselining a Doman-Specific Software Development Process,” Technical Report SFB501 TR-02/99, Univ. of Kaiserslautern, 1999.
[13] The Apache Software Foundation, “Xerces Java Parser v1.4.4,” http://xml.apache.orgxerces-j/, 2001.
[14] D. Harel, “Statecharts: A Visual Formulation for Complex Systems,” Science of Computer Programming, vol. 8, no. 3, pp. 231-274, 1987.
[15] D. Harel and H. Kugler, “Synthesizing State-Based Object Systems from LSC Specifications,” Foundations of Computer Science, vol. 13, pp. 5-51, 2002.
[16] D. Harel, H. Kugler, and A. Pnueli, “Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements,” Proc. Formal Methods in Software and Systems Modeling, pp. 309-324, 2005.
[17] D. Harel and R. Marelly, Come, Let's Play— Scenario-Based Programming Using LSCs and Play-Engine. Springer, 2003.
[18] O. Haugen and K. Stølen, “Stairs c Steps to Analyze Interactions with Refinement Semantics,” Proc. Int'l Conf. UML, pp. 388-402, 2003.
[19] T.A. Henzinger, O. Kupferman, and S.K. Rajamani, “Fair Simulation,” Proc. Int'l Conf. Concurrency Theory, pp. 273-287, 1997.
[20] C.A.R. Hoare, Communicating Sequential Processes. Prentice-Hall, 1985.
[21] ISO/IEC 13568:2002, “Information Technology-Z Formal Specification Notation-Syntax, Type System and Semantics,” 2002.
[22] J. Sun and J.S. Dong, “Live Sequence Charts as CSP,” , 2005.
[23] C.B. Jones, Systematic Software Development Using VDM. Prentice-Hall, 1990.
[24] J. Klose and H. Wittke, “An Automata Based Interpretation of Live Sequence Charts,” Proc. Symp. Theoretical Aspects of Computer Science, pp. 512-527, 2001.
[25] K. Koskimies and E. Mäkinen, “Automatic Synthesis of State Machines from Trace Diagrams,” Software— Practice and Experience, vol. 24, no. 7, pp. 643-658, 1994.
[26] I. Krüger, R. Grosu, P. Scholz, and M. Broy, “From MSCS to Statecharts,” Proc. IFIP Working Conf. Distributed and Parallel Embedded Systems, pp. 61-72, 1998.
[27] A. Kucera and R. Mayr, “Weak Bisimilarity with Infinite-State Systems Can Be Decided in Polynomial Time,” Proc. Int'l Conf. Concurrency Theory, pp. 368-382, 1999.
[28] E. Letier, J. Kramer, J. Magee, and S. Uchitel, “Monitoring and Control in Scenario-Based Requirements Analysis,” Proc. Int'l Conf. Software Eng., pp. 382-391, 2005.
[29] C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem, “Property Preserving Abstractions for the Verification of Concurrent Systems,” Formal Methods in System Design, vol. 6, pp. 11-44, 1995.
[30] P. Madhusudan and P.S. Thiagarajan, “Branching Time Controllers for Discrete Event Systems,” Theoretical Computer Science, vol. 274, pp. 117-149, 2002.
[31] B. Mahony and J.S. Dong, “Timed Communicating Object Z,” IEEE Trans. Software Eng., vol. 26, no. 2, pp. 150-177, Feb. 2000.
[32] R. Marelly, D. Harel, and H. Kugler, “Multiple Instances and Symbolic Variables in Executable Sequence Charts,” Proc. Int'l Conf. Object-Oriented Programming, Systems, Languages, and Applications, pp. 83-100, 2002.
[33] S. Owre, J.M. Rushby, and N. Shankar, “PVS: A Prototype Verification System,” Proc. Int'l Conf. Automated Deduction, pp. 748-752, 1992.
[34] A. Pnueli and R. Rosner, “On the Synthesis of a Reactive Module,” Proc. ACM Symp. Principles of Programming Languages, pp. 179-190, 1989.
[35] A. Pnueli and R. Rosner, “Distributed Reactive Systems Are Hard to Synthesis,” Proc. IEEE Symp. Foundations of Computer Science, 1990.
[36] P.J. Ramadge and W.M. Wonham, “Supervisory Control of a Class of Discrete Event Processes,” SIAM J. Control and Optimization, vol. 25, no. 1, pp. 206-230, 1987.
[37] F. Lin and W.M. Wonham, “Decentralized Supervisory Control of Discrete-Event Systems,” Information Sciences, vol. 44, no. 3, pp. 199-224, 1988.
[38] A. Roychoudhury and P.S. Thiagarajan, “Communicating Transaction Processes: An MSC-Based Model of Computation for Reactive Embedded Systems,” Proc. Lectures on Concurrency and Petri Nets, pp. 789-818, 2003.
[39] G. Smith and J. Derrick, “Specification, Refinement and Verification of Current Systems— An Integration of Object-Z and CSP,” Formal Methods in System Design, vol. 18, pp. 249-284, 2001.
[40] J. Sun and J.S. Dong, “From Live Sequence Charts to Distributed Implementations,” Technical Report TRC5/05, Nat'l Univ. of Singapore, 2005.
[41] J. Sun and J.S. Dong, “Synthesis of Distributed Processes from Scenario-Based Specifications,” Proc. Int'l Conf. Formal Methods, pp. 415-431, 2005.
[42] J. Sun, J.S. Dong, J. Liu, and H. Wang, “A Formal Object Approach to the Design of ZML,” Annals of Software Eng., vol. 13, pp. 329-356, 2002.
[43] W. Thomas, “On the Synthesis of Strategies in Infinite Games,” Proc. Symp. Theoretical Aspects of Computer Science, pp. 1-13, 1995.
[44] S. Uchitel and J. Kramer, “A Workbench for Synthesising Behaviour Models from Scenarios,” Proc. Int'l Conf. Software Eng., pp. 188-197, 2001.
[45] S. Uchitel, J. Kramer, and J. Magee, “Detecting Implied Scenarios in Message Sequence Chart Specifications,” Proc. Int'l Symp. Foundations of Software Eng., pp. 74-82, 2001.
[46] Int'l Telecomm. Union, Message Sequence Chart (MSC), 1999, Series Z: Languages and general software aspects for telecomm. systems.
[47] P. Welch, “Communicating Sequential Processes for Java (JCSP),” /, 2003.
[48] J. Whittle, J. Saboo, and R. Kwan, “From Scenarios to Code: An Air Traffic Control Case Study,” Proc. Int'l Conf. Software Eng., pp. 490-497, 2003.
[49] J. Woodcock and J. Davies, Using Z: Specification, Refinement, and Proof. Prentice-Hall, 1996.

Index Terms:
Z language, live sequence charts, specification, synthesis.
Jun Sun, Jin Song Dong, "Design Synthesis from Interaction and State-Based Specifications," IEEE Transactions on Software Engineering, vol. 32, no. 6, pp. 349-364, June 2006, doi:10.1109/TSE.2006.55
Usage of this product signifies your acceptance of the Terms of Use.