Semantic translation of simulink/stateflow models to hybrid automata using graph transformations

Aditya Agrawal, Gyula Simon, Gabor Karsai

Research output: Contribution to journalArticle

100 Citations (Scopus)


Embedded systems are often modeled using Matlab's Simulink and Stateflow (MSS), to simulate plant and controller behavior but these models lack support for formal verification. On the other hand verification techniques and tools do exist for models based on the notion of Hybrid Automata (HA) but there are no tools that can convert Simulink/Stateflow models into their semantically equivalent Hybrid Automata models. This paper describes a translation algorithm that converts a well-defined subset of the MSS modeling language into an equivalent hybrid automata. The translation has been specified and implemented using a metamodel-based graph transformation tool. The translation process allows semantic interoperability between the industry-standard MSS tools and the new verification tools developed in the research community.

Original languageEnglish
Pages (from-to)43-56
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
Issue number1-4 SPEC. ISS.
Publication statusPublished - Dec 14 2004


  • Embedded Systems
  • Graph Transformations
  • Hybrid Systems
  • Semantics

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Semantic translation of simulink/stateflow models to hybrid automata using graph transformations'. Together they form a unique fingerprint.

  • Cite this