My research has focused on the design and implementation of specification languages and related tools. My earlier accomplishment in this area is designing the first Larch-style interface specification language for an object-oriented programming language called Larch/Smalltalk. The implementation of Larch/Smalltalk included a graphical user interface, integrated with the ParcPlace Smalltalk system. Larch/Smalltalk made several contributions to specification language design. It was the first object-oriented formal specification language in the Larch style. It features a clear separation of the notions of type and class. Types in Larch/Smalltalk are the unit of abstraction for specifications, and specify the protocols of objects. A type can be implemented either by a single Smalltalk class, or by several classes. Behavioral subtyping organizes types according to behavioral relationships. The language also supports specification inheritance and generic polymorphism, in addition to subtype polymorphism, at the level of types. An article on Larch/Smalltalk was published in the ACM Transactions on Software Engineering and Methodology, one of the most prestigious journals in the field (Cheon and Leavens, 1994a).
Another earlier accomplishment is the design of the formal specification language Larch/C++. I was a major collaborator in this effort. Larch/C++ uses several ideas from Larch/Smalltalk in the context of a C++. I developed the original parser, preprocessor, and reference manual for Larch/C++. I also co-authored two papers about Larch/C++; the paper "Preliminary Design of Larch/C++" was presented at the First International Workshop on Larch (Leavens and Cheon, 1992), and a tutorial "A Quick Overview of Larch/C++" was published in a peer-reviewed journal, Journal of Object-Oriented Programming (Cheon and Leavens, 1994b).
My recent accomplishment is the contributions that I made to the
Java Modeling Language (JML),
an interface specification language for the
Java programming language. As part of my Ph.D. dissertation research I
developed a runtime assertion checking compiler (jmlc)
for JML. The
contributions of my work on the runtime assertion checker are not just
in the software, however. I has made significant and important
contributions to the design of JML and its semantics, for example,
distinction between static and instance invariants,
semantics of specification inheritance,
and privacy issues in specifications.
The most significant contributions of my
dissertation work include (1) supporting abstraction in run-time
assertion checking, (2) systematic support for handling undefinedness
in assertions, and (3) substantial support for specification
inheritance. I have written roughly 70,000 source lines for the JML
tools (including code, documentation, specifications, test cases, and
makefiles).
My publications, especially on JML have both been significant and had a far-reaching impact. This can be seen from the number of citations of these publications. For example, my paper (joint with Burdy, Cok, and others) on JML tools has been cited (according to Google Scholar) 344 times. My paper on unit testing (with Leavens) has been cited 145 times, and my dissertation has been cited 145 times. Furthermore, a popular college textbook on programming languages (Tucker and Noonans, Programming Languages, Principles and Paradigms, second edition, McGraw-Hill, 2007) includes sections devoted to JML, based largely on my dissertation work.
My most recent accomplishments include several extensions to the JML language. With a graduate student, Ashaveena Perumandla, I introduced the notion of protocol contracts to JML (Cheon and Perumandla, 2007; refer to the project website). In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, that we referred to as protocols. However, protocols are essential properties of reusable object-oriented classes and application frameworks. We made an extension to JML to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and postconditions and to specify them in a regular expression-like notation. We defined the semantics of our extension formally and used it as a foundation for extending the JML tools to support protocol contracts. A graduate student, Carlos Rubio, and I recently proposed an approach for formally specifying access control assumptions of a Java program module and enforcing them at run-time. We called such an assumption or assertion an access control contract. For this, we introduced two new built-in JML language constructs and defined their semantics by translating them into runtime checking code. Our approach will contribute to providing a foundation for formally reasoning about security properties of Java programs and facilitate practicing the "security by design" principle.
My current work focuses on re-developing the JML tools by enhancing JML's tool infrastructure. The goal is to update the JML language and its tool support to reflect recent language changes in Java, e.g., generics, and to make JML's software infrastructure more extensible so that it can be used as a research platform for Java-based formal methods.
My recent and current work in the design and implementation of specification languages and related tools has been supported by the following two NSF research grants.
Last modified: $Id: speclang.html,v 1.5 2009/03/06 10:07:56 cheon Exp $