Theory and methodology of assumption/commitment based system interface specification and architectural contracts.

*(English)*Zbl 1392.68238Summary: This paper addresses the specification of and reasoning about interactive real-time systems, their interfaces, and architectures as well as their properties in terms of assumptions and commitments. Specifications are structured into assumptions restricting the behavior of the operational context of systems and commitments about the system behavior (also called rely/guarantee or assumption/promise specification patterns in the literature). A logical approach to assumption/commitment contracts is worked out based on a mathematical system model:

- \(\bullet\)
- From assumption/commitment contracts plain interface assertions for the system are derived.
- \(\bullet\)
- Healthiness conditions based on the system model are worked out for assumptions.
- \(\bullet\)
- Safety and liveness properties for assumption/commitment contracts are identified.
- \(\bullet\)
- From interaction specifications describing the interaction between two systems assumption/commitment contracts for the involved systems are derived.
- \(\bullet\)
- Contracts for components in architectures are formulated in terms of assumptions and commitments and conditions are worked out to guarantee that assumptions for the composite systems guarantee the validity of the assumptions for components.

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68M07 | Mathematical problems of computer architecture |

68M14 | Distributed systems |

68M20 | Performance evaluation, queueing, and scheduling in the context of computer systems |

##### Keywords:

specification; design; contracts; assumptions; commitments; promises; context; system specification; safety; liveness; causality; realizability; interface; architecture
PDF
BibTeX
XML
Cite

\textit{M. Broy}, Form. Methods Syst. Des. 52, No. 1, 33--87 (2018; Zbl 1392.68238)

Full Text:
DOI

##### References:

[1] | Abadi, M; Plotkin, GD, A logical view of composition, Theor Comput Sci, 114, 3-30, (1993) · Zbl 0778.68061 |

[2] | Alur, R; Henzinger, T, No article title, Reactive modules. Form Methods Syst Des, 15, 7-48, (1999) |

[3] | Alpern, B; Schneider, FB, Recognizing safety and liveness, Distrib Comput, 2, 117, (1987) · Zbl 0641.68039 |

[4] | Banerjee A, Pal B, Das S, Kumar A, Dasgupta P (2006) Test generation games from formal specifications. In: Sentovich E (ed) Proceedings of the 43rd design automation conference, DAC 2006, San Francisco, CA, USA, July 24-28, ACM 2006, pp 827-832 |

[5] | Barnett M, Leino K. R. M, Schulte W (2004) The Spec# programming system: an overview. In: Construction and analysis of safe, secure and interoperable smart devices (CASSIS), volume 3362 of Lecture Notes in Computer Science, Springer, pp 49-69 |

[6] | Bauer S, David A, Hennicker R, Guldstrand Larsen K, Legay A, Nyman U, Wasowski A (2012) Moving from specifications to contracts in component-based design. In: Lara J, Zisman A (eds) Fundamental approaches to software Eng., ser. Lec. Notes in computer science, vol 7212. Springer, Berlin, Heidelberg, pp 43-58 |

[7] | Bauer, S; Hennicker, R; Legay, A, A meta-theory for component interfaces with contracts on ports, Sci Comput Program, 91, 70-89, (2014) |

[8] | Bensalem S, Bozga M, Sifakis J, Nguyen T.-H (2008) Compositional verification for component-based systems and application. In: Cha S, Choi J-Y, Kim M, Lee I, Viswanathan M (eds) Proceedings of the 6th international symposium on automated technology for verification and analysis (ATVA ’08), Springer-Verlag, Berlin, Heidelberg, pp 64-79 · Zbl 1183.68364 |

[9] | Benveniste A, Caillaud B, Ferrari A, Mangeruca L, Passerone R, Ch. Sofronis: Multiple viewpoint contract-based specification and design. In: Proceedings of the software technology concertation on formal methods for components and objects (FMCO’07), revised lectures, lecture notes in computer science, Vol 5382 |

[10] | Benveniste A, Caillaud B, Ferrari A, Mangeruca L, Passerone R, Sofronis C (2008) Multiple viewpoint contract-based specification and design. In: de Boer F, Bonsangue M, Graf S, de Roever W-P (eds) Formal methods for components and objects, ser. lecture notes in computer science, vol 5382. Springer, Berlin, Heidelberg, pp 200-225 · Zbl 1209.68120 |

[11] | Benveniste A, Caillaud B, Passerone R (2009) Multi-viewpoint state machines for rich component models. In Nicolescu G, Mosterman P (eds) Model-based design for embedded systems. Taylor & Francis, pp 487-518 |

[12] | Benveniste A, Caillaud B, Dejan Nickovic, Passerone R, Raclet J.-B, Reinkemeier P, Sangiovanni-Vincentelli A, Damm W, Henzinger T, Larsen K (2012) Contracts for system design. Rapport de Recherche RR-8147, INRIA (November) |

[13] | Bliudze S, Sifakis J (2007) The algebra of connectors: structuring interaction in bip. In: Proceedings of the 7th ACM&Amp; IEEE international conference on embedded software. EMSOFT ’07, New York, NY, USA, ACM, pp 11-20 · Zbl 1390.68031 |

[14] | Broy, M, A functional rephrasing of the assumption/commitment specification style, Form Methods Syst Des, 13, 87-119, (1998) |

[15] | Broy M (1998) Compositional refinement of interactive systems modelled by relations. In: de Roever W-P, Langmaack H, Pnueli A (eds) Compositionality: the significant difference. LNCS state of the art survey, lecture notes in computer science, vol 1536, pp 130-149 |

[16] | Broy M, Stølen K (2001) Specification and development of interactive systems: FOCUS on streams, interfaces, and refinement. Springer, Berlin · Zbl 0981.68115 |

[17] | Broy M (2003) Modelling Services and Layered Architectures. In: König H, Heiner M, Wolisz A (eds) Formal techniques for networked and distributed systems. Berlin 2003, lecture notes in computer science, vol 2767. Springer, pp 48-61 · Zbl 1279.68063 |

[18] | Broy M (2004) Service-oriented systems engineering: specification and design of services and layered architectures: The JanusApproach. In: Broy M, Grünbauer J, Harel D, Hoare H (eds) Engineering theories of software intensive systems, Marktoberdorf, 3-15 August Germany, NATO Science Series, II. Mathematics, Physics and Chemistry—Vol 195. Springer, S. pp 47-81 · Zbl 1242.68147 |

[19] | Broy, M; Krüger, I; Meisinger, M, A formal model of services, TOSEM ACM Trans Softw Eng Methodol, 16, 1, (2007) |

[20] | Broy M (2007) Interaction and realizability. In: van Leeuwen J, Italiona GF, van der Hoek W, Meinel C, Sack H, Plasil F (eds) SOFSEM 2007: theory and practice of computer science, lecture notes in computer science, vol 4362. Springer, pp 29-50 |

[21] | Broy, M, A logical basis for component-oriented software and systems engineering, Comput J, 53, 1758-1782, (2010) |

[22] | Broy, M, Computability and realizability for interactive computations, Inf Comput, 241, 277-301, (2015) · Zbl 1309.68064 |

[23] | Brunel J-Y, Natale MD, Ferrari A, Giusto P, Lavagno, L (2004) SoftContract: an assertion-based software development process that enables design-by-contract. In: Proceedings of the conference on design, automation and test in Europe (DATE04), pp 358-363 |

[24] | Burdy, L; Cheon, Y; Cok, DR; Ernst, MD; Kiniry, JR; Leavens, GT; Leino, KRM; Poll, E, An overview of JML tools and applications, STTT, 7, 212-232, (2005) |

[25] | Chandy KM, Misra J (1981) Proofs of networks of processes. IEEE Trans Softw Eng 7(4) · Zbl 0468.68030 |

[26] | Chilton, C; Jonsson, B; Kwiatkowska, M, An algebraic theory of interface automata, Theor Comput Sci, 549, 146-174, (2014) · Zbl 1360.68608 |

[27] | Chilton C, Jonsson B, Kwiatkowska M (2014) Compositional assume-guarantee reasoning for input/output component theories. Sci Comput Program 91(Part A):115-137 |

[28] | Cimatti A, Dorigatti M, Tonetta S (2013) Ocra: a tool for checking the refinement of temporal contracts. In: 2013 IEEE/ACM 28th international conference on automated software engineering (ASE), pp 702-705 |

[29] | Cimatti A, Tonetta S (2015) Contracts-refinement proof system for component-based embedded systems. Sci Comput Program 97(Part 3):333-348 |

[30] | Clements P, Bachmann F, Bass L, Garlan D, Ivers J, Little R, Nord R, Stafford J (2002) Documenting software architectures: views and beyond. The SEI Series in Software Engineering, Addison Wesley Professional, Series |

[31] | Cobleigh, JM; Avrunin, GS; Clarke, LA, Breaking up is hard to do: an evaluation of automated assume-guarantee reasoning, ACM Trans Softw Eng Methodol, 17, 1-52, (2008) |

[32] | Collette, P, Composition of assumption-commitment specifications in a UNITY style, Sci Comput Program, 23, 107-125, (1994) · Zbl 0830.68082 |

[33] | Dasgupta P Private Communication, Munich 2012 |

[34] | Derler P, Lee E. A, Tripakis S, Törngren M (2013) Cyber-physical system design contracts. In: Proceedings of the ACM/IEEE 4th international conference on cyber-physical systems (ICCPS ’13). ACM, New York, NY, USA, pp 109-118 |

[35] | de Alfaro L, Henzinger TA (2001) Interface theories for component-based design. In EMSOFT 01: Proceedings of the First international workshop on embedded software, lecture notes in computer science 2211, Springer-Verlag , pp 148-165 · Zbl 1050.68518 |

[36] | de Alfaro L, Henzinger TA (2005) Interface-based Design. In: Broy M, Grünbauer J, Harel D, Hoare CAR (eds) Engineering theories of software-intensive systems, NATO Science Series: Mathematics, Physics, and Chemistry, vol 195, Springer, pp 83-104 |

[37] | Dragomir I, Ober I, Percebois C (2013) Safety contracts for reactive timed systems (extended abstract). In: Action AFSEC, Journées GDR GPL, 02/04/2013-05/04/2013, Nancy France, pp 37-46, April 2013 |

[38] | Dragomir I, Ober I, Percebois C (2013) Integrating verifiable assume/guarantee contracts in UML/SysML. In: 6th international workshop on model based architecting and construction of embedded systems (ACES-MB), in conjunction with MODELS’13, 29/09/2013, Miami, USA. CEUR Workshop Proceedings, September 2013 |

[39] | de Roever WP (2001) Concurrency verification: introduction to compositional and noncompositional methods. Cambridge University Press, Cambridge · Zbl 1009.68020 |

[40] | Giese H (2000) Contract-based component system design. In: Thirty-third annual Hawaii international conference on system sciences (HICSS-33), Maui, IEEE Press |

[41] | Hayes IJ (2014) Towards structuring system specifications with time bands using layers of rely-guarantee conditions. In: Artho C, Ölveczky PC (eds) Formal techniques for safety-critical systems, vol 419 of communications in computer and information science, Springer, pp 1-2 |

[42] | Henzinger TA, Qadeer S, Rajamani SK, Taşıran S (1998) An assume-guarantee rule for checking simulation. In: Gopalakrishnan GC, Windley P (eds.) FMCAD 1998. LNCS, vol 1522. Springer, Heidelberg, pp 421-431 |

[43] | Henzinger TA, Qadeer S, Rajamani SK (2000) Decomposing refinement proofs using assume-guarantee reasoning. In: Proceedings of the international conference on computer-aided design (ICCAD), IEEE Computer Society Press, pp 245-252 |

[44] | Herzberg, D; Broy, M, Modeling layered distributed communication systems, Form Aspects Comput, 17, 1-18, (2005) · Zbl 1101.68383 |

[45] | Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM, pp 576-580 · Zbl 0179.23105 |

[46] | Iannopollo A, Nuzzo P, Tripakis S, Sangiovanni-Vincentelli AL (2014) Library-based scalable refinement checking for contract-based design. DATE pp 1-6 |

[47] | Jones CB (1983) Specification and design of (parallel) programs. In: Proceedings of F IFIP’83, North-Holland, pp 321-332 |

[48] | Josko B, Ma Q, Metzner A (2008) Designing embedded systems using heterogeneous rich components. Published and used by N COSE with permission 2008 |

[49] | Krüger I, Grosu R, Scholz P, Broy M (1999) From MSCs to statecharts. In: Proceedings of DIPES’98, Kluwer |

[50] | Leavens T, Cheon Y Design by contract with JML. ftp://ftp.cs.iastate.edu/pub/leavens /JML/jmldbc.pdf |

[51] | Meyer B (1988) Object-oriented software construction. Prentice Hall, New Jersey |

[52] | Meyer, B; Mandrioli, D (ed.); Meyer, B (ed.), Design by contract, 1-50, (1991), New Jersey |

[53] | Meyer B (1992) Applying “Design by Contract”. Comput (IEEE) 25(10):40-51 |

[54] | Neubeck P (2012) A probabilitistic theory of interactive systems. Dissertation, Technische Universität München · Zbl 0830.68082 |

[55] | Namjoshi, KS; Trefler, RJ, On the completeness of compositional reasoning. computer aided verification, Lect Notes Comput Sci, 1855, 139-153, (2000) · Zbl 0974.68127 |

[56] | Nuzzo P, Finn JB, Iannopollo A, Sangiovanni-Vincentelli AL (2014) Contract-based design of control protocols for safety-critical cyber-physical systems. In: DATE, pp 1-4 |

[57] | Nuzzo P, Iannopollo A, Tripakis S, Sangiovanni-Vincentelli A ( 2014) Are interface theories equivalent to contract theories? Proceedings international conference on formal methods and models for co-design (MEMOCODE), Oct. pp 104-113 |

[58] | Owicki, S; Gries, D, An axiomatic proof technique for parallel programs, Acta Informatica, 6, 319-340, (1976) · Zbl 0312.68011 |

[59] | Pandya PK (1990) Some comments on the assumption-commitment framework for compositional verification of distributed programs. In de Bakker JW, de Roever WP, Rozenberg G (eds) Lecture notes in computer science, vol 430. Springer, pp 622-640 |

[60] | Pandya, PK; Joseph, M, P-A logic-a compositional proof system for distributed programs, Distrib Comput, 5, 37-54, (1991) · Zbl 0723.68075 |

[61] | Raclet, J-B; Badouel, E; Benveniste, A; Caillaud, B; Legay, A; Passerone, R, A modal interface theory for component-based design, Fundam Inf, 108, 119-149, (2011) · Zbl 1242.68147 |

[62] | Reussner RH (2001) The use of parameterised contracts for architecturing systems with software components. In: Proceedings of the sixth international workshop on component-oriented programming |

[63] | Ruchkin I, de Niz D, Chaki S, Garlan D (2014) Contract-based integration of cyber-physical analyses. In: Proceedings of the 14th international conference on embedded software. EMSOFT ’14, New York, NY, USA, ACM 23:1-23:10 |

[64] | Sangiovanni-Vincentelli A, Damm W, Passerone R (2012) Taming Dr. Frankenstein: Contract-based design for cyber-physical systems. Eur J Control 18(3):217-238 · Zbl 1264.93152 |

[65] | Stark E (1985) A proof technique for rely/guarantee properties. In: Maheshwari SN (ed) FSTTCS 1985. LNCS 206. Springer, Heidelberg, pp 369-391 · Zbl 0585.68026 |

[66] | Soderberg A, Johansson R (2013) Safety contract based design of software components. In: 2013 IEEE international symposium on software reliability engineering workshops (ISSREW), pp 365-370 |

[67] | Soderberg A, Vedder B (2012) Composable safety-critical systems based on pre-certified software components. In: 2012 IEEE 23rd international symposium on software reliability engineering workshops (ISSREW), pp 343-348 |

[68] | Stølen K (1991) A method for the development of totally correct shared-state parallel program. In: Baeten JCM, Groote JF (eds) Proceedings of Concur’91, Lecture notes in computer science, vol 527. Springer Berlin, pp 510-552 |

[69] | Toerngren M, Tripakis S, Derler P, Lee E.A (2012) Design contracts for cyber-physical systems: making timing assumptions explicit. Technical Report UCB/EECS- 2012-191, EECS Department, University of California, Berkeley (Aug) |

[70] | Tripakis S, Lickly B, Henzinger TA, Lee EA (2009) On relational interfaces. In: Chakraborty S, Halbwachs N (eds) Proceedings of the 9th ACM/IEEE international conference on embedded software, EMSOFT 2009, Grenoble 2009, pp 67-76 |

[71] | Tripakis S, Lickly B, Tenzinger TA, Lee EA (2011) A theory of synchronous relational interfaces. ACM Trans Program Lang Syst 33(4): 14:1-14:41 |

[72] | Westmann J (2016) Specifying safety-critical heterogeneous systems using contracts theory. KTH, industrial engineering and management. Doctoral Thesis Stockholm, Sweden · Zbl 0641.68039 |

[73] | Zwiers J (1989) Compositionality, concurrency and partial correctness, vol 321. Lecture notes in computer science, Springer, Berlin · Zbl 0674.68011 |

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.