Mechanised Translation of Control Law Diagrams into Circus

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Previously we proposed a strategy for translating control law diagrams into Circus. Combining elements from Z, CSP, and a refinement calculus, Circus captures functional and dynamic aspects of a diagram, and allows us to formally, verify, implementations. The main contributions of this paper are first to discuss a generalisation of the existing translation strategy, motivated by its mechanisation and application to sizable examples. Secondly, we present a tool, the Circus Producer, which automates the translation, and describe how its architecture facilitates subsequent development of further verification tools.

Original languageEnglish
Title of host publicationIntegrated Formal Methods
EditorsM Leuschel, H Wehrheim
Number of pages16
Volume5423 LNCS
Publication statusPublished - 2009
Event7th International Conference on Integrated Formal Methods - Dusseldorf
Duration: 16 Feb 200919 Feb 2009

Publication series

NameLecture Notes in Computer Science


Conference7th International Conference on Integrated Formal Methods

Cite this