Assumption-Commitment Specifications and Safety-Critical Systems.
Georg Rock, Stephan Werner, Andreas Wolpers · 1998
this paper, we discuss the use of assumption--commitment style specifications for the formal development of safety--critical systems. Assumption--commitment specifications are of the form "as long as the environment will satisfy certain conditions (assumptions), the system will behave in a particular way (commitments)." If the environment violates the assumptions, then after the environment's failure the system may fail to fulfill the commitments as well. Note the requirement that if the system fails, then the environment must have failed before. In this aspect, assumption--commitment specifications differ from ordinary implication.