Résumé de séminaire

Résumé :

The theory of refinement with foundations in the model of concurrency based around Hoare's CSP-Communicating Sequential Processes, allows a wide range of correctness conditions, including deadlock and livelock freedom as well as general safety and liveness properties, to be encoded (using standard idioms) as a comparison between processes.

FDR (Failures-Divergence Refinement) allows the checking of many properties of finite-state systems and the investigation of systems which fail these checks. It is based on the theory of Communicating Sequential Processes developed at Oxford University and applied successfully in a number of industrial applications. Its method of establishing whether a property holds is to test for the refinement of a transition system capturing the property by the candidate machine. There is also the ability to check determinism of a state machine, and this is used primarily for checking security properties.

Previous versions used only explicit model-checking techniques: the check proceeds by a recursion induction which fully expands the reachable state-space of the two systems and visits each pair of supposedly corresponding states in turn. Although it is very efficient in doing this and can deal with processes with approximately 10^7 (10 to the power 7) states taht could be analysed in reasonable time on a standard low-end workstation, the exponential growth of state-space with the number of parallel processes in a network represents a significant limit on its utility. The new version of FDR was to improve on the flexibility and scalability of the tool. In particular, it offers

• support for operators outside the core CSP and, indeed, completely different languages
• improved handling of multi-way synchronisation, with the representation of firing rules based on the events which components may engage in, rather than pattern-matching on their states
• provision of a much more powerful language for data types and expressions potential for "lazy" exploration of systems (allowing some non-finite-state specifications)
• the ability to build up a system gradually, at each stage compressing the subsystems to produce an equivalent process with (hopefully) many less states.

This last item means that FDR2 improves on its performance, and incorporates hierarchical abstraction and compression facilities which allow some forms of system with extremely large state-spaces (7^(2^1024), for example) to be analysed in minutes.

FDR is constructed to make its capabilities understandable and usable, and has extensive debugging facilities to support system development, rather than simply verification.

This seminar will present the basic theory behind FDR and will give some examples of application.