Essay on semantics definition in MDE: An instrumented approach for model verification

被引：31
作者：
Combemale, Benoît [1 ]
Crégut, Xavier [2 ]
Garoche, Pierre-Loïc [3 ]
Thirioux, Xavier [2 ]
机构：
[1] Institut National de Recherche en Informatique et en Automatique (INRIA), France
[2] Institut de Recherche en Informatique de Toulouse (IRIT), France
[3] Office National d' Étude et de Recherche en Aérospatiale (ONERA), France
来源：
Journal of Software | 2009年 / 4卷 / 09期
关键词：
Model checking - Digital subscriber lines - Problem oriented languages;
D O I：
10.4304/jsw.4.9.943-958
中图分类号：
学科分类号：
摘要：
In the context of MDE (Model-Driven Engineering), our objective is to define the semantics for a given DSL (Domain Specific Language) either to simulate its models or to check properties on them using model-checking techniques. In both cases, the purpose is to formalize the DSL semantics as it is known by the DSL designer but often in an informal way. After several experiments to define operational semantics on the one hand, and translational semantics on the other hand, we discuss both approaches and we specify in which cases these semantics seem to be judicious. As a second step, we introduce a pragmatic and instrumented approach to define a translational semantics and to validate it against a reference operational semantics expressed by the DSL designer. We apply this approach to the XSPEM process description language in order to verify process models. © 2009 Academy Publisher.
引用
收藏
页码：943 / 958
页数：15
相关论文
共 57 条
  • [1] 2.0 Core Specification, Object Management Group, Inc., Jan. 2006, Final Adopted Specification
  • [2] Budinsky F., Steinberg D., Ellersick R., Eclipse Modeling Framework: A Developer's Guide, (2003)
  • [3] Budinsky F., Merks E., Steinberg D., Eclipse Modeling Framework 2.0, (2009)
  • [4] Jouault F., Bezivin J., KM3: A DSL for Metamodel Specification, Ifip Int. Conf. On Formal Methods For Open Object-based Distributed Systems (fmoods), Ser. Lncs, 4037, pp. 171-185, (2006)
  • [5] 2.0 Specification, Object Management Group, Inc., Oct. 2003, Final Adopted Specification
  • [6] Farail P., Gaufillet P., Canals A., Camus C.L., Sciamma D., Michel P., Cregut X., Pantel M., The TOPCASED project: A Toolkit in OPen source for Critical Aeronautic SystEms Design, Embedded Real Time Software (erts'06), (2006)
  • [7] Ledeczi A., Maroti M., Bakay A., Karsai G., Garrett J., Iv C.T., Nordstrom G., Sprinkle J., Volgyesi P., The generic modeling environment, Workshop On Intelligent Signal Processing, (2001)
  • [8] Bezivin J., Jouault F., Rosenthal P., Valduriez P., Modeling in the large and modeling in the small, Model Driven Architecture, pp. 33-46, (2004)
  • [9] Winskel G., The Formal Semantics of Programming Languages: An Introduction, (1993)
  • [10] Muller P.-A., Fleurey F., Jezequel J.-M., Weaving executability into object-oriented meta-languages, Mod-els, Ser. Lncs, (2005)
123456