Bas Graaf, Eun Young Kang, Marco Lormans, and Hans Toetenel
Faculty of Electrical Engineering, Mathematics, and Computer Science, Delft University of Technology
The embedded software industry clearly needs objective and reproducible means for early evaluation of software products. Formal methods can potentially fill the void, however industry is reluctant in applying these methods.
In this study we investigate the difficulties that arise when integrating formal methods with the typical software engineering practice. More particular we look at the integration of model checking techniques in the requirement engineering and architecture design phases of the software development lifecycle.
The results indicate some specific shortcomings of the currently available technology that prevent easy integration of model checking techniques in an industrial software development process.