From Partial to Global Assume-Guarantee Contracts: Compositional Realizability Analysis in FRET

Realizability checking refers to the formal procedure that aims to determine whether an implementation exists, always complying to a set of requirements, regardless of the stimuli provided by the system's environment. Such a check is essential to ensure that the specification does not allow behavior that can force the system to violate safety constraints. In this paper, we present an approach that decomposes realizability checking into smaller, more tractable problems. More specifically, our approach automatically partitions specifications into sets of non-interfering requirements. We prove that checking whether a specification is realizable reduces to checking that each partition is realizable. We have integrated realizability checking and implemented our decomposition approach within the open-source Formal Requirements Elicitation Tool (FRET). A FRET user may check the realizability of a specification monolithically or compositionally. We evaluate our approach by comparing monolithic and compositional checking and showcase the strengths of our decomposition approach on a variety of industrial-level case studies.