Proving Things Correct

Abstract

So far we’ve checked to see if a design is correct by taking two SCCS agents, one representing the specification and the other the proposed design, and compared their behaviours action by action using bisimulations — strong bisimulation for complete system behaviour and weaker observational bisimulation for external behaviours. While this method scores on simplicity, in lots of cases action by action comparison is too distinctive; rather than proving two agents identical, we’re more likely to want to prove that they either have or do not have certain properties.