Previous work described how to translate Simulink control law diagrams into Circus specifications to facilitate verification by refinement. This is not a trivial task; several tools have been developed to automate parts of the translation. This paper introduces a new tool chain that extends and integrates existing technology to cover the entire translation and cater for a larger set of diagrams. Our contributions include the integration of data types, generic definitions, and extension of the technique to model action and enabled subsystems. The tool chain has been validated using an industrial case study.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{MarriottZC12,
author = {Chris Marriott and
Frank Zeyda and
Ana Cavalcanti},
editor = {John Derrick and
John S. Fitzgerald and
Stefania Gnesi and
Sarfraz Khurshid and
Michael Leuschel and
Steve Reeves and
Elvinia Riccobene},
title = {A Tool Chain for the Automatic Generation of Circus Specifications
of Simulink Diagrams},
booktitle = {Abstract State Machines, Alloy, B, VDM, and {Z} - Third International
Conference, {ABZ} 2012, Pisa, Italy, June 18-21, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7316},
pages = {294--307},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-30885-7\_21},
doi = {10.1007/978-3-642-30885-7\_21},
timestamp = {Mon, 05 Feb 2024 20:35:41 +0100},
biburl = {https://dblp.org/rec/conf/asm/MarriottZC12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}