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 have implemented a prototype for the refinement and equality checking of component behavior using a reduction to the model checker Mona.

MontiArcAutomaton verification resources

[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