P.O.BOX 26 (TEOLLISUUSKATU 23), FIN-00014 UNIVERSITY OF HELSINKI, FINLAND
|
|
|
P.O.BOX 26 (TEOLLISUUSKATU 23), FIN-00014 UNIVERSITY OF HELSINKI, FINLAND |
After this first period the work of our group has been more conceptual and theoretical. Various equivalence concepts have been studied in process algebra contexts. The group has been especially interested in divergence preserving behavioural equivalences and preorders as well as minimizations. Furthermore, the group has examined the preservation of temporal logic properties in the construction of reduced models based on divergence-sensitive equivalences and preorders. The relations of temporal logics, particularly mu-Calculus or fixed-point temporal logics,have also been studied. A recurrent theme in our research has been the analysis and verification of concurrent systems of realistic size. We have analyzed the CFFD-equivalence which is the weakest equivalence preserving deadlocks and linear temporal logic formulae.
Partially defined specifications are specifications which do not contain all the execution alternatives that are present in the protocol. The initial points of the missing execution branches are explicitly marked. These kind of specifications can be applied in many situations. The most important applications seem to be the stepwise verification of protocols and a partial generation of a global state graph.
We have also studied how the CFFD-equivalence based compositonal verification techniques could be used in the context of automata theoretic verification of real-time systems.
The other areas that has recently been taken into our research program are the verification of cryptographic protocols using strand spaces, the verification of mobile processes and techniques of incorporating fairness constraints in the automata theoretic verification.