Suggested Extensions for Future Work

We list here some project suggestions related to our previous work in the MulSaw project. Some of these suggestions are entry-level and suitable for undergraduates, while others can lead to Master's and even Ph.D. theses. We would like to hear from you if you are interested in collaborating with us on some of these or other ideas. You can send us an email.

Alloy Annotation Language (AAL)

Implement dynamic checking (with Basel Al-Naffouri )

We are currently working on translating AAL annotations to Java assertions that can be checked at runtime.

Extend AAL

This project would extend AAL with primitive types, arrays, and Java method invocations.

Translate JML to AAL

The Java Modeling Language (JML) is a behavioral interface specification language that can be used to specify the behavior of Java modules. A translation from JML to AAL would enable using the Alloy Analyzer to provide static checking of JML specifications.

Translate AAL to JML

The JML toolset provides dynamic checking of Java programs annotated with JML. A translation from AAL to JML would enable using the existing JML toolset to provide dynamic checking of Java programs annotated with AAL.

Use Korat search for AAL

This project would consider using Korat to generate structures for the Java predicates that are produced by the AAL to Java translation.

Implement static checking

This project involves translating Java code and AAL annotations into Alloy. This is the topic of Mandana Vaziri's Ph.D. thesis.

Verification

Prove Alloy specs (with Kostas Arkoudas)

We are exploring the use of theorem provers, in particular the Athena Denotational Proof Language, for automated generation of machine-verifiable proofs of Alloy specifications.

Extend Alloy analysis for verification

The analysis of the Alloy Analyzer is valid only for instances within the given bounds. This project would explore cases where results of this analysis can be generalized to hold for instances of any size.

Korat

Use Korat search for Alloy specs

This project explores "directly" solving for instances of Alloy-like specifications, using state-space pruning of Korat.

Use Korat for white-box testing

We have so far used Korat for specification-based, or black-box, testing. We would like to use Korat to "directly" generate inputs that satisfy a specified coverage criteria, such as statement or branch coverage, while also satisfying the precondition, such as acyclicity.

Use genetic algorithms to guide Korat search

This project would explore using genetic algorithms to guide Korat's search of a predicate's input space; the genetic search can use a fitness measure based on the predicate's executions.

Add symbolic execution to Korat search

Korat currently treats data, such as integer variables, by enumerating the range of possible values specified by the finitization. We would like to add symbolic execution to Korat's search and use it in conjunction with off-the-shelf constraint solvers.

Test TSAFE implementation

The Tactical Separation Assisted Flight Environment (TSAFE) is a decision support tool for air traffic controllers. This project would use Korat to test the TSAFE prototype under development in LCS.

Use model checking for generating inputs

This project would evaluate using a model checker for generating structures from sequences of method invocations. The model checker can use the method preconditions to constrain these invocation sequences so that they produce only valid structures.

Translate repOk to Alloy

This project would evaluate an alternative approach to finding inputs that satisfy repOk: translate repOk to Alloy and then use the Alloy Analyzer. There are several ways to translate repOk, e.g.:
  1. translate repOk to Alloy using finite scope
  2. extract structural invariants in Alloy (joint work with Viktor Kuncak)
  3. translate to Alloy using Daikon; use test inputs generated from repOk and feed them to Daikon to detect structural invariants

TestEra

Generate test inputs from algebraic specifications (a-la-TestEra)

Generate instances of data structure abstractions and use each instance to build one or several concrete inputs.

Back to the MulSaw webpage