MURAL - Maynooth University Research Archive Library



    Specification Reuse using Data Refinement in Dafny


    Saleem, Asif (2013) Specification Reuse using Data Refinement in Dafny. Masters thesis, National University of Ireland Maynooth.

    [img] Download (1MB)


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    Data refinement is a technique for transforming system specifications into system implementation that differs in data types. It gives us the freedom to write specifications in a way that is independent of its implementation; moreover we can generate multiple implementations without changing the system specifications, the client does not have to worry about the underlying implementation. Abstraction Invariant is used to relate the high level abstract specification to its concrete implementation. Dafny is a research language developed by Microsoft. Its main focus is data refinement. The language provides the rich mathematical properties such as sequences, sets and multi-set, along with functions, predicates, methods and user defined data types. In Dafny the Abstraction Invariant is in the form of a function, which is added as a pre and post conditions to all of methods and functions. Given this function one can verify that the code is providing the implementation that satisfies its specifications even when the specification is defined in term of one data structure and the code is implemented in term of another data structure. Dafny works with Boogie which is a static program verifier and the SMT solver Z3. These are the main underlying technologies for verification: Dafny code is translated in to Boogie from which the verification conditions are generated for Z3 in order to verify the program. In this research the programmer over head is identified when replacing one implementation to another in terms of underlying data structure change while preserving the client specification. The motivation behind this work is to assist programmers to come up with a quick solution in situations such as “slow system performance” with new system implementation. Moreover, a semi automatic tool is developed for transforming one implementation to another without changing the client specifications. The result is the generation of a semi verified program whose implementation is in terms of a data structure other than that used in the specifications. The verification can be fully automatic through the provision of implementation details from the user.

    Item Type: Thesis (Masters)
    Additional Information: Taught Masters Thesis for the Erasmus Mundus MSc in Dependable Software Systems
    Keywords: Data Refinement; Dafny;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 4555
    Depositing User: IR eTheses
    Date Deposited: 07 Oct 2013 16:06
    URI:

      Repository Staff Only(login required)

      View Item Item control page

      Downloads

      Downloads per month over past year