You are here: TUCS > RESEARCH > Research Units > Distributed Systems Laboratory (DS Lab)
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
- Formal and semi-formal methods
- Action systems
- Refinement calculus
- Event-B
- Uppaal
- Statistical model checking
- UML
- Integrating formal methods
- Networked systems
- Wireless sensor (and actor) networks
- Peer-to-peer networks
- Mobile networks
- Network-on-chip architectures
- Multicore systems
- Network protocols (eg AODV)
- Extra functional properties
- Network availability
- Energy-awareness
- Context-awareness
- Trustworthiness
- Quantitative evaluations
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
- Integrated: Integrating methods, tools, platforms and architectures for formal system design
- Action Systems
- Refinement calculus
- Event-B
- Simulink
- UPPAAL
- UML
- VHDL
- NoC (Tilera)
- Design: Increasing the flexibility of Formal Methods
- Adaptive design
- Patterns
- Visualisations
- Fault tolerance methods
- Quality: Ensuring and monitoring quality
- Formal methods
- Verification and validation
- Functional properties
- Real-time properties
- Metrics and measurements
- Maintainability and complexity issues
- Systems: Application of Formal Methods to industrial case studies
- Control software, e.g. digital hydraulics
- Safety-critical systems
- Cyber-physical systems
Research Unit Web Page: https://research.it.abo.fi/research/distributed-systems-laboratory
Leader of the unit
Luigia Petre Marina WaldénResearchers
Pontus Boström Mats Neovius Marta OlszewskaDoctoral Students
Petter Sandvik Moigan Kamali Sergey Ostroumov Jonatan Wiik Masoumeh ParsaResearch 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 |
Projects
EFFIMA/DiHy+Digihybrid (2009–2014, FIMECC SHOK)
- Faul-tolerant and reliable controllers for digital hydraulic valves
- Partners: TUT/IHA, VTT, Aalto, Cargotec, Metso Automation, Metso Paper, Norrhydro, Nurmi Hydraulics, Wärtsilä
- Digihybrid (Regenerative hydraulic hybrid with digi-valve and multi chamber cylinder technology) 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.
- DiHy (Digital Microhydraulics) is a project within Fimecc/EFFIMA/MeKo SHOK for the period 2009-2014. 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.
eDiHy (2011–2014, Academy of Finland)
- Contract based design of control systems relying on simulation tools
- Consortium: TUT/IHA
- Within project eDiHy (Energy Efficient Digital Hydraulic Hybrid Machines) 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.
FResCo (2013–2015, Academy of Finland)
- High-quality Measurement Infrastructure for Future Resilient Control Systems
- Consortium: UEF/Kuopio and Digile, Fimecc, Cleen SHOKs
- The control system paradigm, where action is determined based on sensing, monitoring, and measuring, forms a fundamental part of our contemporary and envisioned software-intensive infrastructures. This is illustrated, for instance, by the advent of sensor networks, the growing interest in location- and context-aware computing, and the promotion of the so-called cyber-physical systems that network together computational elements with physical inputs and outputs. Measuring systems will form a critical infrastructure for decision making in novel production planning systems for many industrial sectors and therefore, the high-quality of these systems is of utmost importance. In this project, we focus on high-quality environmental measuring for future resilient control systems and study the contribution of formal methods in devising high-quality solutions. One of the novelties of our project consists in proposing measurement infrastructures for novel control methods. Measuring extends the concept of monitoring currently associated to contemporary control systems and aligns suitably with our proposed focus on environmental systems. Interoperability of environmental systems is a key feature we address, by proposing the use of a top-down, correct-by-construction method instead of the more traditional attempt to integrate various existing (and partial) solutions to interoperability. Our formal approach allows for reliable measuring that, in its turn, provides for resilient future control methods. Hence, our project aims at stretching current knowledge boundaries in a feasible manner and at providing new results to be next experimented with, for further innovations and applicability in industry.
ADVICeS (2013–2017, Academy of Finland)
- Adaptive Integrated Formal Design of Safety-Critical Systems
- Co-operation: Eindhoven Univ. of Techn. (NL), Southampton Univ. (UK)
- The main objective of the project ADVICeS is to develop a collection of tactics for system modelling that is based on formal methods. The aim is to make the formal design process more efficient, flexible and maintainable for developing complex, dependable software systems that are correct by construction. A combination of an adaptive design framework with formal methods is meant to augment the development flexibility and give faster response to changes and, hence, will aid to achieve a feasible formal development process that enhances maintainability. Integrating metrics and quality measurements with the formal design will provide additional development guidelines to support the modelling and enable the assessment of the suitability of the proposed hybrid method.