We present the integration of the refinement method of the VSE verification tool,
successfully used in industrial applications, in the
Heterogeneous Tool Set Hets. The connection is done via introducing the
dynamic logic underlying VSE and two logic translations in the logic
graph of Hets. Thus the logic-independent layers of Hets are not modified and
its proof management formalism can be applied to VSE specifications.
%0 Journal Article
%1 CodescuEtAl2011e
%A Codescu, Mihai
%A Langenstein, Bruno
%A Maeder, Christian
%A Mossakowski, Till
%D 2013
%J Electronic Communications of the EASST
%K Hets VSE dynamic institution logic refinement
%T The VSE Refinement Method in Hets
%U http://journal.ub.tu-berlin.de/eceasst/article/view/859
%V 62
%X We present the integration of the refinement method of the VSE verification tool,
successfully used in industrial applications, in the
Heterogeneous Tool Set Hets. The connection is done via introducing the
dynamic logic underlying VSE and two logic translations in the logic
graph of Hets. Thus the logic-independent layers of Hets are not modified and
its proof management formalism can be applied to VSE specifications.
@article{CodescuEtAl2011e,
abstract = { We present the integration of the refinement method of the VSE verification tool,
successfully used in industrial applications, in the
Heterogeneous Tool Set Hets. The connection is done via introducing the
dynamic logic underlying VSE and two logic translations in the logic
graph of Hets. Thus the logic-independent layers of Hets are not modified and
its proof management formalism can be applied to VSE specifications.},
added-at = {2016-08-05T15:59:03.000+0200},
author = {Codescu, Mihai and Langenstein, Bruno and Maeder, Christian and Mossakowski, Till},
biburl = {https://www.bibsonomy.org/bibtex/22f455f1c60cc45df686670be45216504/tillmo},
interhash = {1271cef34f68f1d89e1c18f8c633e52e},
intrahash = {2f455f1c60cc45df686670be45216504},
journal = {Electronic Communications of the EASST},
keywords = {Hets VSE dynamic institution logic refinement},
pdfurl = {journal.ub.tu-berlin.de/eceasst/article/download/859/853},
status = {Reviewed},
timestamp = {2016-08-05T15:59:03.000+0200},
title = {The VSE Refinement Method in Hets},
url = {http://journal.ub.tu-berlin.de/eceasst/article/view/859},
volume = 62,
year = 2013
}