Mechanised Translation of Control Law Diagrams into Circus

TY - GEN

T1 - Mechanised Translation of Control Law Diagrams into Circus

AU - Zeyda, Frank

AU - Cavalcanti, Ana

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=67650445996&partnerID=8YFLogxK

M3 - Conference contribution

VL - 5423 LNCS

T3 - Lecture Notes in Computer Science

SP - 151

EP - 166

BT - Integrated Formal Methods

A2 - Leuschel, M

A2 - Wehrheim, H

PB - Springer

T2 - 7th International Conference on Integrated Formal Methods

Y2 - 16 February 2009 through 19 February 2009

ER -