The successes and failures of behavioural models

摘要

Concurrency is a complex and fascinating subject, and the ways in which a system composed of many processes running in parallel and interacting with each other might behave would seem to most people to defy description. One of Tony Hoare's great insights is that it is possible to get useful models of a concurrent system by recording the set of all the behaviours that an experimenter with an appropriate degree of interest might record from single observations of it, such as traces or failures. The vital principles required of one of these behavioural models are that they should convey useful information about the system being modelled―possibly or possibly not a 'complete' description of it―and must be compositional This means that whenever a construct in our chosen language is used to build a process from syntactic subcomponents―such as putting P and Q in parallel to get P ‖ Q―it must be possible to calculate the set of behaviours our experimenter might observe of the compound process from those of its parts. What we will do in this paper is to examine the successes and failings of this semantic approach, comparing where appropriate with ones based on transition systems. A particularly telling test-bed is the subject of specifying (the lack of) information flow in computer security research, so in the last section we concentrate on that.