Completed design and implementation are often regarded as pre-requisites of any verification. While recent development methods establish testability as a design criterion, there is no corresponding design support for other verifi- cation methods like model checking and static analysis. Since these methods have inherent scalability problems, their application becomes more difficult where it is most needed - for complex systems.

Our Design-for-Verification (D4V) approach attempts to close this gap using a variety of techniques, such as design patterns, APIs and source annotations. This paper presents a overview of D4V, and introduces Dynamic Assertions as one of the proposed D4V techniques.

Dynamic Assertions are dedicated, non-intrusive check objects that are dynamically activated, evaluated and deactivated via assertions of their target objects. Since these check objects can have their own state, they can be used to verify a broad range of properties. Properties can be expressed in the target programming language, and checked in a testing environment. In addition, Dynamic Assertions can be configured via call contexts, making them suitable for connector-specific verification of component based systems.