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, but verification of their implementations is a challenge that has been taken up by few. We are aware...
| Main Authors: | , , |
|---|---|
| Formato: | Journal article |
| Idioma: | English |
| Publicado: |
2011
|
| _version_ | 1826270302641848320 |
|---|---|
| author | Cavalcanti, A Clayton, P O'Halloran, C |
| author_facet | Cavalcanti, A Clayton, P O'Halloran, C |
| author_sort | Cavalcanti, A |
| collection | OXFORD |
| description | 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, but verification of their implementations is a challenge that has been taken up by few. We are aware only of approaches that rely on automatic code generation, which is not enough assurance for certification, and often not adequate when tailored hardware components are used. Our work is based on Circus, a notation that combines Z, CSP, and a refinement calculus, and on industrial tools that produce partial Z and CSP models of discrete-time Simulink diagrams. We present a strategy to translate Simulink diagrams to Circus, and a strategy to prove that a parallel Ada implementation refines the Circus specification; we rely on a Circus semantics for the program. By using a combined notation, we provide a specification that considers both functional and behavioural aspects of a large set of diagrams, and support verification of a large number of implementations. We can handle, for instance, arbitrarily large data types and dynamic scheduling. © 2010 BCS. |
| first_indexed | 2024-03-06T21:38:43Z |
| format | Journal article |
| id | oxford-uuid:4726e6fb-170f-4d39-b040-c4a5659c28c9 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T21:38:43Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | oxford-uuid:4726e6fb-170f-4d39-b040-c4a5659c28c92022-03-26T15:18:26ZFrom control law diagrams to Ada via CircusJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:4726e6fb-170f-4d39-b040-c4a5659c28c9EnglishSymplectic Elements at Oxford2011Cavalcanti, AClayton, PO'Halloran, CControl 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, but verification of their implementations is a challenge that has been taken up by few. We are aware only of approaches that rely on automatic code generation, which is not enough assurance for certification, and often not adequate when tailored hardware components are used. Our work is based on Circus, a notation that combines Z, CSP, and a refinement calculus, and on industrial tools that produce partial Z and CSP models of discrete-time Simulink diagrams. We present a strategy to translate Simulink diagrams to Circus, and a strategy to prove that a parallel Ada implementation refines the Circus specification; we rely on a Circus semantics for the program. By using a combined notation, we provide a specification that considers both functional and behavioural aspects of a large set of diagrams, and support verification of a large number of implementations. We can handle, for instance, arbitrarily large data types and dynamic scheduling. © 2010 BCS. |
| spellingShingle | Cavalcanti, A Clayton, P O'Halloran, C From control law diagrams to Ada via Circus |
| title | From control law diagrams to Ada via Circus |
| title_full | From control law diagrams to Ada via Circus |
| title_fullStr | From control law diagrams to Ada via Circus |
| title_full_unstemmed | From control law diagrams to Ada via Circus |
| title_short | From control law diagrams to Ada via Circus |
| title_sort | from control law diagrams to ada via circus |
| work_keys_str_mv | AT cavalcantia fromcontrollawdiagramstoadaviacircus AT claytonp fromcontrollawdiagramstoadaviacircus AT ohalloranc fromcontrollawdiagramstoadaviacircus |