Skip to main content Skip to main navigation


Assumption-Commitment Specifications and Safety-Critical Systems

Georg Rock; Werner Stephan; Andreas Wolpers
In: Hartmut König; Peter Langendörfer (Hrsg.). Formale Beschreibungstechniken für verteilte Systeme. GI/ITG-Fachgespräch (FBT-98), 8. June 4-5, Cottbus, Germany, Pages 125-135, Shaker Verlag, Aachen, 1998.


In 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.