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
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.
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.
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.:
- translate repOk to Alloy using finite scope
- extract structural invariants in Alloy (joint work with Viktor Kuncak)
- translate to Alloy using Daikon; use test inputs generated from
repOk and feed them to Daikon to detect structural invariants
Generate test inputs from algebraic specifications
Generate instances of data structure abstractions and use each
instance to build one or several concrete inputs.
Back to the MulSaw webpage