Design for Verification: Using Design Patterns to Build Reliable Systems

Components are mainly used in commercial software development to reduce time to market. While some effort has been spent on formal aspects of components, most of this was done in the context of integration into programming languages or operating system frameworks. As a consequence, increased reliability of composed systems is merely regarded as a side effect of a more rigid testing of pre-fabricated components. In contrast to this, Design for Verification (D4V) puts the focus on component specific property guarantees, which are used to design systems with high reliability requirements. D4V components are domain specific design pattern instances with well-defined property guarantees and usage rules, which are suitable for automatic verification. The guaranteed properties are explicitly used to select components according to key system requirements. The D4V hypothesis is that the same general architecture and design principles leading to good modularity, extensibility and complexity/functionality ratio can be adapted to overcome some of the limitations of conventional reliability assurance methods, such as too large a state space or too many execution paths. 1