Journal
SCIENCE OF COMPUTER PROGRAMMING
Volume 77, Issue 10-11, Pages 1151-1177Publisher
ELSEVIER SCIENCE BV
DOI: 10.1016/j.scico.2011.07.007
Keywords
Simulink; Circus; Formal semantics; Verification; Tools
Categories
Funding
- EPSRC grant [EP/E025366/1]
- EPSRC [EP/E025366/1, EP/H017461/1] Funding Source: UKRI
- Engineering and Physical Sciences Research Council [EP/E025366/1, EP/H017461/1] Funding Source: researchfish
Ask authors/readers for more resources
Simulink block diagrams are widely used in industry for specifying control systems, and of particular interest and complexity are Stateflow blocks, which are themselves defined by separate charts. To make formal reasoning about diagrams and charts possible, we need to formalise their semantics; for the formal verification of their implementations, a refinement-based semantics is appropriate. An extensive subset of Simulink has been formalised in a language for refinement, namely, Circus, and here, we propose an approach to cover Stateflow charts. Our models are distinctive in their operational nature, which closely reflects the informal description of the Stateflow (simulation) semantics. We describe, formalise, and automate a strategy to generate our Circus models. The result is a solid foundation for reasoning based on refinement. (c) 2011 Elsevier B.V. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available