Decomposing Formal Specifications Into Assume-Guarantee Contracts for Hierarchical System Design

Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a way that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct specifications for components that should implement a given specification when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. To identify these variables, we parametrize the information flow between components. The specifications are written in the Temporal Logic of Actions, TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We study whether GR(1) contracts exist in the presence of full information, and prove that memoryless GR(1) contracts that preserve safety do not always exist, whereas contracts in GR(1) with history-determined variables added do exist. We observe that timed stutter-invariant specifications of open-systems in general require GR(2) liveness properties for expressing them. We formalize a definition of realizability in TLA+, and define an operator for forming open-systems from closed-systems, based on a variant of the while-plus operator. The resulting open-system properties are realizable when expected to be. We compare stepwise implication operators from the literature, and establish relations between them, and examine the arity required for expressing these operators. We examine which symmetric combinations of stepwise implication and implementation kind avoid circular dependence, and show that only Moore components specified by strictly causal stepwise implication avoid circular dependence. The proposed approach relies on symbolic algorithms for computing specifications. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We implemented an algorithm for minimal covering over lattices originally proposed for two-level logic minimization. We formalized the computation of essential elements and cyclic core that is part of this algorithm, and machine-checked the proofs of safety properties using a proof assistant. Proofs supporting the thesis are organized as TLA+ modules in appendices.