Partial specifications and compositional verification (Q1177172)

The authors present a compositional proof method for nondeterministic and concurrent systems. The method leads to simple subspecifications by parameterizing bisimulation equivalence with information of the behavioural constraints imposed by the other subsystems. This is possible by allowing partial specifications and partial processes. Partial specifications (processes) may be related through a notion of partial bisimulation (an extension of bisimulation), and the induced implementation ordering. The authors use the method for proving the correctness of a simple scheduler.