Efficient methods to combine timed system contracts for safety design
Computing GR(1) Assume-Guarantee Contracts
Logic in Computer Science
Summary
Designing complex systems often means combining lots of rules about how components assume things about each other and guarantee behaviors. Existing methods only worked well when time wasn’t considered. The authors developed new math and algorithms to handle these assume-and-guarantee contracts when time matters, specifically using a type of logic called GR(1). They built tools that automatically work out how different parts fit together and tested this on emergency braking systems, showing how to spot if parts will work safely together.
What this means in practice
- •For embedded system engineers: Calculate timing-aware compatibility conditions between components to ensure safety-critical systems meet overall requirements before integration.
- •For automotive control developers: Derive system-level control contracts automatically from component specifications to improve design confidence in safety features like automated emergency braking.
Authors
Yigit Narter, Emily Zhao, Inigo Incer
Abstract
Assume-guarantee contracts provide a set of algebraic operations that enable the efficient compositional design and analysis of complex engineering systems. The explicit computation of these operations at component interfaces is currently supported only for some logics lacking a notion of time. This paper develops theory and algorithms to compute these operations when the contracts are expressed in the GR(1) modulo theory. The key challenge is the computation of two quantifier elimination problems for temporal formulas. We develop context-aided variable elimination procedures on GR(1)-modulo formulas, establish their soundness, characterize subproblem-wise optimal solutions within an admissible class of formulas, and use the procedures to compute contract operations, including composition and quotient. We implement the resulting framework in Pacti, automating compositional reasoning over GR(1) contracts. Finally, we demonstrate the framework on an automated emergency-braking case study, where we compute system-level contracts and expose compatibility conditions arising from the interaction of component specifications. Experiments on synthetic families show that the cost is governed by the number of eliminated variables and liveness conjuncts, and a comparison with exact automata-based elimination shows complementary scaling.