Overview
The model checker for Little-JIL allows an analyst to check a process
for deadlock and to prove properties about a process. This model checker
uses
LTSA,
developed at Imperial College by Jeff Kramer and Jeff
Magee. A process is translated to FSP, the input language for LTSA.
The analyst may extend this translation with properties to prove, also
written in FSP.
There are currenlty some limitations on Little-JIL
processes that can be translated to FSP:
- Reactions are not supported.
- Recursion must be manually unrolled prior to translation.
- A parallel step may have at most 4 children. If cardinality is
uses with an unliminted upper bound, the analyzer will use 4 for an
upper bound.
- A choice step should have no more than 5 children.
- The maximum number of exceptions that may arrive at one handler
on one execution of a step is 10.
The Project
A paper describing this work has been accepted to
ISSTA 2004.
Little-JIL is being developed collaboratively with researchers in the
LASER research lab at the University of Massachusetts.
This material is based upon work supported by the National
Science Foundation under Grant No. CCR-9988254. Any opinions,
findings, and conclusions or recommendations expressed in this
material are those of the authors and do not necessarily reflect
the views of the National Science Foundation.
blerner@mtholyoke.edu
