Distributed systems and parallel programs are notoriously prone to errors caused by subtle differences in the relative execution orderings of the components of the system. In order to avoid such errors systems should be carefully specified and analyzed. The international research in this area, often called simply``concurrency'', has been active in the 1980's and has resulted in numerous specification methods and models for this purpose, e.g. state transition systems, Petri nets, process algebras and temporal logics. Elegant and rich theories supporting these models have made the models even more useful. Results in these theories can be employed in computer based analysis tools for checking and verifying concurrent real life software.
An important class of distributed algorithms consists of computer communication protocols. We have worked with the problems of protocol analysis since 1984. We begun by constructing a reachability analysis tool PROTAN88 designed for protocols specified with an extended state transition model (ESTELLE specification language). In the 1980's this tool has been tried out by us in analyzing several well-known real-life protocols like X.25, FTAM and X.411/P1. Some of our improvement suggestions were included in the FTAM state tables published by CCITT and ISO.
Lately our work has been more conceptual and theoretical. Various equivalence concepts have been studied in process algebra contexts (Milners CCS and ISO LOTOS) and the equivalence preserving minimization of labeled state transition systems has been studied. We have been especially interested in divergence preserving behavioural equivalences and preorders. These equivalences allow neat comparisons between bisimulation and failures based equivalences and congruences. If an equivalence does not preserve divergences, it is difficult to analyze liveness properties after equivalence preserving transformations of a transition system. Many aspects of temporal logic are closely related with equivalences and preorders. Research topics in this area include fixpoint calculi (mu-calculi) and automata on infinite objects.
A recurrent theme in our research is to make analysis and verification feasible for concurrent systems of realistic size. That is why the dominant goal in our research is to understand and support compositional (or modular) specification and verification of concurrent systems. We have been e.g. analyzing and applying the weakest equivalence (CFFD-equivalence) preserving deadlocks and linear next-timeless linear temporal formulae. Our research employs case analyses (often computer communication protocols) to ensure the practical usefulness of the theoretical concepts.
At the university of Helsinki we have been developing a computer-based verification tool BIDMIN allowing us to minimize labeled transition systems with respect to divergence preserving bisimilarity and branching bisimilarity as well as the related congruences. We also often use a LOTOS oriented verification tool ARA TOOLS developed at the Technical Research Centre of Finland. ARA TOOLS is a prototype aiming at industrial quality.
Current members of the MOCO group are Prof. Martti Tienari (group leader), Dr. Jaana Eloranta, Dr. Roope Kaivola, M.Sc. Vesa Hellgren, Ph.Lic. Timo Karvi and M.Sc. Päivi Kuuppelomäki. As an associate member of the group we have professor Antti Valmari (Tampere University of Technology, Software Systems Laboratory) who is the chief designer of ARA TOOLS. Our concurrency group is participating (1994-96) in European COST247-project ``Verification and Validation Methods for Formal Descriptions''.
Home page: http://www.cs.helsinki.fi/research/moco/