Checking Human Machine Interactions


This project will experiment with the use of JPF for checking properties
of systems involving humans, user interfaces and the machine being
controlled. It will focus on expressiveness of relevant properties, as
well as analysis capabilities.


student: Sebastien Combefis <email> <SC>

mentor: Dimitra Giannakopoulou <email> <dimitra.giannakopoulou@…> <DG>


Program & Timeline

This project is funded by the Google Summer of Code (GSoC) program.
It follows the GSoC timeline (start 05/24, finish 08/16).


The sources for this project are available from a Mercurial repository


The first part of the project will involve experimenting with the current
JPF support in order to model human machine interactions and check
properties. As a result, we will identify types or patterns of properties
and analysis capabilities that JPF will need to be extended with.

The second part of the project will involve implementation of the
identified extensions and further experimentation with examples
in order to improve the usability.

We expect to use the following capabilities of JPF:

  • listeners for property verification
  • learning within the compositional verification extension
    for identifying the part of the system behavior that
    needs to be controlled through an interface.

Project Blog

(most recent on top)

2010-05-07 (NR) - project page created
2010-05-21 (DG) - project details added to wiki

Last modified 8 years ago Last modified on 05/21/2010 11:22:00 AM