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:

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.

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.

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.

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.

Luigia Petre, Emil Sekerinski (Eds.), From Action Systems to Distributed Systems - The Refinement Approach, Computer and Information Science Series, Taylor & Francis, 2016.

Einar Broch Johnsen, Luigia Petre (Eds.), Theme Issue on Integrated Formal Methods. Software and Systems Modeling 15(4), 2016.

Marta Olszewska, Jeanette Heidenberg, Max Weijola, Kirsi Mikkonen, Ivan Porres, Quantitatively Measuring a Large-Scale Agile Transformation. Journal of Systems and Software 117, 258–273, 2016.

Jonatan Wiik, Pontus Boström, Contract-Based Verification of MATLAB-Style Matrix Programs. Formal Aspects of Computing 28(1), 79–107, 2016.

Andrew Edmunds, Marta Olszewska, Marina Walden, Using the Event-B Formal Method for Disciplined Agile Delivery of Safety-critical Systems. In: Hermann Kaindl, Roberto Meli (Eds.), SOFTENG 2016: The Second International Conference on Advances and Trends in Software Engineering, 1–9, IARIA, 2016.

Andrew Edmunds, Marina Waldén, On Component-Based Reuse for Event-B. In: M. Butler, K.-D. Schewe, A. Mashkoor, M. Biro (Eds.), Abstract State Machines, Alloy, B, TLA, VDM, and Z, Lecture Notes in Computer Science 9675, 151–166, Springer, 2016.

Andrew Edmunds, Marina Waldén, Modelling ‘Operation-Calls’ in Event-B with Shared-Event Composition. In: Leila Ribeiro, Thierry Lecomte (Eds.), Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 10090, 97–111, Springer, 2016.

Johan Ersfolk, Pontus Boström, Ville Timonen, Jan Westerholm, Jonatan Wiik, Otso Karhu, Matti Linjama, Marina Waldén, Optimal Digital Valve Control Using Embedded GPU. In: Janne Uusi-Heikkilä, Matti Linjama (Eds.), Preceedings of the Eight Workshop on Digital Fluid Power, 239–250, Tampere University of Technology, 2016.

Mojgan Kamali, Luigia Petre, Modelling Link State Routing in Event-B. In: Hai Wang, Mounir Mokhtari (Eds.), 21st International Conference on Engineering of Complex Computer Systems, ICECCS 2016, 207–210, IEEE Conference Publishing Services, 2016.

Mats Neovius, A Model for Experience-Based Agent Specific Trust. In: Jaime Lloret Mauri, Mario Freire (Eds.), In proceedings of The Eighth International Conference on Adaptive and Self-Adaptive Systems and Applications, 10–15, IARIA XPS Press, 2016.

Mats Neovius, Luigia Petre, Kaisa Sere, A Theory of Service Dependency. In: John Derrick, Eerke Boiten, Steve Reeves (Eds.), Proceedings 17th International Workshop on Refinement (Refine'15), Oslo, Norway, 22nd June 2015, 209, 112–128, Electronic Proceedings in Theoretical Computer Science (EPTCS), 2016.

Marta Olszewska, Yanja Dajsuren, Harald Altinger, Alexander Serebrenik, Marina Waldén, Mark G. J. van den Brand, Tailoring Complexity Metrics for Simulink Models. In: Rami Bahsoon, Rainer Weinreich (Eds.), Proccedings of the 10th European Conference on Software Architecture Workshops, 1–7, ACM New York, 2016.

Marta Olszewska, Sergey Ostroumov, Marina Waldén, Using Scrum to Develop a Formal Model – An Experience Report. In: Pekka Abrahamsson, Andreas Jedlitschka, Anh Nguyen Duc, Michael Felderer, Sousuke Amasaki, Tommi Mikkonen (Eds.), Product-Focused Software Process Improvement: 17th International Conference, PROFES 2016, Trondheim, Norway, November 22-24, 2016, LNCS 10027, 621–626, Springer International Publishing, 2016.

Jüri Vain, Leonidas Tsiopoulos, Jishu Guin, Developing Multi-View Contracts using Event-B and Uppaal Timed Automata. In: Hai Wang, Mounir Mokhtari (Eds.), 21st International Conference on Engineering of Complex Computer Systems, ICECCS 2016, 126–134, IEEE Conference Publishing Services, 2016.

Mats Neovius, Mauno Rönkkö, Marina Waldén, A Provably Correct Resilience Mediator Pattern. In: Luigia Petre, Emil Sekerinski (Eds.), From Action Systems to Distributed Systems - The Refinement Approach, Computer and Information Science Series, 125–141, Taylor & Francis, 2016.

Jüri Vain, Leonidas Tsiopoulos, Pontus Boström, Integrating Refinement-Based Methods for Developing Timed Systems. In: Luigia Petre, Emil Sekerinski (Eds.), From Action Systems to Distributed Systems: The Refinement Approach, 171 – 185, Taylor & Francis, 2016.

Mojgan Kamali, Luigia Petre, Modelling Link State Routing in Event-B. TUCS Technical Reports 1154, TUCS, 2016.

Mojgan Kamali, Luigia Petre, Uppaal vs Event-B for Modelling Optimised Link State Routing. TUCS Technical Reports 1158, TUCS, 2016.

Marta Olszewska, Sergey Ostroumov, Marina Waldén, Synergising Event-B and Scrum – Experimentation on a Formal Development in an Agile Setting. TUCS Technical Reports 1152, TUCS, 2016.

Jonatan Wiik, Pontus Boström, Specification and Automated Verification of Dynamic Dataflow Networks. TUCS Technical Reports 1170, TUCS, 2016.

Usman Sanwal, Luigia Petre, Ion Petre, Stepwise Construction of a Metabolic Network in Event-B: the Heat Shock Response. TUCS Technical Reports 1160, TUCS, 2016.