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 Seiten 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. (gz, 56 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence