Sciweavers

Share
ERSHOV
2009
Springer

Applicability of the BLAST Model Checker: An Industrial Case Study

10 years 2 months ago
Applicability of the BLAST Model Checker: An Industrial Case Study
Model checking of software has been a very active research topic recently. As a result, a number of software model checkers have been developed for analysis of software written in different programming languages, e.g., SLAM, BLAST, and Java PathFinder. Applicability of these tools in the industrial development process, however, is yet to be shown. In this paper, we present results of an experiment, in which we applied BLAST, a state-of-the-art model checker for C programs, in industrial settings. An industrial strength C implementation of a protocol stack has been verified against a set of formalized properties. We have identified real bugs in the code and we have also reached the limits of the tool. This experience report provides valuable guidance for developers of code analysis tools as well as for general software developers, who need to decide whether this kind of technique is ready for application and suitable for their particular goals.
Emanuel Kolb, Ondrej Sery, Roland Weiss
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Where ERSHOV
Authors Emanuel Kolb, Ondrej Sery, Roland Weiss
Comments (0)
books