Abstract
The requirements capture of complex systems requires powerful mechanisms for specifying system state, structure and interactive behaviors. Integrated formal specification languages are well suited for presenting more complete and coherent requirement models for complex systems. Given an integrated model, one can project it into multiple views for specialized analysis. Message Sequence Charts (MSCs) is a popular graphical notation for presenting interactive viewpoints of a system. In this paper, we investigate the semantic based transformation from an integrated formal specification language TCOZ to MSCs. An automated tool has also been developed for generating MSCs from TCOZ models. Furthermore, by inserting operation constraints (as assertions) into the generated MSCs, system testing requirements can be obtained.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science 18(1) (1990)
Bolton, C., Davies, J.: Activity Graphs and Processes. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 77–96. Springer, Heidelberg (2000)
Bowman, H., Steen, M.W.A., Boiten, E.A., Derrick, J.: A Formal Framework for Viewpoint Consistency. Formal Methods in System Design 21, 111–166 (2002)
Brooke, P.J., Paige, R.F.: The Design of a Tool-Supported Graphical Notation for Timed CSP. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol. 2335, Springer, Heidelberg (2002)
Butler, M.: csp2B: A Practical Approach To Combining CSP and B. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, Springer, Heidelberg (1999)
Chen, C.-A., Kalvala, S., Sinclair, J.: Generating b specifications from message sequence charts. In: St.Eve Workshop (September 2003)
Coombes, A., McDermid, J.A.: Using Diagrams to Give a Formal Specification of Timing Constraints in Z. In: Z User Workshop, pp. 119–130 (1992)
Davies, J., Crichton, C.: Using State Diagrams to Describe Concurrent Behaviour. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 105–124. Springer, Heidelberg (2003)
Davies, J., Schneider, S.: A Brief History of Timed CSP. Theoretical Computer Science 138 (1995)
Dias, M.S., Richardson, D.J.: Identifying Cause and Effect Relations between Events in Concurrent Event-Based Componenents. In: Richardson, J., Emmerich, W., Wile, D. (eds.) The 17th IEEE International Conference on Automated Software Engineering (ASE 2002) (2002)
Duke, R., Rose, G.: Formal Object Oriented Specification Using Object-Z, March 2000. Cornerstones of Computing Series. Macmillan, Basingstoke (2000)
Feldmann, R.L., Munch, J., Queins, S., Vorwieger, S., Zimmermann, G.: Baselining a Doman-Specific Software Development Process. Tech Report SFB501 TR- 02/99, University of Kaiserslautern (1999)
Fischer, C., Wehrheim, H.: Model-Checking CSP-OZ Specifications with FDR. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM 1999: Integrated Formal Methods, York, UK, June 1999, Springer, Heidelberg (1999)
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1985)
ITU. Message Sequence Chart(MSC), Series Z: Languages and general software aspects for telecommunication systems (Novomber 1999)
Liu, S., Jeff Offutt, A., Ho-Stuart, C., Sun, Y., Ohba, M.: A formal engineering methodology for industrial applications, pp. 24–45 (1998)
Mahony, B., Dong, J.S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering 26(2), 150–177 (2000)
Mahony, B., Dong, J.S.: Deep Semantic Links of TCSP and Object-Z: TCOZ Approach. Formal Aspects of Computing 13(2), 142–160 (2002)
Mahony, B., Dong, J.S.: Deep Semantic Links of TCSP and Object-Z: TCOZ Approach. Formal Aspects of Computing 13(1), 142–160 (2002)
Ng, M.Y., Butler, M.: Tool Support for Visualizing CSP in UML. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 287–298. Springer, Heidelberg (2002)
Nuseibeh, B., Kramer, J., Finkelstein, A.: A Framework for Expressing the Relationships Between Multiple Views in Requirement Specifications. IEEE Trans. Software Eng. 20(10), 760–773 (1994)
Petre, L., Sere, K.: Developing Control Systems Components. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, p. 156. Springer, Heidelberg (2000)
Richardson, D.J., Aha, S.L., O’Malley, T.O.: Specification-Based Test Oracles for Reactive Systems. International Conference on Software Engineering, 105–118 (1992)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)
Smith, G.: The Object-Z Specification Language. Advances in Formal Methods. Kluwer Academic Publishers, Dordrecht (2000)
Smith, G., Derrick, J.: Specification, Refinement and Verification of Concurrent Systems - an Integration of Object-Z and CSP. Formal Methods in System Design 18, 249–284 (2001)
Stocks, P., Carrington, D.: A Framework for Specification-based Testing. IEEE Trans. Software Eng. 22(11), 777–793 (1996)
Sun, J., Dong, J.S., Liu, J., Wang, H.: A Formal Object Approach to the Design of ZML. Annals of Software Engineering 13, 329–356 (2002)
Taguchi, K., Araki, K.: The State-Based CCS Semantics for Concurrent Z Specification. In: Hinchey, M., Liu, S. (eds.) The IEEE International Conference on Formal Engineering Methods (ICFEM 1997), Hiroshima, Japan, November 1997, pp. 283–292. IEEE Press, Los Alamitos (1997)
Treharne, H., Schneider, S.: Using a Process Algebra to Control B Operations. In: Araki, K., Galloway, A., Taguchi, K. (eds.) IFM 1999: Integrated Formal Methods, York, UK, June 1999, Springer, Heidelberg (1999)
van Hee, K.M.: Information Systems Engineering: A Formal Approach. Cambridge University Press, Cambridge (1994)
Woodcock, J., Cavalcanti, A.: The Steam Boiler in a Unified Theory of Z and CSP. In: He, J., Li, Y., Lowe, G. (eds.) The 8th Asia-Pacific Software Engineering Conference (APSEC 2001), pp. 291–298. IEEE Press, Los Alamitos (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dong, J.S., Qin, S., Sun, J. (2004). Generating MSCs from an Integrated Formal Specification Language. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-24756-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21377-2
Online ISBN: 978-3-540-24756-2
eBook Packages: Springer Book Archive