Refinement-based verification of sequential implementations of Stateflow charts

TY - JOUR

T1 - Refinement-based verification of sequential implementations of Stateflow charts

AU - Miyazawa, Alvaro

AU - Cavalcanti, Ana

N1 - In Proceedings Refine 2011, arXiv:1106.3488

PY - 2011/6/21

Y1 - 2011/6/21

N2 - Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such models. In previous work, we have proposed a technique for automatic generation of formal models of Stateflow blocks to support refinement-based reasoning. In this article, we present a refinement strategy that supports the verification of automatically generated sequential C implementations of Stateflow charts. In particular, we discuss how this strategy can be specialised to take advantage of architectural features in order to allow a higher level of automation.

AB - Simulink/Stateflow charts are widely used in industry for the specification of control systems, which are often safety-critical. This suggests a need for a formal treatment of such models. In previous work, we have proposed a technique for automatic generation of formal models of Stateflow blocks to support refinement-based reasoning. In this article, we present a refinement strategy that supports the verification of automatically generated sequential C implementations of Stateflow charts. In particular, we discuss how this strategy can be specialised to take advantage of architectural features in order to allow a higher level of automation.

KW - cs.LO

U2 - 10.4204/EPTCS.55.5

DO - 10.4204/EPTCS.55.5

M3 - Article

SN - 2075-2180

SP - 65

EP - 83

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

ER -