• Quantitative evaluation of the availability of distributed applications:

The current state of the art of micro processors and wireless networking technologies open several new development directions for car manufacturers. There is the possibility that in the near future the on-board computers of vehicles will be constantly connected to the environment (neighbouring cars, and the fixed infrastructure). Applications like the distributed black box,  ambulance warning and coordinated traffic jam avoidance will make our journeys safer and more confortable.

On the other hand these distributed applications are required to have a certain level of service availability, the provision of which is even theoretically questionable, since wireless connections are well known to be inherently unreliable.

In our work we created a stochastic modelling formalism capturing the statistical failure-repair properties of components and their relationships. The methodology is used to evaluate the availability measures of distributed applications along deterministic scenarios.

• Formal modeling and analysis of business workflows:
  

Electronic data storage solutions are used by even non-IT organisations for decades. The observable tendency of the last five years shows that IT solutions gain control over even crucial business processes of companies. This level of responsibility generated need for formal techniques to model and verify such workflows.

I investigated the possibilities to model BPEL workflows to facilitate formal verification using model-checkers in practice. The latest results indicate that our approach based on data abstraction and transition systems makes our goal feasible to achieve.