• Process Calculi and the SENSORIA Approach.
  

 

The calculi for service specification and analysis play a central role in SENSORIA. They are needed both to describe, discover and compose systems and to prove that their behaviour is consistent with the expectation of the designer. They have been used as target of services specifications provided in abstract modelling languages like SRML or UML4SOA but have been also equipped with tools for both qualitative and quantitative analysis and have been the basis for defining abstract machine that guarantee provably correct implementations of services.

 

 

In "A unifying formal basis for the SENSORIA approach" the evidence is given that the formal methods in SENSORIA, while spanning over a variety of theories and employing diverse mathematical results, are coherent and refer to well understood kernel of theoretical computer science. 

 

For the qualitative analysis of services, we have:

• equipped process calculi with type systems that enable checking conformance of services with contracts and deadlock freedom of the outcome of the composition of given services;
• introduced temporal logics that permits naturally expressing typical service-oriented properties like session data correlation, service availability, service responsiveness, and by means of an on-the fly verification engine, the verification of the specified properties;
• used flow logics to statically compute over-approximations of services behaviour and guarantee expected properties;
• introduced behavioural relations the permit studying the relationships between concrete descriptions of services (close to the implementation) and abstract descriptions (providing the specification).

For the quantitative analysis of services, we have:

• defined stochastic variants of the calculi that allows the description of services whose basic actions are paired with a rate expressing their frequency and enables us to analyze services by using markovian techniques and model checking of stochastic logic.
• defined a service-oriented stochastic logic - a probabilistic, timed, temporal logic, that is resource oriented to address open-endedness of service oriented computing.