Decomposing Specifications Using the Quotient of Assume-Guarantee Contracts

Contracts have been proposed as a formal mechanism to support compositional design first for complex software (e.g., see [1] and references therein) and later for system design (e.g., see [2] and references therein). We embed our contribution on contracts in reuse-based, meet-in-the-middle design methodologies such as Platform-Based Design (e.g., see [3]). In these methodologies that are fairly common in industry, during the top-down phase, the specification for a system is decomposed into a set of refined specifications of sub-components, i.e., the high-level architecture of the design is determined. This step fits in a refinement driven process where higher-level specifications are mapped into lower level implementations. This decomposition is "guided" by the existence of a set of predefined components in a library, the bottom-up part of the methodology.

More formally, suppose a designer wishes to implement a system that satisfies a top-level specification T, and will use in this design a set of n components from a library with specifications F = (T_i)_i (for i = 1..n). If the composition of these n design elements refines the top-level specification T, the design assembled from the components satisfies the specification. However, if this is not the case, the designer must add at least one element to the library. In other words, the designer must identify a specification T_M such that its composition with the composition of (T_i)_i (for i = 1..n) refines T.

This problem corresponds to identifying the missing (unknown) component in a library (e.g., see [4] and references therein). In the language of contract-based design, we need to compute the contract quotient that guarantees that T_M is as "large" a specification as possible in the refinement order so that whoever is in charge of adding the element to the library has the maximum degree of freedom in its implementation. In industry, this problem is in general tackled heuristically. Our proposed notion of quotient for assume-guarantee contracts aims at finding a rigorous procedure for the determination of the largest specification of the missing component.

References

[1] B. Meyer, Touch of Class: Learning to Program Well Using Object Technology and Design by Contracts. Springer, Software Engineering, 2009.

[2] A. Benveniste, B. Caillaud, D. Nickovic, R. Passerone, J.-B. Raclet, P. Reinkemeier, A. Sangiovanni-Vincentelli, W. Damm, T. A. Henzinger, and K. G. Larsen, "Contracts for system design," Foundationsand Trends in Electronic Design Automation, vol. 12, no. 2-3, pp. 124-400, 2018.

[3] F. Balarin, M. D'Angelo, A. Davare, D. Densmore, T. Meyerowitz, R. Passerone, A. Pinto, A. Sangiovanni-Vincentelli, A. Simalatsar, Y. Watanabe, G. Yang, and Q. Zhu, Chapter 10. Platform-Based Design and Frameworks. Cham: CRC Press, 2009, pp. 259-322.

[4] T. Villa, N. Yevtushenko, R. Brayton, A. Mishchenko, A. Petrenko, and A. Sangiovanni-Vincentelli, The Unknown Component Problem: Theory and Applications. Springer, 2012.