This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Template Semantics for Model-Based Notations
October 2003 (vol. 29 no. 10)
pp. 866-882
Joanne M. Atlee, IEEE Computer Society

Abstract—We propose a template-based approach to structuring the semantics of model-based specification notations. The basic computation model is a nonconcurrent, hierarchical state-transition machine (HTS), whose execution semantics are parameterized. Semantics that are common among notations (e.g., the concept of an enabled transition) are captured in the template, and a notation's distinct semantics (e.g., which states can enable transitions) are specified as parameters. The template semantics of composition operators define how multiple HTSs execute concurrently and how they communicate and synchronize with each other by exchanging events and data. The definitions of these operators use the template parameters to preserve notation-specific behavior in composition. Our template is sufficient to capture the semantics of basic transition systems, CSP, CCS, basic LOTOS, a subset of SDL88, and a variety of statecharts notations. We believe that a description of a notation's semantics using our template can be used as input to a tool that automatically generates formal analysis tools.

[1] P. Alexander and C. Kong, "Rosetta: Semantic Support for Model Centered Systems Level Design," Computer, vol. 34, no. 11, Nov. 2001, pp. 64-70.
[2] J.M. Atlee and J. Gannon, "State-Based Model Checking of Event-Driven System Requirements," IEEE Trans. Software Eng., vol. 19, no. 1, pp. 24-40, Jan. 1993.
[3] G. Avrunin, J. Corbett, and L. Dillon, Analyzing Partially-Implemented Real-Time Systems Proc. Int'l Conf. Software Eng., pp. 228-238, 1997.
[4] S. Bensalem et al., An Overview of SAL Proc. Langley Formal Methods Workshop, pp. 187-196, 2000.
[5] G. Berry and G. Gonthier, The Synchronous Programming Language ESTEREL: Design, Semantics, Implementation Science of Computer Programming, vol. 19, no. 2, pp. 87-152, 1992.
[6] L. Blair and G. Blair, Composition in Multi-Paradigm Specification Techniques Proc. Int'l Workshop Formal Methods for Open Object-based Distributed Systems, pp. 401-417, 1999.
[7] M. Bozga, J.-C. Fernandez, L. Ghirvu, S. Graf, J. Krimm, L. Mounier, and J. Sifakis, IF: An Intermediate Representation for SDL and Its Applications Proc. SDL-Forum '99, pp. 423-440, 1999.
[8] T. Bultan, Action Language: A Specification Language for Model Checking Reactive Systems Proc. Int'l Conf. Software Eng., pp. 335-344, 2000.
[9] W. Chan, R.J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J.D. Reese, "Model Checking Large Software Specifications," IEEE Trans. Software Eng., vol. 24, no. 7, July 1998.
[10] P. Chou and G. Borriello, "An Analysis-Based Approach to Composition of Distributed Embedded Systems," Proc. Int'l Work. Hardware-Software Codesign, IEEE CS Press, 1998.
[11] R. Cleaveland, J. Parrow, and B. Steffen, The Concurrency Workbench: A Semantics-Based Tool for the Verification of Concurrent Systems ACM Trans. Programming Languages and Systems, vol. 15, no. 1, pp. 36-72, 1993.
[12] R. Cleaveland and S. Sims, Generic Tools for Verifying Concurrent Systems Science of Computer Programming, vol. 41, no. 1, pp. 39-47, Jan. 2002.
[13] N.A. Day and J.J. Joyce, Symbolic Functional Evaluation Proc. 12th Int'l Conf. Theorem Proving in Higher Order Logics, Sept. 1999.
[14] P. Degano and C. Priami, Enhanced Operational Semantics: A Tool for Describing and Analyzing Concurrent Systems ACM Computing Surveys, vol. 33, no. 2, pp. 135-176, 2001.
[15] L. Dillon and R. Stirewalt, Inference Graphs: A Computational Structure Supporting Generation of Customizable and Correct Analysis Components IEEE Trans. Software Eng., vol. 29, no. 2, pp. 133-150, Feb. 2003.
[16] D. Harel et al., On the Formal Semantics of Statecharts Proc. Symp. Logic in Computer Science, pp. 54-64, 1987.
[17] D. Harel and A. Naamad, The Statemate Semantics of Statecharts ACM Trans. Software Eng. Methods, vol. 5, no. 4, pp. 293-333, 1996.
[18] C.L. Heitmeyer, R.D. Jeffords, and B.G. Labaw, Automated Consistency Checking of Requirements Specifications ACM Trans. Software Eng. Methods, vol. 5, no. 3, pp. 231-261, 1996.
[19] C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall, 1985.
[20] International Organization for Standardization, LOTOS A Formal Description Technique Based on the Temporal Ordering of Observational Behavior Technical Report ISO8807, 1988.
[21] International Telecommunications Union, Recommendation Z.100. Specification and Description Language (SDL)} Technical Report Z-100, Standardization Sector, 1999.
[22] N.C. Levenson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, "Requirements Specification for Process-Control Systems," IEEE Trans. Software Eng., vol. 20, no. 9, pp. 684-707, Sept. 1994.
[23] A. Maggiolo-Schettini, A. Peron, and S. Tini, Equivalences of Statecharts Proc. Int'l Conf. Concurrency Theory, 1996.
[24] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1991.
[25] K. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, 1993.
[26] E. Mikk, Y. Lakhnech, and M. Siegel, Hierarchical Automata as Model for Statecharts Proc. Asian Computer Science Conf., 1997.
[27] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[28] J. Niu, J.M. Atlee, and N.A. Day, Composable Semantics for Model-Based Notations Proc. Int'l Symp. Foundations of Software Eng. (FSE-10), pp. 149-158, 2002.
[29] J. Niu, J.M. Atlee, and N.A. Day, Understanding and Comparing Model-Based Soecification Notations Proc. IEEE Int'l Requirements Eng. Conf., pp. 188-199, 2003.
[30] Object Management Group, Unified Modelling Language (UML), version 1.4, 2001, www.omg.org.
[31] S. Owre, J. Rushby, and N. Shankar, Analyzing Tabular and State-Transition Requirements Specifications in PVS Technical Report CSL-95-12, SRI Int'l, Computer Science Laborabory, 1995.
[32] J.L. Peterson, Petri Nets ACM Computing Surveys, vol. 9, no. 3, pp. 223-252, 1977.
[33] M. Pezzè and M. Young, Constructing Multi-Formalism State-Space Analysis Tools Proc. Int'l Conf. Software Eng., pp. 239-249, 1997.
[34] A. Pnueli and M. Shalev, What is in a Step: On the Semantics of Statecharts Proc. Symp. Theoretical Aspects of Computer Software, 1991.
[35] M. von der Beeck, A Comparison of Statecharts Variants Formal Techniques in Real Time and Fault-Tolerant Systems, 1994.
[36] P. Zave and M. Jackson, Conjunction as Composition ACM Trans. Software Eng. Methods, vol. 2, no. 4, pp. 379-411, 1993.

Index Terms:
Model-based specification notations, semantics, composition, concurrency, automated generation of analysis tools.
Citation:
Jianwei Niu, Joanne M. Atlee, Nancy A. Day, "Template Semantics for Model-Based Notations," IEEE Transactions on Software Engineering, vol. 29, no. 10, pp. 866-882, Oct. 2003, doi:10.1109/TSE.2003.1237169
Usage of this product signifies your acceptance of the Terms of Use.