id: 06059160
dt: j
an: 06059160
au: Miyazawa, Alvaro; Cavalcanti, Ana
ti: Refinement-oriented models of Stateflow charts.
so: Sci. Comput. Program. 77, No. 10-11, 1151-1177 (2012).
py: 2012
pu: Elsevier Science B.V. (North-Holland), Amsterdam
la: EN
cc: 
ut: Simulink; Circus; formal semantics; verification; tools
ci: 
li: doi:10.1016/j.scico.2011.07.007
ab: Summary: 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.
rv: