CheckVML: A tool for model checking visual modeling languages

Ákos Schmidt, D. Varró

Research output: Contribution to journalArticle

54 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)92-95
Number of pages4
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2863
Publication statusPublished - 2003

Fingerprint

Visual Languages
Model checking
Modeling Language
Model Checking
Language
Metamodeling
Graph Transformation
Transition Systems
Metamodel
Specification
Specifications
Modeling languages
Arbitrary
Model

Keywords

  • Formal verification
  • Graph transformation
  • Metamodeling
  • Model checking
  • Visual modeling languages

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science
  • Engineering(all)

Cite this

@article{c2217db6230040359646cfaa5ec10527,
title = "CheckVML: A tool for model checking visual modeling languages",
abstract = "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 = "Formal verification, Graph transformation, Metamodeling, Model checking, Visual modeling languages",
author = "{\'A}kos Schmidt and D. Varr{\'o}",
year = "2003",
language = "English",
volume = "2863",
pages = "92--95",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - CheckVML

T2 - A tool for model checking visual modeling languages

AU - Schmidt, Ákos

AU - Varró, D.

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

KW - Formal verification

KW - Graph transformation

KW - Metamodeling

KW - Model checking

KW - Visual modeling languages

UR - http://www.scopus.com/inward/record.url?scp=0242276159&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0242276159&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0242276159

VL - 2863

SP - 92

EP - 95

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -