| The Approach: Integrating Object Oriented Design and Formal Veri cation (2007) | |||||||||||||||
Abstract | |||||||||||||||
| . This paper reports on the ongoing KeY project aimed at bridging the gap between (a) OO software engineering methods and tools and (b) deductive verication. A distinctive feature of our approach is the use of a commercial CASE tool enhanced with functionality for formal specication and deductive verication. 1 Introduction 1.1 Analysis of the Current Situation While formal methods are by now well established in hardware and system design (the majority of producers of integrated circuits are routinely using BDD-based model checking packages for design and validation), usage of formal methods in software development is currently conned essentially to academic research projects. Although there are industrial applications of formal software development [7], these are still exceptional [8]. The limits of applicability of formal methods in software design are not dened by the potential range and power of existing approaches. Several case studies clearly demonstrate that computer... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||