Correct-by-construction requirement decomposition

TL;DR

The paper tackles the lack of rigorous top-down methods for decomposing high-level requirements in safety-critical systems. It introduces a semi-automated correct-by-construction decomposition framework that combines contract-based design with $reachability\ analysis$ and constraint programming, enabling sub-requirements to be represented as $continuous\ bounded\ sets$. The framework defines relational and functional contracts, refinement, and IO properties, and validates them through a cruise-control case study. Results indicate improved interpretability, tractability, and verifiability of system requirements, while acknowledging limitations and opportunities for extending the approach to discrete transition systems.

Abstract

In systems engineering, accurately decomposing requirements is crucial for creating well-defined and manageable system components, particularly in safety-critical domains. Despite the critical need, rigorous, top-down methodologies for effectively breaking down complex requirements into precise, actionable sub-requirements are scarce, especially compared to the wealth of bottom-up verification techniques. Addressing this gap, we introduce a formal decomposition for contract-based design that guarantees the correctness of decomposed requirements if specific conditions are met. Our (semi-)automated methodology augments contract-based design with reachability analysis and constraint programming to systematically identify, verify, and validate sub-requirements representable by continuous bounded sets -- continuous relations between real-valued inputs and outputs. We demonstrate the efficacy and practicality of a correct-by-construction approach through a comprehensive case study on a cruise control system, highlighting how our methodology improves the interpretability, tractability, and verifiability of system requirements.

Figures (9)

• Figure 1: Requirements engineering can be enhanced through the application of formal methods, typically employed on the right side of the V model, to ensure precision and accuracy (adapted from 4754a).
• Figure 2: Refinement by decomposition takes a high-level contract and reduces it to a candidate implementation.
• Figure 3: Primary refinement decomposes top-level contracts and joins them in one representation.
• Figure 4: Decomposition produces a potential design solution with associated behavioral guarantees.
• Figure 5: The inherent tension between subcontracts.