Initially supported by NSF under Grant No. CNS-0509299 and DUE-0837567, the goal of this project is to develop approaches for constructing correct programs that are formally proved or verified. A specific focus is on investigating the use of formally-specified design documents such as OCL constraints. The Object Constraint Language (OCL) is a textual notation to specify constraints or rules that apply to UML models such as class diagrams. This project investigates both static and dynamic verification techniques and methods. The goal for static verification is to automatically translating OCL constraints to source code-level assertions such as JML specification and CleanJava annotations for formal program verification. The goal for dynamic verification is to automatically translating OCL constraints to executable assertions. 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. In particular, the project focuses on deriving JML assertions and AspectJ aspects from architectural or design constraints written in architecture description languages (ADL) or OCL. Our research has shown that formally-specified design constraints such as class invariants and operation pre and postconditions written in OCL can be systematically translated to code-level annotations written in CleanJava and the resulting annotations can be used in the correctness proof of code [Cheon and Avila 2013]. The approach provides a practical alternative, or complementary technique, to program testing to assure the correctness of software. Our research also showed that runtime checks can mitigate the problem of design drift and corrosion. The key idea is to systematically translate architectural or design constraints written in a formal notation such as OCL and ADL into executable assertions to check them at run-time. The executable assertions can be JML assertions [Jung and Rubio, et al., 2007] [Avila, Flores and Cheon 2008] or AspectJ aspects [Cheon, Avila, Roach, et al. 2009a, 2009b]. Our approach and framework enable runtime verification of design-implementation conformance by detecting design corrosion. Our AspectJ framework is modular and plug-and-playable in that the constraint checking logic is completely separated from the implementation modules that are oblivious of the former. We also found a shortcoming of OCL in its support for qualified associations and proposed a small extension to OCL to make it more expressive [Dove, Barua and Cheon 2014]. In our recent work [Cheon, Cao and Rahad 2016], we proposed to use Java 8 streams for writing more concise and cleaner assertions on a collection. The use of streams in JML can be minimal and non-invasive in the conventional style of writing assertions. It can also be holistic to write all assertions in the abstract state defined by streams.
Last modified: $Id: vericop.html,v 1.1 2019/08/17 05:54:06 cheon Exp $