Abstract: Modal process logic is a generalisation of CCS that provides for ``looseness'' in process specification. This looseness is achieved by labelling each action in a specification to show that it either may be implemented, or must be implemented. We present a case study in which modal process logic is applied to the verification of a safety-relevant air transport application. The modelling of failure recovery in modal process logic is natural: failures are specified as may actions, and recovery procedures are specified as must actions. Thus an implementation that cannot fail is acceptable, but if a failure can occur, then recovery must follow. To simplify the refinement proof we extend the refinement relation of modal process logic with an ``up-to'' proof technique.
Previous | Index | Next An error occured whilst processing this directive