Advanced Tools and Techniques for the Specification and Verification of Systems with Elevated Granularity



Planned Activities

CNR-RSTL project
FM&&T group  CNR-ISTI
Pisa, IT
Friday April 16th, 2010.

  • Project Coordinator
  •   M.Massink AT isti.cnr.it

In this project we address the problem of modelling and analysing concurrent software systems composed of  a large, or even huge, number of interacting components which individually maybe of relatively low complexity. At a high level of abstraction such a general model can be adapted to a variety of artificial systems, both hardware and software, that are inspired by natural systems such as molecular aggregates or cells ("bio-inspired systems"). One may think of groups of software agents that are moving throughout the Web, of control software for sensor networks or for populations of micro-/nano-robots, or also of neural networks. Models such as finite state automata, Petri nets, proces algebras, temporal logics and their relative analysis tools (such as for example Model Checkers) may be very efficient when dealing with "traditional systems" such as network protocols, but without further modifications would be relatively inadeguate to stand the challenge that the analysis of complex systems at a fine granularity pose. It is therefore necessary to "cross-fertilize" these approaches with other concepts and mathematical instruments, among which we would consider for example, statistics, stochastic processes and cellular automata. The goal of this activity is to develop mixed formal techniques to model and analyse such systems and to apply the results to a number of case studies.

Last update: April 16, 2010