CheckVML: A Tool for Model Checking Visual Modeling Languages. In the paper, we present a tool for model checking dynamic consistency properties in arbitrary well-formed instance models of any modeling language defined visually by metamodeling and graph transformation techniques. Our tool first translates such high-level specifications into a tool independent abstract representation of transition systems defined by a corresponding metamodel. From this intermediate representation the input language of the back-end model checker tool (i.e., SPIN in our case) is generated automatically.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Rensink, Arend: The edge of graph transformation -- graphs for behavioural specification (2010)
- Kuske, Sabine; Gogolla, Martin; Kreowski, Hans-Jörg; Ziemann, Paul: Towards an integrated graph-based semantics for UML (2009) ioport
- Ermel, Claudia; Ehrig, Hartmut: Behavior-preserving simulation-to-animation model and rule transformations (2008)
- Narayanan, Anantha; Karsai, Gabor: Towards verifying model transformations (2008)
- Rafe, Vahid; Rahmani, Adel T.: Formal analysis of workflows using UML 2.0 activities and graph transformation systems (2008)
- Jürjens, Jan; Shabalin, Pasha: Tools for secure systems development with UML (2007) ioport
- Baresi, Luciano; Spoletini, Paola: On the use of Alloy to analyze graph transformation systems (2006)
- Rensink, Arend; Schmidt, Ákos; Varró, Dániel: Model checking graph transformations: A comparison of two approaches (2004)
- Varró, Dániel: Automated formal verification of visual modeling languages by model checking (2004) ioport