A formal object-oriented analysis for software reliability: Design for verification

Abstract

This paper presents the OOA design step in a methodology which integrates automata-based model checking into a commercially supported OO software development process.We define and illustrate a set of design rules for OOA models with executable semantics, which lead to automata models with tractable state spaces. The design rules yield OOA models with functionally structured designs similar to those of hardware systems. These structures support modelchecking through techniques known to be feasible for hardware. The formal OOA methodology, including the design rules, was applied to the design of NASA robot control software. Serious logical design errors that had eluded prior testing, were discovered in the course of model-checking.