Model checking in practice: Analysis of Generic Bootloader using SPIN

被引：0

作者：

Das Barman, Kuntal ^{[1
]}

Mukhopadhyay, Debapriyay ^{[2
]}

机构：

[1] HTSL, 15-1 Doraisanipalya,Bannerghatta Rd, Bangalore 560076, Karnataka, India

[2] Tor Anumana Technol Pvt Ltd, Kolkata 700020, India

来源：

FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS | 2007年 / 4789卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This work presents a case study of the use of model checking for analyzing an industrial software, the Generic Bootloader. Analysis of the software have been carried out using the automated verification system SPIN. A model of the software has been developed using the specification language PROMELA, and the properties expressed in the LTL have been verified against the model. We propose a new modeling technique that helps to model communication protocols efficiently. Formal analysis has also helped us to reveal a flaw in the implementation of the software which otherwise remain undetected through testing process.

引用

页码：232 / +

页数：2