×

zbMATH — the first resource for mathematics

Unifying theories of reactive design contracts. (English) Zbl 1436.68195
Summary: Design-by-contract is an important technique for model-based design in which a composite system is specified by a collection of contracts that specify the behavioural assumptions and guarantees of each component. In this paper, we describe a unifying theory for reactive design contracts that provides the basis for modelling and verification of reactive systems. We provide a language for expression and composition of contracts that is supported by a rich calculational theory. In contrast with other semantic models in the literature, our theory of contracts allows us to specify both the evolution of state variables and the permissible interactions with the environment. Moreover, our model of interaction is abstract, and supports, for instance, discrete time, continuous time, and hybrid computational models. Being based in Unifying Theories of Programming (UTP), our theory can be composed with further computational theories to support semantics for multi-paradigm languages. Practical reasoning support is provided via our proof framework, Isabelle/UTP, including a proof tactic that reduces a conjecture about a reactive program to three predicates, symbolically characterising its assumptions and guarantees about intermediate and final observations. This allows us to verify programs with a large or infinite state space. Our work advances the state-of-the-art in semantics for reactive languages, description of their contractual specifications, and compositional verification.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Armstrong, A.; Gomes, V.; Struth, G., Building program construction and verification tools from algebraic principles, Form. Asp. Comput., 28, 2, 265-293 (2015) · Zbl 1342.68066
[2] Back, R. J.; Wright, J., Refinement Calculus: A Systematic Introduction (1998), Springer · Zbl 0949.68094
[3] Bauer, S.; David, A.; Hennicker, R.; Larsen, K.; Legay, A.; Nyman, U.; Wasowski, A., Moving from specifications to contracts in component-based design, (Proc. 15th Intl. Conf. on Fundamental Approaches to Software Engineering (FASE). Proc. 15th Intl. Conf. on Fundamental Approaches to Software Engineering (FASE), LNCS, vol. 7212 (2012), Springer), 43-58
[4] Benveniste, A.; Caillaud, B.; Ferrari, A.; Mangeruca, L.; Passerone, R.; Sofronis, C., Multiple viewpoint contract-based specification and design, (6th Intl. Symp. on Formal Methods for Components and Objects (FMCO). 6th Intl. Symp. on Formal Methods for Components and Objects (FMCO), LNCS, vol. 5382 (2007), Springer), 200-225 · Zbl 1209.68120
[5] Benvenuti, L.; Ferrari, A.; Mangeruca, L.; Mazzi, E.; Passerone, R.; Sofronis, C., A contract-based formalism for the specification of heterogeneous systems, (Proc. Forum on Specification, Verification, and Design Languages (FDL) (2008)), 142-147
[6] Blanchette, J. C.; Bulwahn, L.; Nipkow, T., Automatic proof and disproof in Isabelle/HOL, (FroCoS. FroCoS, LNCS, vol. 6989 (2011), Springer), 12-27 · Zbl 1348.68214
[7] Butterfield, A.; Gancarski, P.; Woodcock, J., State visibility and communication in unifying theories of programming, (Proc. 3rd Intl. Symp on Theoretical Aspects of Software Engineering (TASE) (2009), IEEE), 47-54
[8] Canham, S.; Woodcock, J., Three approaches to timed external choice in UTP, (Proc. 5th Intl. Symp. on Unifying Theories of Programming (UTP). Proc. 5th Intl. Symp. on Unifying Theories of Programming (UTP), LNCS, vol. 8963 (2015), Springer), 1-20 · Zbl 1457.68059
[9] Cavalcanti, A.; Woodcock, J., A tutorial introduction to designs in unifying theories of programming, (Proc. 4th Intl. Conf. on Integrated Formal Methods (IFM). Proc. 4th Intl. Conf. on Integrated Formal Methods (IFM), LNCS, vol. 2999 (2004), Springer), 40-66 · Zbl 1196.68031
[10] Cavalcanti, A.; Woodcock, J., A Tutorial Introduction to CSP in Unifying Theories of Programming, Refinement Techniques in Software Engineering, LNCS, vol. 3167, 220-268 (2006), Springer
[11] Cimatti, A.; Tonetta, S., A property-based proof system for contract-based design, (38th. Conf. on Software Engineering and Advanced Applications (SEAA) (2012), IEEE), 21-28
[12] Colvin, R. J.; Hayes, I. J.; Meinicke, L. A., Designing a semantic model for a wide-spectrum language with concurrency, Form. Asp. Comput., 29, 5 (2017) · Zbl 1375.68036
[13] Coquand, T., Infinite objects in type theory, (Proc. 1st Intl. Workshop on Types for Proofs and Programs. Proc. 1st Intl. Workshop on Types for Proofs and Programs, LNCS, vol. 806 (1993), Springer), 62-78
[14] Dijkstra, E. W., Guarded commands, nondeterminacy and formal derivation of programs, Commun. ACM, 18, 8, 453-457 (1975) · Zbl 0308.68017
[15] Floyd, R. W., Assigning Meanings to Programs, Proc. Symp. in Applied Science, Mathematical Aspects of Computer Science, vol. 19, 19-32 (1967), American Mathematical Society · Zbl 0189.50204
[16] Foster, S.; Cavalcanti, A.; Woodcock, J.; Zeyda, F., Unifying theories of time with generalised reactive processes, Inf. Process. Lett., 135, 47-52 (2018) · Zbl 06856068
[17] Foster, S.; Thiele, B.; Cavalcanti, A.; Woodcock, J., Towards a UTP semantics for Modelica, (Proc. 6th Intl. Symp. on Unifying Theories of Programming (UTP). Proc. 6th Intl. Symp. on Unifying Theories of Programming (UTP), LNCS, vol. 10134 (2016), Springer) · Zbl 06700457
[18] Foster, S.; Zeyda, F.; Woodcock, J., Isabelle/UTP: a mechanised theory engineering framework, (Proc. 5th Intl. Symp. on Unifying Theories of Programming (UTP). Proc. 5th Intl. Symp. on Unifying Theories of Programming (UTP), LNCS, vol. 8963 (2014), Springer), 21-41 · Zbl 1457.68061
[19] Foster, S.; Zeyda, F.; Woodcock, J.; Nemouchi, Y.; Ribeiro, P.; Wolff, B., Isabelle/UTP: Mechanised theory engineering for unifying theories of programming (2019), Archive of Formal Proofs
[20] Foster, S.; Zeyda, F.; Woodcock, J., Unifying heterogeneous state-spaces with lenses, (Proc. 13th Intl. Conf. on Theoretical Aspects of Computing (ICTAC). Proc. 13th Intl. Conf. on Theoretical Aspects of Computing (ICTAC), LNCS, vol. 9965 (2016), Springer) · Zbl 06667713
[21] Gomes, V. B.F.; Struth, G., Modal Kleene algebra applied to program correctness, (21st. Intl. Symp. on Formal Methods (FM). 21st. Intl. Symp. on Formal Methods (FM), LNCS, vol. 9995 (2016), Springer), 310-325
[22] Guttman, W.; Möller, B., Normal design algebra, J. Log. Algebraic Program., 79, 2, 144-173 (2010) · Zbl 1184.68179
[23] Hayes, I. J., Generalised rely-guarantee concurrency: an algebraic foundation, Form. Asp. Comput., 28, 6, 1057-1078 (2016) · Zbl 1348.68035
[24] Hayes, I. J.; Colvin, R. J.; Meinecke, L. A.; Winter, K.; Velykis, A., An algebra of synchronous atomic steps, (Proc. 21st Intl. Symp. on Formal Methods (FM). Proc. 21st Intl. Symp. on Formal Methods (FM), LNCS, vol. 9995 (2016), Springer), 352-369
[25] He, J., From CSP to hybrid systems, (Roscoe, A. W., A Classical Mind: Essays in Honour of C. A. R. Hoare (1994), Prentice Hall), 171-189
[26] He, J.; Xiaoshan, L.; Zhiming, L., Component-based software engineering: the need to link methods and their theories, (Proc. 2nd Intl. Colloq. on Theoretical Aspects of Computing (ICTAC). Proc. 2nd Intl. Colloq. on Theoretical Aspects of Computing (ICTAC), LNCS, vol. 3722 (2005), Springer), 70-95
[27] He, J.; Xiaoshan, L.; Zhiming, L., rCOS: a refinement calculus of object systems, Theor. Comput. Sci., 365, 109-142 (2006) · Zbl 1118.68049
[28] Hehner, E. C.R., A Practical Theory of Programming (1993), Springer · Zbl 0793.68002
[29] Henkin, L.; Monk, J.; Tarski, A., Cylindric Algebras, Part I (1971), North-Holland · Zbl 0214.01302
[30] Hoare, C. A.R., An axiomatic basis for computer programming, Commun. ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105
[31] Hoare, C. A.R., Some properties of predicate transformers, J. ACM, 25, 3, 461-480 (1978) · Zbl 0379.68016
[32] Hoare, C. A.R., Communicating Sequential Processes (1985), Prentice-Hall · Zbl 0637.68007
[33] Hoare, C. A.R.; Hayes, I.; He, J.; Morgan, C.; Roscoe, A.; Sanders, J.; Sørensen, I.; Spivey, J.; Sufrin, B., The laws of programming, Commun. ACM, 30, 8, 672-687 (1987) · Zbl 0629.68006
[34] Hoare, C. A.R.; He, J., Unifying Theories of Programming (1998), Prentice-Hall
[35] Huffman, B.; Kunčar, O., Lifting and transfer: a modular design for quotients in Isabelle/HOL, (CPP. CPP, LNCS, vol. 8307 (2013), Springer), 131-146 · Zbl 1426.68284
[36] Jones, C. B., Development Methods for Computer Programs Including a Notion of Interference (1981), Oxford University, Ph.D. thesis
[37] Jones, C. B., Wanted: a compositional approach to concurrency, (Programming Methodology, Monographs in Computer Science (2003), Springer), 5-15
[38] von Karger, B., A calculational approach to reactive systems, Sci. Comput. Program., 37, 139-161 (2000) · Zbl 0954.68035
[39] von Karger, B.; Hoare, C. A.R., Sequential calculus, Inf. Process. Lett., 53, 123-130 (1995) · Zbl 0875.68202
[40] Lassez, J. L.; Nguyen, V. L.; Sonenberg, E. A., Fixed point theorems and semantics: a folk tale, Inf. Process. Lett., 14, 3, 112-116 (1982) · Zbl 0488.68015
[41] McEwan, A., Concurrent Program Development in Circus (2006), Oxford University, Ph.D. thesis
[42] Meyer, B., Eiffel: a language and environment for software engineering, J. Syst. Softw., 8, 3, 199-246 (1988)
[43] Meyer, B., Applying “design by contract”, IEEE Comput., 25, 10, 40-51 (1992)
[44] Morgan, C., Programming from Specifications (1996), Prentice-Hall
[45] Morris, J. M., A theoretical basis for stepwise refinement and the programming calculus, Sci. Comput. Program., 9, 3, 287-306 (1987) · Zbl 0624.68017
[46] Nipkow, T.; Wenzel, M.; Paulson, L. C., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283 (2002), Springer · Zbl 0994.68131
[47] Oliveira, M.; Cavalcanti, A.; Woodcock, J., A UTP semantics for Circus, Form. Asp. Comput., 21, 3-32 (2009) · Zbl 1165.68048
[48] Oliveira, M. V.M., Formal Derivation of State-Rich Reactive Programs Using Circus (2006), Department of Computer Science - University of York: Department of Computer Science - University of York UK, YCST-2006-02
[49] Roscoe, A. W., The Theory and Practice of Concurrency (2005), Prentice-Hall
[50] Roscoe, A. W.; Hoare, C. A.R., The laws of Occam programming, Theor. Comput. Sci., 60, 2, 177-229 (1988) · Zbl 0719.68039
[51] Sangiovanni-Vincentelli, A.; Damm, W.; Passerone, R., Taming Dr. Frankenstein: contract-based design for cyber-physical systems, Eur. J. Control, 3, 217-238 (2012) · Zbl 1264.93152
[52] Santos, T.; Cavalcanti, A.; Sampaio, A., Object-orientation in the UTP, (Dunne, S.; Stoddart, B., Proc. 1st Intl. Symp. on Unifying Theories of Programming (UTP). Proc. 1st Intl. Symp. on Unifying Theories of Programming (UTP), LNCS, vol. 4010 (2006), Springer), 20-38 · Zbl 1186.68091
[53] Scott, D., Continuous lattices, (Toposes, Algebraic Geometry and Logic. Toposes, Algebraic Geometry and Logic, LNM, vol. 274 (1971), Springer), 97-136
[54] Sherif, A.; Cavalcanti, A.; He, J.; Sampaio, A., A process algebraic framework for specification and validation of real-time systems, Form. Asp. Comput., 22, 2, 153-191 (2010) · Zbl 1214.68224
[55] Spivey, M., The Z-Notation - A Reference Manual (1989), Prentice Hall: Prentice Hall Englewood Cliffs, N.J. · Zbl 0777.68003
[56] Tarksi, A., A lattice-theoretical fixpoint theorem and its applications, Pac. J. Math., 5, 2, 285-309 (1955)
[57] Tarski, A., On the calculus of relations, J. Symb. Log., 6, 3, 73-89 (1941) · JFM 67.0973.02
[58] Tonetta, S.; Cimatti, A., Contracts-refinement proof system for component-based embedded systems, Sci. Comput. Program., 97, 333-348 (2015)
[59] Wei, K.; Woodcock, J.; Cavalcanti, A., Circus time with reactive designs, (Proc. 4th Intl. Symp. on Unifying Theories of Programming (UTP). Proc. 4th Intl. Symp. on Unifying Theories of Programming (UTP), LNCS, vol. 7681 (2013), Springer), 68-87 · Zbl 1452.68057
[60] Woodcock, J., The miracle of reactive programming, (Proc. 2nd Intl. Symp. on Unifying Theories of Programming (UTP). Proc. 2nd Intl. Symp. on Unifying Theories of Programming (UTP), LNCS, vol. 5713 (2008), Springer), 202-217 · Zbl 1286.68096
[61] Woodcock, J., Engineering UToPiA - formal semantics for CML, (Jones, C.; Pihlajasaari, P.; Sun, J., FM 2014: Formal Methods. FM 2014: Formal Methods, LNCS, vol. 8442 (2014), Springer), 22-41
[62] Woodcock, J.; Cavalcanti, A., A concurrent language for refinement, (Butterfield, A.; Strong, G.; Pahl, C., Proc. 5th Irish Workshop on Formal Methods (IWFM), Workshops in Computing (2001), BCS)
[63] Woodcock, J.; Cavalcanti, A.; Fitzgerald, J.; Foster, S.; Larsen, P. G., Contracts in CML, (ISoLA 2014, Part II. ISoLA 2014, Part II, LNCS, vol. 8803 (2014), Springer), 54-73
[64] Zeyda, F.; Foster, S.; Freitas, L., An axiomatic value model for Isabelle/UTP, (Proc. 6th Intl. Symp. on Unifying Theories of Programming. Proc. 6th Intl. Symp. on Unifying Theories of Programming, LNCS, vol. 5713 (2014), Springer), 155-175 · Zbl 06700462
[65] Zhan, N.; Kang, E. Y.; Liu, Z., Component publications and compositions, (2nd Intl. Symp. on Unifying Theories of Programming (UTP). 2nd Intl. Symp. on Unifying Theories of Programming (UTP), LNCS, vol. 5713 (2008), Springer), 238-257 · Zbl 1286.68098
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.