Composing Specifications Given in Different Formalisms

Abstract: The field of contract theory is concerned with formal proofs of how smaller components may be composed into larger systems. This thesis shows how one framework for constructing such proofs may be used to prove properties of compositions where some components are specified using the TLA+ formalism. This is done by showing an equivalence between a TLA+ formula and an assume-guarantee contract and then carrying out a proof of compositionality utilizing the assume-guarantee contract. The components that are specified are part of a toy system previously specified in an earlier work, from where the bulk of the specifications used in the proof is taken. Furthermore, it is shown that any specification given in TLA+ is assertional, meaning that a composition with a component fulfilling such a specification preserves the component’s behavior.