MURAL - Maynooth University Research Archive Library



    On Two Friends for Getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in Rodin


    Cheng, Zheng and Mery, Dominique and Monahan, Rosemary (2016) On Two Friends for Getting Correct Programs Automatically Translating Event B Specifications to Recursive Algorithms in Rodin. Lecture Notes in Computer Science. pp. 821-838. ISSN 0302-9743

    [img]
    Preview
    Download (634kB) | Preview


    Share your research

    Twitter Facebook LinkedIn GooglePlus Email more...



    Add this article to your Mendeley library


    Abstract

    We report on our progress-to-date in implementing a software development environment which integrates the efforts of two formal software engineering techniques: program refinement as supported by Event B and program verification as supported by the Spec# programming system. Our objective is to improve the usability of formal verification tools by providing a general framework for integrating these two approaches to software verification. We show how the two approaches Correctness-by-Construction and Post-hoc Verification can be used in a productive way. Here, we focus on the final steps in this process where the final concrete specification is transformed into an executable algorithm. We present EB2RC, a plug-in for the Rodin platform, that reads in an Event B model and uses the control framework introduced during its refinement to generate a graphical representation of the executable algorithm. EB2RC also generates a recursive algorithm that is easily translated into executable code. We illustrate our technique through case studies and their analysis.

    Item Type: Article
    Additional Information: from: Leveraging Applications of Formal Methods, Verification and Validation Foundational Techniques 7th International Symposium, ISoLA 2016 Imperial, Corfu, Greece, October 10–14, 2016 Proceedings, Part I
    Keywords: Recursive Algorithm; Proof Obligation; Executable Code; Program Verification; Recursive Program;
    Academic Unit: Faculty of Science and Engineering > Computer Science
    Faculty of Science and Engineering > Research Institutes > Hamilton Institute
    Item ID: 15584
    Identification Number: https://doi.org/10.1007/978-3-319-47166-2
    Depositing User: Rosemary Monahan
    Date Deposited: 28 Feb 2022 14:18
    Journal or Publication Title: Lecture Notes in Computer Science
    Publisher: Springer Verlag
    Refereed: Yes
    URI:

    Repository Staff Only(login required)

    View Item Item control page

    Downloads

    Downloads per month over past year