My primary research interest is in what I call operational formal methods, practical formal techniques that are applicable to real-life programming. Operational formal methods ranges over broad areas including but not limited to specification languages, verification and reasoning techniques, and support tools. I am particularly interested in combining operational formal methods with object-oriented and aspect-oriented programming paradigms, and my current research focuses on specification language design and implementation, with an emphasis on the object-oriented and aspect-oriented programming.
I am looking for motivated students at the undergraduate, M.S., and Ph.D. levels to contribute research projects in this field. The following is a list of potential topics for students looking for research projects, from individual studies to dissertations.
Past projects:
| Milaap: Unification of Verification and Validation Methods | |
| Area | Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description | The aim of this project is to investigate techniques for unifying several different software verification and validation (V&V) methods, including theorem proving, model checking, testing, and runtime monitoring. In particular we will focus on designing a unified property specification language (UPSL) and integrating existing V&V tools through UPSL. Initially, the tools to be integrated include testing tools, runtime assertion checking tools, and performance monitoring tools. |
| Reference | Milaap, JML |
| Status | Poonam Agarwal, Carlos Rubio |
| OpenJML: Multiple formalisms for JML | |
| Area | Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description | This project will study a way to open up JML to support multiple formalisms. The idea is to design a framework to plug in different specification and verification formalisms, such as functional (e.g., Haskell), equational (e.g., OBJ3), and logic (e.g., Prolog). Initially, the project will focus on the JML-Haskell connection; e.g., can we use Haskell to define vocabulary for writing JML assertions? |
| Reference | JML, Haskell |
| Status | Open |
| Specification and Checking of Performance Contracts | |
| Area | Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description | This project will explore performance contracts and related tools. The focus is on ways to specify and dynamically check the time and space behavior of components in a modular fashion. Performance checking is important because ultimately critical systems must meet both functional and performance constraints. The theory of performance contracts will need to address object-oriented features such as dynamic dispatch and subtyping. Implementation of tools and experimental evaluation are central themes of the project. The project will investigate tools for runtime checking. Specifically, the project will enhance JML with support for specifying time and space constraints. JML's runtime checking support will be extended to check performance contracts. |
| Reference | JML |
| Status | Open |
| Specification Reflection | |
| Area | Programming Languages, Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description | In programming languages, reflection is the ability to discover and manipulate, at runtime, information about program entities, such as objects. This project explores the idea of extending the concept of reflection to behavioral interface specifications. Specification reflection brings many benefits such as runtime access to specifications, customization of assertion checking, and open development of specification-based tools. The project will define meta protocols for specification reflection and implement support tools such as specification compilers. |
| Reference | JML |
| Status | Open |
| RubySL: DBC for Ruby | |
| Area | Programming Languages, Software Engineering |
| Credit | Undergraduate or M.S. project |
| Description | Ruby provides a powerful facility for meta programming. Can we take an advantage of this to implement a DBC tool for Ruby? This project will design and implement a DBC language for Ruby to monitor and to ensure the correctness (i.e., conformance to the DBC specification)b of a program at runtime. |
| Reference | Ruby |
| Status | Open |
| Aspect-Oriented Specification | |
| Area | Programming Languages, Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description | The notion of aspects found in aspect-oriented programming languages such as AspectJ provides an elegant way to support separation of concerns --- an approach to decompose software into modules, each of which deals with, and encapsulates, a particular area of interest, called a concern. We believe that aspects can also play an important role in behavioral interface specification languages (BISL) such as JML to decompose and modularize interface specifications. Aspects are particularly well suited to separate from module specifications non-functional properties such as time and space, concurrency, security, etc. This project will explore aspect-oriented specifications and specification languages, and support tools. Particular topics to study include (1) extension of JML to specify AOP, (2) user-extensible specifications through aspects (e.g., non-functional properties as aspects), (3) tool extension to support aspects. The main challenge is that the semantics of AOL is not clear and modular yet. |
| Reference | JML, AspectJ, Pipa |
| Status | Open |
| JML Light | |
| Area | Software Engineering, Programming Languages |
| Credit | M.S. or Ph.D. project |
| Description | The objective of this project is to study the feasibility and the effectiveness of the layered approach to developing formal behavioral interface specification languages such as JML. Define a subset of JML that is sufficient enough to write effective Design by Contract specifications. The idea is to reduce the notational complexity of JML and to define it in a layered fashion. This will allow for even beginning Java programmers to learn and use JML easily. |
| Reference | JML |
| Status | Open |
| Specification-Based Debugging | |
| Area | Software Engineering, Programming Languages |
| Credit | M.S. or Ph.D. project |
| Description | The objective of this project is to explore the idea of using formal interface specifications as a debugging tool. The project will investigate approaches and techniques for debugging program modules based on their formally specified behaviors. An interactive debugger will be developed to step through the execution of both program code and specification. The debugger will allow one to choose various options of evaluating specifications (e.g., suppressing some assertions), and to explore the program and specification states, in particular, on an assertion violation. The project will evaluate the effectiveness of the specification-based debugging approach. |
| Reference | JML, Java Debugging Interface (JDI) |
| Status | Open |
| Runtime Assertion Checking as Aspects | |
| Area | Programming Languages, Software Engineering |
| Credit | M.S. project |
| Description | Can runtime assertion checking be viewed as an aspect? Translate JML specifications into AspectJ code to check them at runtime. Critically evaluate such an approach and the capability of the AspectJ programming language. |
| Reference | JML, AspectJ, Contract4J |
| Status | Open |
| From Domain Properties to Runtime Assertion Checking | |
| Area | Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description | Problem-domain properties are high-level, abstract properties that are identified and often formalized during domain modeling. Domain properties should hold in general, regardless of implementations. But, how do we ensure that a particular implementation satisfy domain properties? Rather than re-formulating such properties for each implementation, we can automatically derive assertions from formal specifications of domain properties. The derived assertions can be checked or monitored at run-time. The main benefit of such an approach is separation of concerns and reuse of specifications. The domain properties are captured and recorded once and for all as abstract specifications, and later automatically checked on different implementations or various versions of the same implementation (e.g., when an iterative, incremental development approach is used). Thus, it avoids the cost of identifying and formulating the common, essential properties separately for each implementation or version, and such specification-derived assertions may be more effective than hand-written assertions. |
| Reference | JML, AspectJ, ProSpecs |
| Status | Open |
| Concurrency Specification and Checking | |
| Area | Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description |
How to specify multi-threaded programs in JML, and how to check
concurrency specifications at run-time? An important issue that need
be considered is the interplay between concurrency and purity. JML
currently considers the synchronization lock as a kind of side
effect and thus prohibits synchronized methods from being pure. The
main reason is that gaining a lock by a synchronized method may
change the outcome of other concurrent threads. One consequence of
this restriction is that the synchronized methods in the commonly
used java.util.Vector class cannot be specified pure.
|
| Reference | JML |
| Status | Open |
| Automatic Test Case Generation | |
| Area | Software Engineering |
| Credit | Ph.D. project |
| Description | This project will explore techniques for automatically generating test cases from JML specifications. The goal is to completely automate unit testing by feeding generated test cases to the JML/JUnit tool. There are many well-known approaches of specification-based test case generation, some of which may be may be adapted for our purpose, or the JML language may be extended to facilitate automatic test case generation. |
| Reference | UTJML, JML, JUnit |
| Status | Myoung Kim |
| Improving Performance of JML Compiler | |
| Area | Programming Language, Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description | This project will address two different but related performance problems: the performance of the compiler itself (compile time) and the performance of generated bytecode (run time). The main culprit of the compile time efficiency is the double-round compilation strategy and parsing of recursively referenced types. The project will develop and implement an efficient compilation strategy (e.g., incremental compilation, direct bytecode generation, or the use of external symbol tables). How to minimize the runtime overhead due to assertion checking? Based on the performance measurement and analysis, we need to consider several approaches, e.g., minimizing the number of assertion method calls, finding an efficient mechanism for specification inheritance that doesn't use costly reflection facility, minimizing cost of evaluating specification-only fields and method (use of cache?), and using separate threads for assertion checking. |
| Reference | JML |
| Status | Open |
| Implementing Specification Inheritance Using Open Methods | |
| Area | Programming Languages, Software Engineering |
| Credit | M.S. project |
| Description | An approach to support specification inheritance is to emulate, in some way, dynamic dispatch. The current JML compiler uses Java's reflection facility for this. Another possibility is to use MJ's open methods; with this approach we can add dispatch methods even to such classes as Object, thus can eliminate the use of reflection. We may also adapt this approach to implement model methods (as open methods), e.g., equals method for the class Object. The objective of this project is to implement and study the effectiveness of this approach. |
| Reference | JML, MJ |
| Status | Open |
| Compiling Specifications without Source Code | |
| Area | Programming Languages, Software Engineering |
| Credit | M.S. project |
| Description | The current JML compiler requires source code files to compile their specifications, even if the specifications are given as separate, refinement files. Improve the compiler to compile JML specifications without requiring the corresponding Java source code files. The idea is to generate assertion checking code (RAC) such as RAC fields, methods, and classes from specification-only files,q and inject them into to the corresponding bytecode files. This will allow one to use JML to write specifications and runtime assertion check them for library classes, e.g., JDK classes. |
| Reference | JML, BCEL |
| Status | Open |
| Supporting Specification-Only Methods, Classes, and Interfaces | |
| Area | Programming Language, Software Engineering |
| Credit | M.S. project |
| Description | This project will investigate a systematic way of supporting specification-only methods, classes, and interfaces in runtime assertion checking. The current JML compiler supports only model methods in a ad-hoc fashion. |
| Reference | JML |
| Status | Open |
| IDE for UTJML | |
| Area | Software Engineering |
| Credit | M.S. project |
| Description | This project will develop an integrated development environment (IDE) for UTJML, an extension to JML. Developing a GUI to the UTJML compiler (utjmlc) and the testing tool (tgen) will be the essential part of this project. An early prototype is available from the UTJML download page. |
| Reference | UTJML, JML |
| Status | Angelica Perez |
| Specification of Java Foundation Classes | |
| Area | Software Engineering |
| Credit | Undergraduate project |
| Description | JML provides specifications for some of JFC classes, such as collection classes. However, there are still huge number of JFC classes that are needed to be specified. |
| Reference | JML |
| Status | Open |
| GUI for JML/JUnit | |
| Area | Software Engineering |
| Credit | Undergraduate project |
| Description |
Develop a graphical user interface front-end for the JML-JUnit
(jmlunit) tool. The GUI will give more control over
providing user-defined test cases to the automatically generated
test classes. The GUI may look like that of JUnit or Eclipse.
|
| Reference | JML, JUnit |
| Status | Open |
| Javadoc for CRC | |
| Area | Software Engineering, Programming Languages |
| Credit | Undergraduate or M.S. project |
| Description | In our software engineering courses (CS 4310/4311), we use the CRC approach to teach object-oriented analysis and design. Students write detailed design documents based on CRC cards. A significant amount of information from these design documents (e.g., protocol descriptions) is later duplicated in the source programs as some forms of program comments such as Javadoc comments. This leads to a potential problem of the change management and the waste of effort. The underlying idea of this project is to use Javadoc as a CRC recording notation and tool by adding CRC-specific Javadoc tags, e.g., for CRC, subsystems, contracts, and protocols. The main benefit of this approach is no duplication of documents, hypertext CRC cards, and a potential for simultaneous round-trip engineering when integrated with GUI-based CRC tools. |
| Reference | CRC, Javadoc, Doclet API |
| Status | Open |
| Automation of Teaming Forming | |
| Area | Software Engineering |
| Credit | MS project |
| Description | In Software Engineering classes (CS 4310 and 4311), students are grouped into student teams. The goal of this project is to help automate the forming of student teams by developing a support tool. The tool shall suggest an ideal set of teams by considering several variables, such as GPAs, preferences, personality, sex, etc. There are several techniques that can be used or adapted, such as exhaustive search, random search, genetic algorithms, and constraints solving; the effectiveness of each of these approaches need be evaluated experimentally. |
| Reference | None |
| Status | Veronica Ulloa |
| Specifying and Checking Temporal Properties | |
| Area | Software Engineering |
| Credit | M.S. or Ph.D. project |
| Description | How to write temporal properties as a part of an interface specification, and how to check them at run-time? A particular interest is in specifying a sequence of permissible method calls, i.e., the order in which certain operations should be performed. This would be a key component of formally specifying the interfaces of object-oriented frameworks. In terms of JML, a unified theory may be needed to combine and extend invariants and history constraints. |
| Reference | UTJML, JML |
| Status | Ashaveena Perumendla |
| Bib2Web: A Web-based Interface to BibTeX Files | |
| Area | Software Engineering |
| Credit | Undergraduate project |
| Description | Many researchers make use of BibTeX to maintain a bibliographic database. The so-called bib file contains a series of bibliographic entries and is used to generate the bibliography of a document. This project will investigate ways to provide a Web-based interface to bib files so that the bib files can be browsed, searched, and accessed through a Web browser. This will facilitate researchers to publish and share their bibliographic databases through the Internet. |
| Reference | PHP |
| Status | Joel Garcia, Leonardo Ruiz |
| PSP Web Tool | |
| Area | Software Engineering |
| Credit | Undergraduate project |
| Description | PSP stands for Personal Software Process (not Paint Shop Pro :-)) and it helps individual engineers to improve their performance by bringing discipline to the way they develop software. For example, based on various measurements and logging (e.g., time, size, and defects), one can analyze, estimate, and improve various aspects of projects, products, and one's skills (e.g., time, size, and quality). This project will create a Web-based tool for PSP, and is most likely to be a Web programming. |
| Reference | PSP, PHP |
| Status | William Skinner |
| JML Server | |
| Area | Software Engineering |
| Credit | Undergraduate project |
| Description | In CS 3331 and 4311, we use JML both as a Design by Contract tool and a notation for writing formal pre and postconditions. Students write several small-sized specifications and want to check their specifications. However, they are often reluctant to install JML on their laptops or home PCs. It would be nice if they can access JML tools through Web pages. Develop a Web site for this. This project is most likely to be a Web programming. Click >>here<< for a primitive, experimental web page that I wrote in PHP for CS 3331. |
| Reference | JML, PHP |
| Status | Gaspar Guerra, Bravlio Guzman, and Christian Servin |
| GUI for JML Runtime Assertion Checker | |
| Area | Software Engineering |
| Credit | Undergraduate project |
| Description | The problems that this project tries to solve are that it's not easy to identify the cause or source of an assertion violation, and it's not easy to finely control the behavior of the runtime assertion checker. The goal of this project is to develop a graphical user interface for the JML runtime assertion checker (RAC). The GUI will allow one to select or set various RAC options such as the kind of assertion violations to be monitored (e.g., pre- and postconditions, invariants, etc), classes to be monitored, and the way to monitor (e.g., exceptions, logging, etc.). The GUI will also let one to explore the cause of an assertion violation, e.g., by providing detailed information about the assertion violation, perhaps, in the form of the object explorer in Smalltalk. The approach is to modify the JML compiler to support external monitors (e.g., by using the Observer Design Pattern), and to write the GUI as an observer to the runtime assertion checker.The GUI may also be integrated with the JML/JUnit tool. |
| Reference | JML |
| Status | Omar Garcia, Jesus Gamez, and Jorge Ivan Vargas |