Verifying Cross-Layer Interactions Through Formal Model-Based Assertion Generation

被引：1

作者：

Salehi Fathabadi, Asieh ^{[1
]}

Dalvandi, Mohammadsadegh ^{[2
]}

Butler, Michael ^{[1
]}

Al-Hashimi, Bashir M. ^{[1
]}

机构：

[1] Univ Southampton, Fac Engn & Phys Sci, Southampton SO17 1BJ, Hants, England

[2] Univ Surrey, Dept Comp Sci, Guildford GU2 7XH, Surrey, England

来源：

IEEE EMBEDDED SYSTEMS LETTERS | 2020年 / 12卷 / 03期

基金：

英国工程与自然科学研究理事会;

关键词：

Embedded systems; Event-B; formal methods; formal verification; runtime management; VERIFICATION;

D O I：

10.1109/LES.2019.2955316

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

Cross-layer runtime management (RTM) frameworks for embedded systems provide a set of standard application programming interfaces (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 letter, 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.

引用

页码：83 / 86

页数：4

共 12 条

[1] Rodin: An open toolset for modelling and reasoning in Event-B [J].

Abrial J.-R. ;

Butler M. ;

Hallerstede S. ;

Hoang T.S. ;

Mehta F. ;

Voisin L. .

International Journal on Software Tools for Technology Transfer, 2010, 12 (06) :447-466

[2]

Abrial J.-R., 2010, MODELING EVENT B SYS

[3]

Bragg G. M., 2018, P 3 INT C PERV EMB C, P195

[4]

Dalvandi M., 2015, EVENT B MODELS DAFNY

[5]

Dalvandi M., 2018, P INT C STAT MACH AL, P234

[6] A model-based framework for software portability and verification in embedded power management systems [J].

Fathabadi, Asieh Salehi ;

Butler, Michael J. ;

Yang, Sheng ;

Maeda-Nunez, Luis Alfonso ;

Bantock, James ;

Al-Hashimi, Bashir M. ;

Merrett, Geoff V. .

JOURNAL OF SYSTEMS ARCHITECTURE, 2018, 82 :12-23

[7] Towards Automatic Code Generation of Run-Time Power Management for Embedded Systems using Formal Methods [J].

Fathabadi, Asieh Salehi ;

Maeda-Nunez, Luis Alfonso ;

Butler, Michael J. ;

Al-Hashimi, Bashir M. ;

Merrett, Geoff V. .

2015 IEEE 9TH INTERNATIONAL SYMPOSIUM ON EMBEDDED MULTICORE/MANYCORE SYSTEMS-ON-CHIP (MCSOC), 2015, :104-111

[8]

Gadioli D, 2015, PROCEEDINGS INTERNATIONAL CONFERENCE ON EMBEDDED COMPUTER SYSTEMS - ARCHITECTURES, MODELING AND SIMULATION (SAMOS XV), P173, DOI 10.1109/SAMOS.2015.7363673

[9] Runtime Verification of Web Service Interface Contracts [J].

Halle, Sylvain ;

Bultan, Tevfik ;

Hughes, Graham ;

Alkhalaf, Muath ;

Villemaire, Roger .

COMPUTER, 2010, 43 (03) :59-66

[10]

Hoffmann H., 2010, P ACM 7 INT C AUT CO, P79

← 1 2 →