Powered by OpenAIRE graph
Found an issue? Give us feedback

Conversation-Based Governance for Distributed Systems by Multiparty Session Types

Funder: UK Research and InnovationProject code: EP/K011715/1
Funded under: EPSRC Funder Contribution: 1,500,660 GBP
visibility
download
views
OpenAIRE UsageCountsViews provided by UsageCounts
downloads
OpenAIRE UsageCountsDownloads provided by UsageCounts
23
7

Conversation-Based Governance for Distributed Systems by Multiparty Session Types

Description

Software is increasingly organised centring on distributed communicating processes. This is especially true in large-scale distributed computing platforms such as the backend of popular Web-based services and public sector platforms for e-healthcare and e-science, which often provide lifelines of society. An application is organised as a dynamic collection of distributed components. The framework is based on interacting processes, which extends the traditional paradigm of functions and objects and which allows far more versatile and scalable organisation of software components. Assuring safety in such distributed systems is a vital societal concern: many platforms are long-lived, offer socially critical services, and collect security-sensitive data; safety violations, including security breaches, can have wide-ranging consequences, from temporary service outage to information leakage to exploitation of security vulnerability by criminal organisations. However, existing assurance methodologies are based on objects and functions: no well-established formal assurance methodologies are known for distributed systems. Large-scale distributed computing infrastructures are like skyscrapers used by hundreds of thousands of people, for building which the well-established structural engineering principles are used as a foundation of safe engineering. Can we establish the corresponding engineering principles for building software skyscrapers vital to modern society? Against this background, the central aim of this project is to establish a general, formally based safety assurance methodology for distributed systems, which we call conversation-based governance. The conversation-based governance starts from advanced types for capturing conversations, called multiparty session types (MPSTs), recently introduced by the PIs and extensively studied by researchers. Building on the latest theoretical results and on the PIs' ongoing collaborations with the project partners, we introduce the new development and assurance framework based on MPSTs. At the centre of our approach is a high-level, programming-language-agnostic MPST-based declarative protocol description language. The safety assurance in this framework is realised through verifications of distributed components against formal specifications in this protocol language, performed either statically (at the development time) or dynamically (at runtime), of which we place an emphasis on the latter: large-scale distributed systems are rarely amenable to static verification as a whole due to, for example, heterogeneous components, so that only the dynamic verification and enforcement can offer a comprehensive safety assurance. It is due to this emphasis on runtime policing of conversations that we call the proposed assurance framework, conversation-based governance. The project will establish this new methodology through the following tasks: (1) The development of a programing-language-agnostic protocol description language, called Scribble, and its open source tool chain, programming interfaces (APIs) and runtimes, backed up by a uniform type theory of MPSTs. (2) The development of an assertion language for specifying and verifying refined safety properties as elaboration of protocols, together with a policy language linked to the assertion language. Decentralised monitors backed up by a theory of the pi-calculus offer efficient, scalable runtime verification and enforcement. (3) Large-scale experiments through collaboration with project partners, realising formal safety assurance for real-world applications, including global cyberinfrastructure, enterprise software, and messaging middleware. Throughout the project, an extensive dialogue between theories and practice will be conducted, leading to truly effective principles and tools for general safety assurance methodologies of distributed systems vital for future IT infrastructures and society.

Data Management Plans
  • OpenAIRE UsageCounts
    Usage byUsageCounts
    visibility views 23
    download downloads 7
  • 23
    views
    7
    downloads
    Powered byOpenAIRE UsageCounts
Powered by OpenAIRE graph
Found an issue? Give us feedback

Do the share buttons not appear? Please make sure, any blocking addon is disabled, and then reload the page.

All Research products
arrow_drop_down
<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=ukri________::85f3d63bad7aae7acc5ed1b069b11806&type=result"></script>');
-->
</script>
For further information contact us at helpdesk@openaire.eu

No option selected
arrow_drop_down