MURAL - Maynooth University Research Archive Library



    Transforming EVENT B Models into Verified C# Implementations


    Mery, Dominique and Monahan, Rosemary (2013) Transforming EVENT B Models into Verified C# Implementations. In: Verification and Program Transformation 2013 (VPT 2013), 13-14 July 2013, St. Petersburg, Russia.

    [img]
    Preview
    Download (315kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    The refinement-based approach to developing software is based on the correct-by-construction paradigm where software systems are constructed via the step-by-step refinement of an initial high-level specification into a final concrete specification. Proof obligations, generated during this process are discharged to ensure the consistency between refinement levels and hence the system’s overall correctness. Here, we are concerned with the refinement of specifications using the EVENT B modelling language and its associated toolset, the RODIN platform. In particular, we focus on the final steps of the process where the final concrete specification is transformed into an executable algorithm. The transformations involved are (a) the transformation from an EVENT B specification into a concrete recursive algorithm and (b) the transformation from the recursive algorithm into its equivalent iterative version. We prove both transformations correct and verify the correctness of the final code in a static program verification environment for C# programs, namely the Spec# programming system

    Item Type: Conference or Workshop Item (Paper)
    Keywords: software development; EVENT B Models; Verified C# Implementations; C# programs; Spec# programming;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Item ID: 6502
    Depositing User: Rosemary Monahan
    Date Deposited: 29 Oct 2015 16:56
    Refereed: Yes
    URI:
      Use Licence: This item is available under a Creative Commons Attribution Non Commercial Share Alike Licence (CC BY-NC-SA). Details of this licence are available here

      Repository Staff Only(login required)

      View Item Item control page

      Downloads

      Downloads per month over past year

      Origin of downloads