You are here: TUCS > RESEARCH > Research Units > Distributed Systems Laboratory (DS Lab)
Distributed Systems Laboratory (DS Lab)
The Distributed Systems Laboratory has been a research laboratory within the Turku Centre for Computer Science (TUCS) for more than one decade. The researchers belong to the Department of Information Technologies at Åbo Akademi University and their background is in computer science and software engineering. The mission of the Distributed Systems Laboratory is to develop methods, techniques and tools facilitating the design of correct and dependable parallel and distributed systems. The Distributed Systems Laboratory was a part of the Centre of Excellence in Formal Methods in Programming, Academy of Finland during 2002-07. We apply our modelling and verification methods to systems ranging from distributed algorithms to large distributed networks, processor farms, and multi-core architectures. Our research involves a significant range of industrial software-intensive systems in areas such as communication technology, digital hydraulics, satellite software, and various control systems.
Our main areas of expertise are formal methods, control systems, dependable systems, fault tolerance, automated reasoning, verification, trusted networks and services, and formal hardware design.
Formal Methods. Our laboratory has a long experience on working in the field of formal methods – precise analysis frameworks for developing reliable software and systems. We have traditionally based our research on the Action Systems/Refinement Calculus framework for distributed systems proposed by Back, Sere and Waldén. This framework especially supports the stepwise refinement approach to the design of correct systems. The related formal method Event-B, that was developed based on Action Systems, provides tool support (the Rodin platform) for correct-by-construction system development.
Control Systems. Our expertise related to control systems consists in modelling and analysing the control loop via the so-called system approach. The system approach is firmly based on stepwise refinement techniques. It gives structure to the design of complex distributed and control systems and helps in managing the derivation task. The approach turned out to be extremely successful and was further developed from theory to practice in a series of EU projects (FP5 MATISSE 2000-2003, FP6 RODIN 2004-2007, FP7 DEPLOY 2008-2012) into a method ready to be deployed by industrial users. A more recent application of the system approach is on developing digital hydraulic controllers, based on Simulink and Contract-Based Design.
Dependable Systems. We have a strong track record in developing formal design theories for highly dependable systems. We focus on modelling safety-critical and fault tolerant systems from various domains – from traditional control systems to self-adapting multi-agent applications. We work on interfacing formal models with safety analysis techniques, creating patterns and process guidelines for modelling various aspects of dependability as well as proof-based verification and model-checking of essential dependability properties. We are also actively involved into extension refinement-based development method with stochastic reasoning and integration with probabilistic model checking.
Automated Reasoning. We heavily employ and contribute to the development of the Rodin platform, a theorem prover tool for the correct development of systems in Event-B. In addition to providing a user interface for editing Event-B models, the proving process is closely integrated with the modelling process, encouraging proof-based model improvement. We also work with model-based verification in the Event- B model checker ProB and experiment with existing probabilistic model checkers. Moreover, we use simulation together with formal modelling based on the Simulink tool. We have also developed tool support (VERSÅA) to verify Simulink models.
Trusted Networks and Services. As pervasive computing, mobile agent systems and services are becoming a part of our everyday life, the correctness and trustworthiness of such systems needs to be ensured. We apply our expertise in rigorous software development methods to such diverse topics as service-oriented development of (mobile) distributed systems, ad hoc, peer-to-peer and sensor networks, grid computing, component-based design etc. In particular, we propose an approach to deriving fault tolerant middleware for mobile agent systems and demonstrate how to reason about safety and data integrity of critical multi-agent system by refinement.
Formal Hardware Design. Formal hardware verification has become increasingly popular in industry, where new methods and tools are now in demand for the formal verification of digital circuits. Our work focuses on developing new hardware design and verification methods for both asynchronous and synchronous circuits as well as such novel hardware platforms as system-on-chips (SoC), 2D and 3D network-on-chips (NoC), and Multi-core. We have a strong cooperation with the (forthcoming) Embedded Computer and Electronic Systems laboratory at University of Turku in this area.
Research Unit Web Page: https://research.it.abo.fi/research/distributed-systems-laboratory
Co-leader of the unit
Luigia Petre Elena Troubitsyna Marina WaldénSenior Researchers
Linas LaibnisResearchers
Petr Alexeev Pontus Boström Mats Neovius Marta Olszewska Anton Tarasyuk Leonidas TsiopoulosDoctoral Students
Kashif Javed Maryam Kamali Sergey Ostroumov Inna Pereverzeva Yuliya Prokhorova Petter SandvikProjects
RECOMP
Reduced Certification Costs for trusted Multi-core Platforms. The project is an ARTEMIS Joint Undertaking project during 2010-2013 financed by EU. Our laboratory is responsible for the component based design methods for trusted multi-core based systems relying on contract based component models, as well as utilisation of formal methods with respect to safety critical standards.
ASSURE
Autonomic Software-intensive Systems: foundations of safety and resilience. The goal of this project funded by the Academy of Finland during 2010 – 2013 is to enhance safety and resilience of critical software-intensive systems via creating a system-health monitoring framework.
DECO
Formal Dependability-Explicit development model for Complex software-intensive systems. The Academy of Finland funded project (2011 – 2012) aims at creating a formal model-driven approach that facilitates design of highly dependable systems.
eDiHy
Energy Efficient Digital Hydraulic Hybrid Machines. The project is funded by the Academy of Finland during 2011-2014. Within this project we investigate a contract-based methodology for the design of control systems relying on formal software construction techniques and simulation tools, as well as building fault-tolerant platforms for reliable software.
EFFIMA/DiHy
Digital Microhydraulics. This is a project within Fimecc/EFFIMA/MeKo SHOK for the period 2009-2013. The goal of the project is to develop second generation digital hydraulic valves that are energy efficient, as well as to improve controllability and fault tolerance of control systems via developing modular control code.
EFFIMA/Digihybrid
Regenerative hydraulic hybrid with digi-valve and multi chamber cylinder technology. This is a Fimecc/EFFIMA/MeKo SHOK project financed during 2011-2014. The goal of the project is to reduce hydraulic losses using a regenerative, multi-chamber cylinder approach and to prove safety and reliability of the software for the digital hydraulic technology. Moreover, the project aims at implementing a fault-tolerant, general purpose platform for digital hydraulic accumulators.
FResCo
High-quality Measurement Infrastructure for Future Resilient Control Systems. This project is funded by the Academy of Finland 2013 - 2015 as a cooperation with three national strategic SHOK centers: TIVIT, FIMECC and CLEEN. The project is implemented as a consortium of Åbo Akademi University with the University of Eastern Finland. In the project we will provide formal foundations for environmental measuring infrastructures, leading to reusable solutions for future resilient control systems. To reach this goal, we plan to integrate the environmental measuring within the development process, as well as to employ formal means for assessing context-awareness. Our methodology will be tested via existing industrial sensor networks and living labs.
Publications
Click here to see the full list of publications from the TUCS Publication Database
The latest updated publications:
Alexei Iliasov, Elena Troubitsyna, Linas Laibinis, Alexander Romanovsky, Kimmo Varpaaniemi, Dubravka Ilic, Timo Latvala, Developing Mode-Rich Satellite Software by Refinement in Event-B. Science of Computer Programming 78(7), 884–905, 2013.
Maryam Kamali, Linas Laibinis, Luigia Petre, Kaisa Sere, A Distributed Design of a Network Recovery Algorithm. International Journal of Critical Computer-Based Systems 4(1), 45–68, 2013.
Kristian Lumme, Luigia Petre, Petter Sandvik, Kaisa Sere, A Formal Approach to H.264 Video Decoding on Multicore Systems. International Journal of Critical Computer-Based Systems 4(1), 3–26, 2013.
Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, A Refinement-Based Approach to Developing Critical Multi-Agent Systems. International Journal of Critical Computer-Based Systems 4(1), 69–91, 2013.
Petr Alexeev, Pontus Boström, Marina Waldén, Mikko Huova, Matti Linjama, Kaisa Sere, Fault-tolerant Scheduling of Stateful Tasks in Uniprocessor Real-time Systems. In: César Benavente-Peces, Joaquim Filipe (Eds.), Proceedings of the 3rd International Conference on Pervasive Embedded Computing and Communication Systems, 189 – 194 , SCITEPRESS, 2013.
Elena Troubitsyna, Towards Formal Specification of Autonomic Control Systems. In: Dini Petre, Elena Troubitsyna (Eds.), The Fourth International Conference on Adaptive and Self-Adaptive Systems and Applications, 109–114, IEEE Computer Press, 2013.
Elena Troubitsyna, Safety Analysis for Architecting Safety-Critical Systems. In: Dave West (Ed.), Proceedings of 30th International System Safety Conference, 250–261, System Safety Society, 2013.
Michael Butler, Stefan Hallerstede, Marina Waldén (Eds.), Proceedings of the 4th Rodin User and Development Workshop, TUCS Lecture Notes, 2013.
Anton Tarasyuk, Formal Development and Quantitative Verification of Dependable Systems. TUCS Dissertations 156. 2013.
Mats Neovius, Formal Stepwise Development of an In-House Temperature Control System. TUCS Technical Reports 1078, 2013.
Sergey Ostroumov, Leonidas Tsiopoulos, Juha Plosila, Kaisa Sere, Generation of Structural VHDL Code with Library Components from Formal Event-B Models. TUCS Technical Reports 1073, 2013.
Inna Pereverzeva, Linas Laibnis, Elena Troubitsyna, Markus Holmberg, Mikko Pöri, Formal Modelling of Resilient Data Storage in the Cloud. TUCS Technical Reports 1076, 978-952-12-2887-2, 2013.
Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis, Dubravka Ilic, Timo Latvala, Formalisation of an Industrial Approach to Monitoring Critical Data. TUCS Technical Reports 1070, TUCS, 2013.
Petter Sandvik, Formal Stepwise Development of an In-House Lighting Control System. TUCS Technical Reports 1079, 2013.
Marina Waldén, Luigia Petre (Eds.), The 22nd Nordic Workshop on Programming Theory (NWPT 2010). The Journal of Logic and Algebraic Programming 81(3), 2012.
Masoud Daneshtalab, Maryam Kamali, Masoumeh Ebrahimi, Siamak Mohammadi, Ali Afzali-Kusha, Juha Plosila, Adaptive Input-Output Selection Based On-Chip Router Architecture. Journal of Low Power Electronics (JOLPE) 8(1), 11–29, 2012.
Sergey Ostroumov, Leonidas Tsiopoulos, Formal Development of Hierarchical Agent-Based Monitoring Systems for Dynamically Reconfigurable NoC Platforms. International Journal of Embedded and Real-Time Communication Systems (IJERTCS) 3(2), 40–72, 2012.
Yuliya Prokhorova, Linas Laibinis, Elena Troubitsyna, Kimmo Varpaaniemi, Timo Latvala, Deriving a Mode Logic Using Failure Modes and Effects Analysis. International Journal of Critical Computer-Based Systems 3(4), 305–328, 2012.
Jesper Berthing, Pontus Boström, Kaisa Sere, Leonidas Tsiopoulos, Jüri Vain, Refinement-Based Development of Timed Systems. In: Diego Latella, Helen Treharne (Eds.), 9th International Conference on Integrated Formal Methods (iFM 2012), Lecture Notes in Computer Science 7321, 69–84, Springer, Heidelberg, 2012.
Jerker Björkqvist, Luigia Petre, Karl Rönnholm, Dragos Truscan, Integrating Innovation Activities in a Master Level Capstone Project Course. In: Jerker Björkqvist, Mikko-Jussi Laakso, Janne Roslöf, Raija Tuohi, Seppo Virtanen (Eds.), International Conference on Engineering Education, Research Reports 38, 1065–1072, Turku University of Applied Sciences, 2012.
Fredrik Degerlund, Scheduling of Compute-Intensive Code Generated from Event-B Models: An Empirical Efficiency Study. In: Karl Göschka, Seif Haridi (Eds.), Distributed Applications and Interoperable Systems (Proc. of DAIS 2012), Lecture Notes in Computer Science 7272, 177–184, Springer, 2012.
Denisa Diaconescu, Ioana Leustean, Luigia Petre, Kaisa Sere, Gheorghe Stefanescu, Refinement-Preserving Translation from Event-B to Register-Voice Interactive Systems. In: Diego Latella, Helen Treharne (Eds.), 9th International Conference on Integrated Formal Methods (iFM 2012), Lecture Notes in Computer Science 7321, 221–236, Springer, Heidelberg, 2012.
Mikko Huova, Miikka Ketonen, Petr Alexeev, Pontus Boström, Matti Linjama, Marina Waldén, Kaisa Sere, Simulations with Fault-Tolerant Controller Software of a Digital Valve. In: Arto Laamanen (Ed.), Proceedings of the Fifth Workshop on Digital Fluid Power - DFP12, Tampere, Finland, 223–242, Tampere University of Technology, Finland, 2012.
Kashif Javed, Elena Troubitsyna, A Case Study in Modeling a Fault-tolerant Satellite System Through Implementation of Dynamic Reconfiguration via Handshake. In: Mannaert,Herwig , Luigi Lavazza, Roy Oberhauser, Elena Troubitsyna, Michael Gebhar, Osamu Takaki (Eds.), The Seventh International Conference on Software Engineering Advances, 44 to 49, IEEE Computer Press, 2012.
Kashif Javed, Elena Troubitsyna, Modelling a Fault-Tolerant Distributed Satellite System. In: Lasse Berntzen, Katya Toneva, Abdulrahman Yarali (Eds.), The Second International Conference on Advanced Collaborative Networks, Systems and Applications, 35 to 41, IEEE Computer Press, 2012.
Maryam Kamali, Luigia Petre, Kaisa Sere, Masoud Daneshtalab, Refinement-Based Modeling of 3D NoCs. In: Farhad Arbab, Marjan Sirjani (Eds.), 4th IPM International Conference on Fundamentals of Software Engineering, Lecture Notes in Computer Science 7141, 236–252, Springer, 2012.
Kashif Javed, Elena Troubitsyna, Designing a Fault-Tolerant Satellite System in SystemC. In: Hermann Kaindl, Leszek Koszalka, Herwig Mannaert, Marko Jäntti, Petre Dini (Eds.), ICONS 2012, The Seventh International Conference on Systems, 49–54, IEEE Computer Press, 2012.
Luigia Petre, Petter Sandvik, Kaisa Sere, Node Coordination in Peer-to-Peer Networks. In: Marjan Sirjani (Ed.), COORDINATION 2012, Lecture Notes in Computer Science 7274, 196–211, Springer-Verlag GmbH Berlin Heidelberg, 2012.
Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, Formal Development of Critical Multi-Agent Systems: A Refinement Approach. In: 9th European Dependable Computing Conference (EDCC 2012), 156–161, IEEE Computer Society, 2012.
Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, Formal Goal-Oriented Development of Resilient MAS in Event-B. In: Mats Brorsson, Luís Miguel Pinho (Eds.), 17th International Conference on Reliable Software Technologies (Ada-Europe 2012) , Lecture Notes in Computer Science 7308, 147–161, Springer, Heidelberg, 2012.
Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, A Case Study in Formal Development of a Fault Tolerant Multi-Robotic System. In: Paris Avgeriou (Ed.), Proceedings of the 4th International Workshop on Software Engineering for Resilient Systems (SERENE 2012), Lecture Notes in Computer Science 7527, 16–31, Springer-Verlag Berlin Heidelberg, 2012.
Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, Development of Fault Tolerant MAS with Cooperative Error Recovery by Refinement in Event-B. In: Fuyuki Ishikawa, Alexander Romanovsky (Eds.), Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, 1–7, ACM CoRR, 2012.
Yuliya Prokhorova, Elena Troubitsyna, Linking Modelling in Event-B with Safety Cases. In: Paris Avgeriou (Ed.), Proceedings of the 4th International Workshop on Software Engineering for Resilient Systems (SERENE 2012), Lecture Notes in Computer Science 7527, 47–62, Springer-Verlag Berlin Heidelberg, 2012.
Petter Sandvik, SPECTA: A Formal Specification Language for Content Transfer Algorithms. In: Uwe Wolter, Yngve Lamo (Eds.), 24th Nordic Workshop on Programming Theory, Reports in Informatics 403, 81–83, University of Bergen, 2012.
Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna, Timo Latvala, Laura Nummila, Formal Development and Assessment of a Reconfigurable On-Board Satellite System. In: Frank Ortmeier, Peter Daniel (Eds.), Proceedings of 31st International Conference on Computer Safety, Reliability and Security (SAFECOMP 2012), Lecture Notes in Computer Science 7612, 210–222, Springer-Verlag Berlin Heidelberg , 2012.
Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis, Formal Modelling and Verification of Service-Oriented Systems in Probabilistic Event-B. In: John Derrick, Stefania Gnesi, Diego Latella, Helen Treharne (Eds.), Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012, Lecture Notes in Computer Science 7321, 237–252, Springer, 2012.
Elena Troubitsyna, Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements. In: Fuyuki Ishikawa, Alexander Romanovsky (Eds.), Proceedings of DS-Event-B 2012: Workshop on the experience of and advances in developing dependable systems in Event-B, 1–7, ACM CoRR, 2012.
Luigia Petre, Kaisa Sere, Marina Waldén, Location-Awareness with Action Systems. In: Paulo Alencar, Donald Cowan (Eds.), Handbook of Research on Mobile Software Engineering - Design, Implementation, and Emergent Applications, 1, 463–483, IGI Global, 2012.
Fredrik Degerlund, Scheduling of Guarded Command Based Models. TUCS Dissertations 152. 2012.
Mats Neovius, Trustworthy Context Dependency in Ubiquitous Systems. TUCS Dissertations 151. 2012.
Fredrik Degerlund, Scheduling Performance of Compute-Intensive Concurrent Code Developed Using Event-B. TUCS Technical Reports 1051, Turku Centre for Computer Science, 2012.
Radu Gramatovici, Luigia Petre, Kaisa Sere, Alin Stefanescu, Gheorghe Stefanescu, Synchronization in Timed Interactive Systems. TUCS Technical Reports 1047, 2012.
Kashif Javed, Elena Troubitsyna, Ensuring Mode Consistency for a Complex Fault-Tolerant Distributed Satellite System. TUCS Technical Reports 1040, Turku Centre for Computer Science, 2012.
Luigia Petre, Petter Sandvik, Kaisa Sere, A Modular Approach to Formal Modelling of Peer-to-Peer Networks. TUCS Technical Reports 1039, Turku Centre for Computer Science, 2012.
Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, Formal Goal-Oriented Development of Resilient MAS in Event-B. TUCS Technical Reports 1033, Turku Centre for Computer Science, 2012.
Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis, A Case Study in a Formal Development of a Fault Tolerant Multi-Robotic System. TUCS Technical Reports 1052, Turku Centre for Computer Science, 2012.
Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna, Timo Latvala, Laura Nummila, Formal Development and Assessment of Reconfigurable On-Board Satellite System. TUCS Technical Reports 1038, Turku Centre for Computer Science, 2012.