Design for Verification with Dynamic Assertions

Completed design and implementation are often regarded as prerequisites of any verification. While recent development methods establish testability as a design criterion, there is no corresponding design support for other verification 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