e-journal

Recursive Modeling of Stateflow as Input/Output-Extended Automaton

---

Stateflow, a graphical interface tool for Matlab, is a common choice for design of event-driven software and systems. In order for their offline analysis (testing/verification) or online analysis (monitoring), the Stateflow model must be converted to a form that is amenable to formal analysis. In this paper, we present a systematic method, which translates Stateflow into a formal model, called Input/Output Extended Finite Automata (I/O-EFA). The translation method treats each state of the Stateflow model as an atomic module, and applies composition/refinement rules for each feature (such as state-hierarchy, local events) recursively to obtain the entire model. The size of the translated model is linear in the size of the Stateflow chart. Our translation method is sound and complete in the sense that it preserves the discrete
behaviors as observed at the sample times. Further, the translation method has been implemented in a Matlab tool, which outputs the translated I/O-EFA model that can itself be simulated in Matlab.
Note to Practitioners—This paper presents a methodology and tool that enables a formal reasoning about the correctness of a reactive/control software written in Simulink/Stateflow through its translation into an automaton model. The discrete modeling formalism of an automaton extended with input/ouput/state variables suffices, since Simulink/Stateflow is a discrete-time system and the translated model preserves all the discrete-time behaviors. This work complements our earlier work that translated only the timedriven blocks; the event-driven components (Stateflow blocks) are
also translated here.
Index Terms—Extended finite automata, stateflow, translation.

---

Ketersediaan

Tidak ada salinan data

Informasi Detail

Judul Seri

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING

No. Panggil

-

Penerbit

New York : IEEE., 2014

Deskripsi Fisik

IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, VOL. 11, NO. 4, OCTOBER 2014

Bahasa

English

ISBN/ISSN

1545-5955

Klasifikasi

-

Tipe Isi

-

Tipe Media

-

Tipe Pembawa

-

Edisi

VOL. 11, NO. 4, OCTOBER 2014

Subjek

TEKNIK

Info Detail Spesifik

-

Pernyataan Tanggungjawab

Yuli/Agus

Versi lain/terkait

Lampiran Berkas

Komentar

---

Anda harus masuk sebelum memberikan komentar