Projects per year
Abstract
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 language | English |
---|---|
Title of host publication | Integrated Formal Methods |
Editors | M Leuschel, H Wehrheim |
Publisher | Springer |
Pages | 151-166 |
Number of pages | 16 |
Volume | 5423 LNCS |
Publication status | Published - 2009 |
Event | 7th International Conference on Integrated Formal Methods - Dusseldorf Duration: 16 Feb 2009 → 19 Feb 2009 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 2999 |
Conference
Conference | 7th International Conference on Integrated Formal Methods |
---|---|
City | Dusseldorf |
Period | 16/02/09 → 19/02/09 |
Projects
- 1 Finished
-
ProCLaws: Programming from Control Laws
1/07/07 → 30/09/11
Project: Research project (funded) › Research