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:

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.