main page

getting started








RWTH Aachen

Fachgruppe Informatik

An Analysis Framework for MontiArcAutomaton Component Behavior

Jan Oliver Ringert, Bernhard Rumpe, and Andreas Wortmann

The development of distributed interactive systems is a challenging task. Hierarchical decomposition of the systems' functionality and explicit identification of interaction help to reduce this complexity. System development involves multiple steps including formalizing initial behavior and refining and evolving functionality. These steps require support for checking refinement and comparing component and subsystem behavior.

MontiArcAutomaton integrates component & connector models and component behavior descriptions via embedded automata. We present mechanisms of MontiArcAutomaton to enable underspecification and allow component models to be used as behavior specifications for subsets of component interfaces or complete systems. Behavior specification and implementation in the same modeling language enable a seamless development process based on stepwise refinement following the Focus methodology. Final models are ready for code generation for various robotics platforms supported by MontiArcAutomaton.

We implemented two prototypes for refinement and equality checking of component behavior

  • using a reduction to the model checker Mona,
  • using a reduction to the language inclusion problem for Büchi automata and using RABIT.

MontiArcAutomaton verification resources including the translation to Mona

[Rin14] J. O. Ringert. Analysis and Synthesis of Interactive Component and Connector Systems. Shaker Verlag, ISBN 978-3-8440-3120-1. Aachener Informatik-Berichte, Software Engineering Band 19. 2014.

Additional example models verification projects Büchi automata in the "BA format" resulting from the translation of the component behavior specifications to Büchi automata: