%0 Conference Paper %1 CodescuEtAl09 %A Codescu, Mihai %A Langenstein, Bruno %A Maeder, Christian %A Mossakowski, Till %B ICFEM 2009 %D 2009 %E Breitman, K. %E Cavalcanti, A. %I Springer %K comorphism hets institution refinement specification vse %P 660-678 %T The VSE Refinement Method in HETS %U http://dx.doi.org/10.1007/978-3-642-10373-5_34 %V 5885 %X We present the integration of refinement method of 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.

@inproceedings{CodescuEtAl09, abstract = { We present the integration of refinement method of 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/2c7e150575f232d8cdb934876ba4db872/tillmo}, booktitle = {ICFEM 2009}, editor = {Breitman, K. and Cavalcanti, A.}, interhash = {9a0cc121a45b6a84dd286675fc40a1ad}, intrahash = {c7e150575f232d8cdb934876ba4db872}, keywords = {comorphism hets institution refinement specification vse}, pages = {660-678}, pdfurl = {http://www.informatik.uni-bremen.de/~till/papers/hetsvse.pdf}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, status = {Reviewed}, timestamp = {2016-08-05T15:59:03.000+0200}, title = {The VSE Refinement Method in HETS}, url = {http://dx.doi.org/10.1007/978-3-642-10373-5_34}, volume = 5885, year = 2009 }