Mechanised Translation of Control Law Diagrams into Circus

摘要

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.