A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems

被引：0

作者：

Andre, Etienne ^{[1
]}

Barbot, Benoit ^{[2
]}

Demoulins, Clement ^{[3
]}

Hillah, Lom Messan ^{[4
,5
]}

Hulin-Hubard, Francis ^{[2
]}

Kordon, Fabrice ^{[4
,5
]}

Linard, Alban ^{[2
]}

Petrucci, Laure ^{[1
]}

机构：

[1] Univ Paris 13, Sorbonne Paris Cite, LIPN, CNRS,UMR 7030, F-93430 Villetaneuse, France

[2] LSV, CNRS, INRIA & ENS, Cachan, France

[3] EPITA Res & Dev Lab LDRE, Sainte Savine, France

[4] Univ Paris 06, LIP6, CNRS, UMR 7606, Paris, France

[5] Univ Paris Ouest, Nanterre, France

来源：

FORMAL METHODS AND SOFTWARE ENGINEERING | 2013年 / 8144卷

关键词：

Formal methods; Model Driven Engineering; Interoperability; Reusability; Concurrent Systems; Model Checking; NETS;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Over the past two decades, numerous verification tools have been successfully used for verifying complex concurrent systems, modelled using various formalisms. However, it is still hard to coordinate these tools since they rely on such a large number of formalisms. Having a proper syntactical mechanism to interrelate them through variability would increase the capability of effective integrated formal methods. In this paper, we propose a modular approach for defining new formalisms by reusing existing ones and adding new features and/or constraints. Our approach relies on standard XML technologies; their use provides the capability of rapidly and automatically obtaining tools for representing and validating models. It thus enables fast iterations in developing and testing complex formalisms. As a case study, we applied our modular definition approach on families of Petri nets and timed automata.

引用

页码：199 / 214

页数：16