 |
|
 |
Back to list of 2000/01 seminars
| Circus: a unifying theory of Z and CSP | ||
|---|---|---|
| Tuesday 27 March 2001 | 16:00 | Brian Spratt Room |
|
Jim Woodcock
Oxford University Computing Laboratory |
||
Circus is a new language that combines specification statements with imperative CSP, in the same manner that Morgan's refinement calculus combines them with the guarded command language. The specification statements in Circus are operations ona state described using the Z notation. Circus has a formal model, and we're in the process of deriving refinement laws to form a calculus. A Circus specification denotes a Z specification, and the formal model is given in Hoare & He's Unifying Theory of Programming.
State components may be referred to directly in the CSP processes of a Circus specification, with an implicit finalisation containing all references; this means that the Z paragraphs may be refined separately. The Circus specification is not permitted to make any reference to the underlying failures-divergences model.
A number of case studies have driven the design of Circus: Abrial's safety-critical steam boiler, Alcatel's safety-critical dwarf signal, Handel-C's secure IP-packet firewall, and Mondex's secure smart card. Extracts from these specifications will be used to illustrate Circus specifications and their analysis.
Circus n. An open space where different routes converge (as in Oxford Circus).
