The VSE Refinement Method in HETS

Mihai Codescu, Bruno Langenstein, Christian Maeder, Till Mossakowski

In: K. Breitman , A. Cavalcanti (Hrsg.). Proceedings of the 11th International Conference on Formal Engineering Methods. International Conference on Formal Engineering Methods (ICFEM-2009) December 9-12 Rio de Janeiro Brazil Lecture Notes in Computer Science (LNCS) 5885 Springer 2009.


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.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence