Project Details
Layman's description
In our tech-driven world, computers and the internet are integral to daily life, seen in smartphones and automated systems like driverless trains and factory robots. These constitute "distributed systems," complex networks where independent parts communicate over the internet. A decentralised distributed system is a network of interconnected and independent components or nodes that work collectively towards a common goal without relying on a central authority for coordination or control. In these systems, tasks, processes, or data are distributed across multiple nodes, allowing them to operate autonomously and make decisions locally. When these systems exhibit diverse characteristics, functionalities, or capabilities among components, they are termed heterogeneous swarm systems.
Automated factory robots represent heterogeneous swarm systems, showcasing diverse capabilities and functionalities tailored for assembly or transportation. Equipped with distinct sensors and communication methods, we want these robots to collaborate seamlessly as a unified entity, efficiently managing tasks and sharing crucial information to enhance the manufacturing process. Nevertheless, conceptualising and strategizing around these systems pose significant challenges. How precisely do the robots coordinate their movements? How can the system maintain message integrity among robots? And how does it handle communication setbacks?
Our research centres on ensuring the reliability and trustworthiness of these systems. To achieve this, we're crafting a framework ensuring their flawless and secure operation. Using Formal Methods—mathematical tools—we model and comprehend system behaviour, guaranteeing these systems perform as intended without unexpected outcomes. We build upon theoretical foundations for such methods such as process calculi, behavioural types, and a combination of static and dynamic verification, leveraging type systems, model checking, and runtime monitors.
Our goal is to create a comprehensive toolbox facilitating the development of distributed message passing applications that prioritise correctness by design. The toolbox would enable the developers of swarm systems to easily create trustworthy and reliable systems. In turn, this initiative will instil trust and reliability in the daily users of these systems, ensuring their seamless interaction with the applications.
Automated factory robots represent heterogeneous swarm systems, showcasing diverse capabilities and functionalities tailored for assembly or transportation. Equipped with distinct sensors and communication methods, we want these robots to collaborate seamlessly as a unified entity, efficiently managing tasks and sharing crucial information to enhance the manufacturing process. Nevertheless, conceptualising and strategizing around these systems pose significant challenges. How precisely do the robots coordinate their movements? How can the system maintain message integrity among robots? And how does it handle communication setbacks?
Our research centres on ensuring the reliability and trustworthiness of these systems. To achieve this, we're crafting a framework ensuring their flawless and secure operation. Using Formal Methods—mathematical tools—we model and comprehend system behaviour, guaranteeing these systems perform as intended without unexpected outcomes. We build upon theoretical foundations for such methods such as process calculi, behavioural types, and a combination of static and dynamic verification, leveraging type systems, model checking, and runtime monitors.
Our goal is to create a comprehensive toolbox facilitating the development of distributed message passing applications that prioritise correctness by design. The toolbox would enable the developers of swarm systems to easily create trustworthy and reliable systems. In turn, this initiative will instil trust and reliability in the daily users of these systems, ensuring their seamless interaction with the applications.
Short title | Verification Of Distributed Message Passing Applications |
---|---|
Status | Not started |