Automatická veri kace software

• Main Author: Šerý, Ondřej
• Other Authors: Plášil, František
• Format: Doctoral Thesis
• Language: English
• Published: 2010
• Online Access: http://www.nusl.cz/ntk/nusl-299478

Despite the research e ort being invested into the eld of automated veri cation of software, its adoption in industry is still rather slow. Several reasons for this hesitation may be identi ed. The thesis focuses on the following two (i) dificulty of assessment of di erent tools, and (ii) difficulty of tools usage and integration in the development process. To facilitate tool assessment, we provide a comprehensive overview of code model checking techniques with evaluation based on a common set of criteria. In addition, we contribute by an industrial case study on applicability of the BLAST model checker. Since also proper education is necessary for the ability of tool assessment, we include our experience report on preparation of two master-level formal method courses. By incorporating an easy to use speci cation language into the BLAST model checker, the thesis contributes to facilitating tools usage. In addition, we introduce the concept of unit checking, a combination of unit testing and code model checking, which helps integration of code model checking in the software development process.