Assertions from Design Constraints

This is a relatively new territory in my research. It is said that assertions---self-checks on the state of a running program---are most effective when they are derived or generated from the formal specification of a program. The goal of this research is to develop approaches and tool support for generating effective assertions automatically from a program's formal specification. Initially we are investigating on deriving implementation assertions from architectural or design constraints written in architecture description languages (ADL) or the Object Constraint Language (OCL). This will make our approaches and tools more useful to practitioners.

In a position paper that I recently co-authored (Jung, et al., 2007) we proposed a framework for checking at run-time architectural constraints or properties and thus detecting architectural drift and corrosion automatically, which is one of the biggest problems in software maintenance and evolution. The framework is generic in that it isn't defined in terms of a specific ADL or assertion language. We also showed how the framework could be instantiated to a particular pair of ADL (Armani) and assertion language (JML). The key idea of our approach is to express architectural constraints or properties in an assertion language and use the runtime assertion checker of the assertion language to detect any violations of the constraints. The architectural assertions are written in terms of architectural concepts such as components, connectors, and configurations, and thus they can be easily mapped to or traced back to the original high-level constraints written in an architectural description language. The seminal feature of our framework is that it leverages the recent advances of two different but related areas, software architecture and runtime assertion checking. We believe that our approach is effective and more practical than and complements static techniques.

The current research thrust is on runtime checking design constraints written in OCL. OCL is a formal notation to specify constraints on UML models that cannot otherwise be expressed by diagrammatic notations such as class diagrams. OCL constraints cannot be directly executed and thus checked at runtime by an implementation. Thus, constraint violations by an implementation may not be detected or noticed, causing many potential development and maintenance problems. We are investigating different ways of checking OCL constraints at runtime, e.g., translating them to JML assertions or AspectJ aspects (Cheon, et al., 2009). An undergraduate student, Carmen Avila, recently developed a Java library to facilitate the translation of OCL constraints into JML assertions (Avila, Flores, and Cheon, 2008). The library classes implement OCL collection types and enable a direct mapping from OCL to JML by using JML's model variables. The translated JML assertions are stored in specification files, separate from source code files, to ease change management of both OCL constraints and Java source code. We believed that the approach facilitate a seamless transition from OCL-based designs to Java implementations.

Last modified: $Id: assertion.html,v 1.4 2009/03/06 10:22:46 cheon Exp $