Transforming Event-B Models to Dafny Contracts

Mohammadsadegh Dalvandi, Michael Butler, Abdolbaghi Rezazadeh

Abstract


Our work aims to build a bridge between constructive (top-down) and analytical (bottom-up) approaches to software verification. This paper presents a tool-supported method for linking two existing verification methods: Event-B (constructive) and Dafny (analytical). This method combines Event-B abstraction and refinement with the code-level verification features of Dafny. The link transforms Event-B models to Dafny contracts by providing a framework in which Event-B models can be implemented correctly. The paper presents a method for transformation of Event-B models of abstract data types to Dafny contracts. Also a prototype tool implementing the transformation method is outlined. The paper also defines and proves a formal link between property verification in Event-B and Dafny. Our approach is illustrated with a small case study.

Full Text:

PDF


DOI: http://dx.doi.org/10.14279/tuj.eceasst.72.1021

DOI (PDF): http://dx.doi.org/10.14279/tuj.eceasst.72.1021.1002

Hosted By Universit├Ątsbibliothek TU Berlin.