Where academic tradition
meets the exciting future

Distributed Systems Laboratory (DS Lab)

The Distributed Systems Laboratory is a research laboratory within the Turku Centre for Computer Science (TUCS). It involves a group of researchers from the Department of Information Technologies at Åbo Akademi University. The laboratory is multidisciplinary with background in computer science, software engineering, and mathematics. The mission of the Distributed Systems Laboratory is to develop methods, techniques and tools that help in the design of correct and dependable distributed systems. The Distributed Systems Design Laboratory was a part of the Centre of Excellence in Formal Methods in Programming, Academy of Finland 2002-07.

Our main areas of expertise are formal methods, control systems, dependable systems, fault tolerance, automated reasoning, verification, trusted networks and services, formal hardware design and quality measurement.

Two research groups:

Formal Methods and Networks Group (Formnet)

In this group we focus on modeling, analyzing, and developing networked systems, from both a qualitative and a quantitative point of view. We are interested in wireless sensor networks, mobile networks, peer-to-peer networks, multi-core systems, network-on-chip architectures and study trustworthiness as well as location-, context-, and energy-awareness. We are working on discovering suitable language abstractions for capturing contemporary networked systems and protocols. Our main tools at the moment consist of formal approaches such as the action systems formalism, Event-B, and statistical model checking. Our favorite modeling methods consist of abstraction and refinement. We use the Rodin platform to correctly model networked systems and to prove various properties for the systems we model.

Leader: Doc. Luigia Petre

Research Themes

Integrated Design of Quality Systems group (InDeQS)

The Integrated Design of Quality Systems Group is a research group within the Distributed Systems laboratory that focuses their research on integrating methods and tools in the development of high quality systems. In order to ensure the quality of the systems, formal verification techniques are used to guarantee the correctness of the systems. The group is are also interested in increasing the flexibility and maintainability of formal methods in the design process and to evaluate the benefit of this via metrics and measurements.

Leader: Doc. Marina Waldén

Research interests

Research Unit Web Page: https://research.it.abo.fi/research/distributed-systems-laboratory

Leader of the unit

Luigia Petre Marina Waldén


Pontus Boström Mats Neovius Marta Olszewska

Doctoral Students

Petter Sandvik Moigan Kamali Sergey Ostroumov Jonatan Wiik Masoumeh Parsa

Research Groups

Formal Methods and Networks (FormNet)

Leaders: Luigia Petre
Members:       Mats Neovius
Petter Sandvik
Moigan Kamali

Integrated Design of Quality Systems (InDeQS)

Leaders: Marina Waldén
Members:       Pontus Boström
Marta Olszevska
Sergey Ostroumov
Jonatan Wiik
Masoumeh Parsa


EFFIMA/DiHy+Digihybrid (2009–2014, FIMECC SHOK)

eDiHy (2011–2014, Academy of Finland)

FResCo (2013–2015, Academy of Finland)

ADVICeS (2013–2017, Academy of Finland)


Click here to see the full list of publications from the TUCS Publication Database

The latest updated publications:

Mojgan Kamali, Massimo Merro, Alice Dal Corso, AODVv2: Performance vs. Loop Freedom. In: A Min Tjoa, Ladjel Bellatreche, Stefan Biffl, Jan van Leeuwen, Jiři Wiedermann (Eds.), SOFSEM 2018: Theory and Practice of Computer Science, 337–350, Springer, 2018.

Aivo Anier, Jüri Vain, Leonidas Tsiopoulos, DTRON: A Tool for Distributed Model-Based Testing of Time Critical Applications. Proceedings of the Estonian Academy of Sciences 66(1), 1–16, 2017.

Usman Sanwal, Luigia Petre, Ion Petre, Stepwise Construction of a Metabolic Network in Event-B: The Heat Shock Response. Computers in Biology and Medicine (91), 1–12, 2017.

Marin Aranitasi, Benjamin Byholm, Mats Neovius, Quantifying Uncertainty for Preemptive Resource Provisioning in the Cloud. In: A Min Tjoa, Roland R. Wagner (Eds.), 28th International Workshop on Database and Expert Systems Applications (DEXA), 127–131, IEEE Computer Society, 2017.

Mojgan Kamali, Luigia Petre, Uppaal vs Event-B for Modelling Optimised Link State Routing. In: K. Barkaoui, H. Boucheneb, A. Mili, S. Tahar (Eds.), Verification and Evaluation of Computer and Communication Systems. VECoS 2017, Lecture Notes in Computer Science 10466, 189–203, Springer, 2017.

Aranitasi Marin, Neovius Mats, Anomaly Detection in Cloud Based Application using System Calls. In: Westphall Carlos Becker, Lee Yong Woo, Duncan Bob, Olmsted Aspen, Vassilakopoulos Michael, Lambrinoudakis Costas, Katsikas Sokratis K., Ege Raimund (Eds.), Cloud Computing 2017, 44–48, IARIA XPS, 2017.

Mats Neovius, Bob Duncan, Anomaly Detection for Soft Security in Cloud Based Auditing of Accounting Systems. In: Donald Ferguson, Víctor Méndez Muñoz, Jorge Cardoso, Markus Helfert, Claus Pahl (Eds.), Proceedings of the 7th International Conference on Cloud Computing and Services Science, 499–506, INSTICC, 2017.

Marta Olszewska, Sergey Ostroumov, Mikołaj Olszewski, To Agile or not to Agile Students (With a Twist) - Experience Report from a Student Project Course. In: Michael Felderer, Helena Holmström-Olsson (Eds.), The Proceedings of the 43rd Euromicro Conference on Software Engineering and Advanced Applications, 83–87, IEEE, 2017.

Sergey Ostroumov, Marina Waldén, Visual Component-Based Development of Formal Models. In: Mira Kajko-Mattsson, Pål Ellingsen, Paolo Maresca (Eds.), The Third International Conference on Advances and Trends in Software Engineering (SoftEng), 43–50, IARIA, 2017.

Jüri Vain, Apneet Kaur, Leonidas Tsiopoulos, Jaan Raik, Maksim Jenihhin, Modeling for Multi-View Interference Analysis of Design Aspects in MPSoC Designs. In: Proceedings of 22nd IEEE European Test Symposium: RESCUE 2017, Workshop on Reliability, Security and Quality, 1–6, KIOS Research Center | University of Cyprus, 2017.

Jüri Vain, Leonidas Tsiopoulos, Vyacheslav Kharchenko, Apneet Kaur, Maksim Jenihhin, Jaan Raik, Multi-Fragment Markov Model Guided Online Test Generation for MPSoC. In: Vadim Ermolayev, Nick Bassiliades, Hans-Georg Fill, Vitaliy Yakovyna, Heinrich C. Mayr, Vyacheslav Kharchenko, Vladimir Peschanenko, Mariya Shyshkina, Mykola Nikitchenko, Aleksander Spivakovsky (Eds.), ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer: Proceedings of the 13th International Conference, ICTERI 2017, Kyiv, Ukraine, May, 2017, CEUR Workshop Proceedings 1844, 594–607, RWTH Aachen University, 2017.

Jonatan Wiik, Pontus Boström, Specification and Automated Verification of Dynamic Dataflow Networks. In: Alessandro Cimatti, Marjan Sirjani (Eds.), Software Engineering and Formal Methods: 15th International Conference, SEFM 2017, Trento, Italy, September 4-8, 2017, Proceedings, Lecture Notes in Computer Science 10469, 136–151, Springer, 2017.

Proceedings of the 29th Nordic Workshop on Programming Theory, TUCS Lecture Notes, 2017.

Kashif Javed, Model-Driven Development and Verification of Fault Tolerant Systems. TUCS Dissertations 223. 2017.

Mojgan Kamali, Massimo Merro, Alice Dal Corso, AODVv2: Performance vs. Loop Freedom. TUCS Technical Reports 1177, TUCS, 2017.

Marta Olszewska, Mikołaj Olszewski, Sergey Ostroumov, Gohar Shah, Haider Rizvi, Bilal Altaf, Experimenting with Event-B and Scrum on Student Project Course. TUCS Technical Reports 1176, TUCS, 2017.