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.

References in zbMATH (referenced in 11 articles )

Showing results 1 to 11 of 11.
Sorted by year (citations)

  1. Rensink, Arend: The edge of graph transformation -- graphs for behavioural specification (2010)
  2. Kuske, Sabine; Gogolla, Martin; Kreowski, Hans-Jörg; Ziemann, Paul: Towards an integrated graph-based semantics for UML (2009) ioport
  3. Rafe, Vahid; Rahmani, Adel T.: Towards automated software model checking using graph transformation systems and bogor (2009)
  4. Baresi, Luciano; Rafe, Vahid; Rahmani, Adel T.; Spoletini, Paola: An efficient solution for model checking graph transformation systems (2008) ioport
  5. Ermel, Claudia; Ehrig, Hartmut: Behavior-preserving simulation-to-animation model and rule transformations (2008)
  6. Narayanan, Anantha; Karsai, Gabor: Towards verifying model transformations (2008)
  7. Rafe, Vahid; Rahmani, Adel T.: Formal analysis of workflows using UML 2.0 activities and graph transformation systems (2008)
  8. Jürjens, Jan; Shabalin, Pasha: Tools for secure systems development with UML (2007) ioport
  9. Baresi, Luciano; Spoletini, Paola: On the use of Alloy to analyze graph transformation systems (2006)
  10. Rensink, Arend; Schmidt, Ákos; Varró, Dániel: Model checking graph transformations: A comparison of two approaches (2004)
  11. Varró, Dániel: Automated formal verification of visual modeling languages by model checking (2004) ioport