Verifying Cross-layer Interactions through Formal Model-based Assertion Generation
Tools
Tools
Tools
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.
|
Text
Verifying Cross-layer Interactions through Formal Model-based Assertion Generation.pdf - Accepted version Manuscript Download (229kB) | Preview |
Official URL: http://dx.doi.org/10.1109/LES.2019.2955316
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 : |
|
|||||||||||||||
| 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 |
Downloads
Downloads per month over past year