Global and distributed communication infrastructures, like the Internet, but also "software-intensive" systems,  support  an ever  larger part of our  activities. Each of these infrastructures has been designed to provide particular services to its users, for example providing:

• a reliable means of transportation of information (e.g. Internet),
  
• extended interaction of the type Client/Server (e.g. Web);
  
• privacy and confidentiality (e.g. Virtual Private Networks);
  
• quality of service (e.g. telephone network);
  
• sharing of computing power (e.g. GRID);
  
• ubiquitous computing (UC);
• distributed computing capacity on micro components;

Such infrastructures are evolving more and more into distributed systems that are composed of an ever growing number of heterogeneous components, which in turn may be of small dimensions. The growing human dependency on applications that are based on such infrastructures create the need to guarantee their reliability, security, consistency, robustness, usability and efficiency. It is therefore necessary to develop new formal techniques and related tools that can be used during the early stages of their design in order to guarantee that those systems satisfy the above mentioned desirable properties.


The main research objectives of this project are:

1. Development of formal specification languages for the modelling of highly complex systems.
2. Development of automatic tools to support the verification of functional and non-functional properties.
3. Integration and unification of the various models, styles and specification paradigms.

 

Last update: April 16, 2010