This paper addresses the specification of and reasoning about interactive real-time systems, their interfaces, and architectures as well as their properties in terms of assumptions and commitments. Specifications are structured into assumptions restricting the behavior of the operational context of systems and commitments about the system behavior (also called rely/guarantee or assumption/promise specification patterns in the literature). A logical approach to assumption/commitment contracts is worked out based on a mathematical system model:
- From assumption/commitment contracts plain interface assertions for the system are derived.
- Healthiness conditions based on the system model are worked out for assumptions.
- Safety and liveness properties for assumption/commitment contracts are identified.
- From interaction specifications describing the interaction between two systems assumption/commitment contracts for the involved systems are derived.
- Contracts for components in architectures are formulated in terms of assumptions and commitments and conditions are worked out to guarantee that assumptions for the composite systems guarantee the validity of the assumptions for components.
Based on the theoretical foundation architectural issues are considered for a systematic use of assumption/commitment patterns in system specification and architecture design.
