University of Surrey

Test tubes in the lab Research in the ATI Dance Research

SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B

Dalvandi, Mohammadsadegh, Butler, Michael and Fathabadi, Asieh Salehi (2019) SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B In: Workshop on Practical Formal Verification for Software Dependability (AFFORD 2019), 07 Oct 2019, Porto, Portugal.

[img]
Preview
Text
SEB-CG.pdf - Accepted version Manuscript

Download (660kB) | Preview

Abstract

The guarded atomic action model of Event-B allows it to be applied to a range of systems including sequential, concurrent and distributed systems. However, the lack of explicit sequential structures in Event-B makes the task of sequential code generation difficult. Scheduled Event-B (SEB) is an extension of Event-B that augments models with control structures, supporting incremental introduction of control structures in refinement steps. SEB-CG is a tool for automatic code generation from SEB to executable code in a target language. The tool provides facilities for derivation of algorithmic structure of programs through refinement. The flexible and configurable design of the tool allows it to target various programming languages. The tool benefits from xText technology for a user-friendly text editor together with the proving facilities of Rodin platform for formal analysis of the algorithmic structure.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computer Science
Authors :
NameEmailORCID
Dalvandi, Mohammadsadeghm.dalvandi@surrey.ac.uk
Butler, Michael
Fathabadi, Asieh Salehi
Date : 7 October 2019
Funders : Engineering and Physical Sciences Research Council (EPSRC)
Grant Title : PRiME Project
Uncontrolled Keywords : Automatic Code Generation; Event-B; Program Verification
Related URLs :
Additional Information : Co-located with the Formal Methods 2019 (FM'19), Porto, Portugal, 07-11 Oct 2019 (http://formalmethods2019.inesctec.pt/)
Depositing User : Clive Harris
Date Deposited : 09 Dec 2019 13:03
Last Modified : 09 Dec 2019 13:03
URI: http://epubs.surrey.ac.uk/id/eprint/853249

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800