From Control Law Diagrams to Ada Via Circus

Control engineers make extensive use of diagrammatic notations; control law diagrams are used in industry every day. Techniques and tools for analysis of these diagrams or their models are plentiful; verification of code created to implement them, however, is a challenge that has been taken up by few. The paper is based on industrial tools that produce partial Z and CSP models of discrete-time Simulink diagrams, and on Circus, a notation that combines Z, CSP, and a refinement calculus. The authors present a strategy to translate Simulink diagrams to Circus, and a strategy to prove that a parallel Ada implementation refines the specification of a diagram; they rely on a Circus semantics for the program.