Tutorial D      a pre        DAIS - FMOODS 2003  event    -    18 November 2003

Action-based Model Checking 
(and its applications to distributed, mobile, object-oriented systems)

Alessandro Fantechi, Stefania Gnesi


This tutorial aims to present the possibilities offered by model checking tools for the verifcation of distributed, mobile, object-oriented systems, modelled by formalisms derived by process algebras. In process algebras, a system is seen as a set of processes, and each process is characterised by the actions performed in the time by the process. Hence a model checker focusing on actions, rather than states, is able to address the whole word of systems commonly modelled with process algebras, and with languages derived by process algebras. These systems include concurrent and distributed systems, mobile systems, and cover the behavioural aspects of object oriented systems.

The tutorial will first introduce action-based logics interpreted over LTSs. A series of action-based model-checking tools that have been developed in the academic community (such as the model checkers AMC and FMC of the JACK verification environment, or Evaluator and XTL of the CADP verification environment) will then be presented, by showing also examples of their usage, starting from simple concurrent systems. The different strategies adopted by the tools to cope with state explosion problems will also be addressed.

Mobility is then introduced, referring to the pi-calculus formalism as a basic process algebra able to express the typical issues of mobility. Model checking tools operating over pi-calcualus agent are offered by the Mobility Workbench (MWB) and by the HD-Automata Laboratory (HAL). The core of HAL are the HD-automata: they are used as a common format for the various historydependent languages. The HAL environment includes modules which support verification of behavioral properties of pi-calculus agents expressed as formulae of suitable temporal logics.

A most recent approach to the specification of distributed object-oriented processes is by using the proper UML diagrams, such as the state diagrams, to express the behavioural aspects of the overall design. Again, this tutorial will address the issue of how action-based model checking can be upgraded to deal with UML state diagrams: the UMC model checker will be presented as an example.

The open research issues in this field and the possibility of industrial exploitation will be addressed as well.