Abstract
We describe the COMPASS Modelling Language (CML), which is used to model large-scale Systems of Systems and the contracts that bind them together. The language can be used to document the interfaces to constituent systems using formal, precise, and verifiable specifications including preconditions, postconditions, and invariants. The semantics of CML directly supports the use of these contracts for all language constructs, including the use of communication channels, parallel processes, and processes that run forever. Every process construct in CML has an associated contract, allowing clients and suppliers to check that the implementations of constituent systems conform to their interface specifications.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Andrews, Z., Fitzgerald, J., Payne, R., Romanovsky, A.: Fault Modelling for Systems of Systems. In: Proceedings of the 11th International Symposium on Autonomous Decentralised Systems (ISADS 2013), pp. 59–66 (March 2013)
Beg, A., Butterfield, A.: Linking a state-rich process algebra to a state-free algebra to verify software/hardware implementation. In: FIT 2010, 8th Intl Conf. on Frontiers of Information Technology, Islamabad, p. 47. ACM (2010)
Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. In: White, J., Lipton, R.J., Goldberg, P.C. (eds.) 8th Ann. ACM Symp. on Principles of Programming Languages, Williamsburg, pp. 164–176. ACM Press (1981)
Bryans, J., Fitzgerald, J., Payne, R., Kristensen, K.: Maintaining emergence in systems of systems integration: a contractual approach using SysML. In: INCOSE International Symposium (to appear, 2014)
Bryans, J., Fitzgerald, J., Payne, R., Miyazawa, A., Kristensen, K.: SysML Contracts for Systems of Systems. In: 9th Intl Conf. on Systems of Systems Engineering (SoSE). IEEE (June 2014)
Butler, M., Yadav, D.: An incremental development of the Mondex system in Event-B. Formal Asp. Comput. 20(1), 61–77 (2008)
Cavalcanti, A., Sampaio, A., Woodcock, J.: Unifying classes and processes. Software and System Modeling 4(3), 277–296 (2005)
Cavalcanti, A., Wellings, A., Woodcock, J.: The Safety-Critical Java memory model: A formal account. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 246–261. Springer, Heidelberg (2011)
Cavalcanti, A., Wellings, A.J., Woodcock, J.: The Safety-Critical Java memory model formalised. Formal Asp. Comput. 25(1), 37–57 (2013)
Cavalcanti, A., Wellings, A.J., Woodcock, J., Wei, K., Zeyda, F.: Safety-critical Java in Circus. In: Wellings, A.J., Ravn, A.P. (eds.) The 9th Intl Workshop on Java Technologies for Real-time and Embedded Systems, JTRES 2011, York, pp. 20–29. ACM (2011)
Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006)
Couto, L., Foster, S., Payne, R.: Towards verification of constituent systems through automated proof. In: Proc. Workshop on Engineering Dependable Systems of Systems (EDSoS). ACM CoRR (2014)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press (2002)
Dawes, J.: The VDM-SL Reference Guide. Pitman (1991) ISBN 0-273-03151-1
de Boer, F.S., Hannemann, U., de Roever, W.-P.: Hoare-style compositional proof systems for reactive shared variable concurrency. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol. 1346, pp. 267–283. Springer, Heidelberg (1997)
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs for Object-oriented Systems. Springer (2005)
Fitzgerald, J., Larsen, P.G., Woodcock, J.: Foundations for Model-based Engineering of Systems of Systems. In: Aiguier, M., et al. (eds.) Complex Systems Design and Management, pp. 1–19. Springer (January 2014)
Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: A mechanised theory engineering framework. In: 5th International Symposium on Unifying Theories of Programming (to appear, 2014)
Freitas, L., Woodcock, J.: Mechanising Mondex with Z/Eves. Formal Asp. Comput. 20(1), 117–139 (2008)
George, C., Haxthausen, A.E.: Specification, proof, and model checking of the Mondex electronic purse using RAISE. Formal Asp. Comput. 20(1), 101–116 (2008)
Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — A modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014)
Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Formal Asp. Comput. 20(1), 41–59 (2008)
Hehner, E.C.R.: Retrospective and prospective for Unifying Theories of Programming. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 1–17. Springer, Heidelberg (2006)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall (1998)
ITSEC. Information Technology Security Evaluation Criteria (ITSEC): Preliminary harmonised criteria. Technical Report Document COM(90) 314, Version 1.2, Commission of the European Communities (1991)
Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)
Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall International (1990)
Kopetz, H.: System-of-Systems complexity. In: Proc. 1st Workshop on Advances in Systems of Systems, pp. 35–39 (2013)
Kuhlmann, M., Gogolla, M.: Modeling and validating Mondex scenarios described in UML and OCL with USE. Formal Asp. Comput. 20(1), 79–100 (2008)
Liu, Y., Sun, J., Dong, J.S.: PAT 3: An extensible architecture for building multi-domain model checkers. In: Dohi, T., Cukic, B. (eds.) IEEE 22nd Intl Symp. on Software Reliability Engineering, ISSRE 2011, Hiroshima, pp. 190–199. IEEE (2011)
Lowe, G.: Specification of communicating processes: temporal logic versus refusals-based refinement. Formal Asp. Comput. 20(3), 277–294 (2008)
Meyer, B.: Applying ”design by contract”. IEEE Computer 25(10), 40–51 (1992)
Mota, A., Farias, A., Didier, A., Woodcock, J.: Rapid prototyping of a semantically well founded Circus model checker. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 235–249. Springer, Heidelberg (2014)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A denotational semantics for Circus. Electr. Notes Theor. Comput. Sci. 187, 107–123 (2007)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Asp. Comput. 21(1-2), 3–32 (2009)
Oliveira, M., Gurgel, A.C., Castro, C.G.: CRefine: Support for the Circus refinement calculus. In: 6th Intl. Conf. on Software Engineering and Formal Methods (SEFM 2008), pp. 281–290. IEEE Computer Society (November 2008)
Parnas, D.L.: Really rethinking ‘formal methods’. IEEE Computer 43(1), 28–34 (2010)
Perna, J.I., Woodcock, J.: Mechanised wire-wise verification of Handel-C synthesis. Sci. Comput. Program. 77(4), 424–443 (2012)
Perna, J.I., Woodcock, J., Sampaio, A., Iyoda, J.: Correct hardware synthesis—an algebraic approach. Acta Inf. 48(7-8), 363–396 (2011)
Ramananandro, T.: Mondex, an electronic purse: specification and refinement checks with the Alloy model-finding method. Formal Asp. Comput. 20(1), 21–39 (2008)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall International (1997)
Roscoe, A.W.: On the expressive power of CSP refinement. Formal Asp. Comput. 17(2), 93–112 (2005)
Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in Unifying Theories of Programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Heidelberg (2004)
Woodcock, J., Cavalcanti, A., Fitzgerald, J.S., Larsen, P.G., Miyazawa, A., Perry, S.: Features of CML: A formal modelling language for systems of systems. In: 7th Intl Conf. on Systems of Systems Engineering, SoSE 2012, Genova, pp. 445–450. IEEE (2012)
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice-Hall, Inc. (1996)
Woodcock, J., Stepney, S., Cooper, D., Clark, J.A., Jacob, J.: The certification of the Mondex electronic purse to ITSEC Level E6. Formal Asp. Comput. 20(1), 5–19 (2008)
Zhan, N., Kang, E.Y., Liu, Z.: Component publications and compositions. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 238–257. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Woodcock, J., Cavalcanti, A., Fitzgerald, J., Foster, S., Larsen, P.G. (2014). Contracts in CML. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. ISoLA 2014. Lecture Notes in Computer Science, vol 8803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45231-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-662-45231-8_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45230-1
Online ISBN: 978-3-662-45231-8
eBook Packages: Computer ScienceComputer Science (R0)