|
|
Action de Recherche Coopérative ModoCop
Model checking Of Concurrent Object-oriented Programs
01.01.2002-31.12.2003
|
Contents of this page
This project aims at automatic specification, verification and
symbolic testing of concurrent object-oriented programs. It combines
two important lines of research:
- verification of single-threaded JavaCard programs, which is
mainly theorem-prover based; and
- application of symbolic techniques to generate tests for
embedded applications, which can be analysed using either finite model
checking techniques or symbolic methods that can deal with infinite
state systems.
In particular, the project aims at the development of a framework
for specification, verification and symbolic testing of concurrent
object-oriented programs. This framework should consist of the
following:
- a specification language, which is tailored to specify
properties about concurrent object-oriented programs;
- abstraction techniques, which allow a program to be transformed into an
abstract program model that is amenable to model checking;
- verification techniques which can be used
to verify both the functional behaviour and the interactive behaviour
of the different objects within concurrent object-oriented
programs; and
- symbolic test generation techniques, which allow to check that
an actual, physical implementation still satisfies the behaviour as
described by the verified formal model.
The framework is designed in such a way that it can be applied
to arbitrary concurrent object-oriented programs. JavaCard with
multi-threading will be used as an example instantiation for our
framework, as it is a complete, but still manageable programming
language.
For more information, we have two reports, describing the project's
activities in the first and second year.
Lande (INRIA Rennes/IRISA)
|
Lemme (INRIA
Sophia-Antipolis)
|
Oasis (INRIA
Sophia-Antipolis)
|
Vasy (INRIA Rhône-Alpes)
|
|
Vertecs (INRIA Rennes/IRISA)
|
Several teams
regularly attend ModoCop meetings.
- Start-up meeting, March 13, 2002, Sophia-Antipolis
- Second meeting, July 2, 2002, Rennes
- Third meeting, November 25, 2002, Grenoble
- Fourth meeting, April 17, 2003, Sophia-Antipolis
- Fifth meeting, September 17, 2003, Rennes
- Final Modocop workshop, December 4, 2003, Grenoble
- Development of a specification language for concurrent
object-oriented languages, combining existing specification languages
for Java, such as JML and ESC/Java, and existing specification
languages for concurrent and distributed systems, such as Lotos and
E-Lotos.
- Development of static analysis techniques to extract finite
models of concurrent object-oriented programs in order to be able to
model check them.
- Adaptation of currently existing verification techniques to
JavaCard with multi-threading.
- Adaptation of existing compositional verification techniques
to concurrent open systems.
- Extension of the symbolic test generation techniques
to smart cards.
To compare the different techniques that are used by the Modocop
participants, we have identified a common case study: the
Common Electronic Purse Specifications. Here are some
relevant links:
- The official CEPS site
- Vlad Rusu's work on the
electronic purse, with IF specification and documentation
- Frédéric Lang's NTIF specification: type declarations and
card spec
Further information
For further information, please contact
Marieke Huisman
Last modified: Mon Mar 15 16:09:40 MET 2004