University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Verifying Cross-layer Interactions through Formal Model-based Assertion Generation

Fathabadi, Asieh Salehi, Dalvandi, Mohammadsadegh, Butler, Michael and Al-Hashimi, Bashir M. (2019) Verifying Cross-layer Interactions through Formal Model-based Assertion Generation IEEE Embedded Systems Letters.

[img]
Preview
Text
Verifying Cross-layer Interactions through Formal Model-based Assertion Generation.pdf - Accepted version Manuscript

Download (229kB) | Preview

Abstract

Cross-layer runtime management (RTM) frameworks for embedded systems provide a set of standard APIs for communication between different system layers (i.e. RTM, applications and device) and simplify the development process by abstracting these layers. Integration of independently developed components of the system is an error-prone process that requires careful verification. In this paper, we propose a formal approach to integration testing through automatic generation of runtime assertions in order to test the implementation of the APIs. Our approach involves a formal model of the APIs, developed using the Event-B formal method which is automatically translated to a set of assertions and embedded in the existing implementation of APIs. The embedded assertions are used at runtime to check the correctness of the integration. This work was supported by the EPSRC PRiME Project (EP/K034448/1), www.prime-project.org.

Item Type: Article
Divisions : Faculty of Engineering and Physical Sciences > Computer Science
Authors :
NameEmailORCID
Fathabadi, Asieh Salehi
Dalvandi, Mohammadsadeghm.dalvandi@surrey.ac.uk
Butler, Michael
Al-Hashimi, Bashir M.
Date : 22 November 2019
Funders : Engineering and Physical Sciences Research Council (EPSRC)
DOI : 10.1109/LES.2019.2955316
Grant Title : PRiME Project
Copyright Disclaimer : © 2019 IEEE. Personal use is permitted, but republication/redistribution requires IEEE permission. See http://www.ieee.org/publications_standards/publications/rights/index.html for more information.
Uncontrolled Keywords : Runtime; Monitoring; Tools; Temperature measurement; Temperature sensors; C++ languages; Mathematical model
Depositing User : Clive Harris
Date Deposited : 09 Dec 2019 13:02
Last Modified : 09 Dec 2019 13:02
URI: http://epubs.surrey.ac.uk/id/eprint/853247

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