German-Portuguese Joint Research Programme, GRICES-DAAD, 2008-2009, between
The static verification of various liveness properties of processes has been the object of several works in the last few years. The properties are in general undecidable (even in restricted settings) and a typing discipline is a natural approach to enforce them. In the context of the pi-calculus, examples of properties studied with this approach are lock freedom, name receptiveness, name responsiveness and strong normalisation. When reasoning about process behaviour one often needs to know (or enforce) certain properties of (to) given names, but not to all of them, and moreover, different names may require different properties. Furthermore, imposing properties on names instead of on processes allows more liberal process behaviour (e.g., a process may have deterministic names without being deterministic itself). This approach eases the verification of liveness properties, and is, for instance, often crucial to ensure full abstraction results when defining calculi encodings, like for checking the correctness of an encoding of non-deterministic processes handling deterministic values. We are mainly interested in functional properties at the name level, i.e., properties specifying the functional behaviour of names inside processes (usually called channel properties). % In particular, we are interest in receptiveness, in responsiveness, and in determinacy. Receptive names are immediately able of receiving a request, once created. If every request triggers a continuation with always the same behaviour, the receptiveness is said uniform. Responsive names eventually reply to a request. Determinate names behave uniformly. Given an assignment of channel properties to each free name in a process (a specification of process behaviour, via name behaviour), we want to verify if the specification is actually respected by the process. We thus aim at a type checking algorithm.
These name properties may be combined to ensure properties of processes like termination, strong normalisation, dead- and live-lock freedom. These are crucial properties for distributed systems, and one needs to enforce them, e.g., to verify protocol correctness, or to get full abstraction results of calculi encoding (as the encodings are deterministic and terminating protocols). One then should study its impact on behavioural equivalences and process reasoning, develop theory and proof techniques, and illustrate their usefulness on some non-trivial examples. We thus propose to combine the expertise of both partners to develop a general type system for channel-based properties, to develop typed behavioural theory based on that system. We have also in mind two concrete application problems: (1) the encoding of the Typed Concurrent Objects (TyCO) calculus into the pi-calculus; (2) the verification of the correctness of protocols, in particular that they are deterministic and terminate. TyCO is an object-based version of the asynchronous pi-calculus, particularly suitable to the specification and verification of distributed systems. Although it has powerful and expressive type systems, it lacks behavioural theory. An encoding would allow to import it from the pi-calculus. We plan to use then the theory and techniques to analyse security protocols.