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 yeild OOA models with functionally structured designs similar to those of hardware systems. These structures support model-checking 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.
Published in the Proceedings of the Fundamental Approaches to Software Engineering,
4th International Conference,
FASE 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001,
Genoa, Italy, 2001, 15 pages.
PDF
© 2001 Natasha Sharygina.