BETTY: Behavioural types for reliable large-scale software systems

Abstract

Modern society is increasingly dependent on large-scale software systems that are distributed, collaborative and communication-centred. Software of this kind is very sensitive to undesired behaviour, ranging from security breaches to deadlocks and incompatibilities. These concerns have led to the emergence of mathematical frameworks for describing and reasoning about distributed software. One such framework is that of behavioural type theory, which describes the interplay between the behaviour and the interface of systems. This is now emerging as an important research topic in a number of European countries.

Keywords: programming languages, programming theories, distributed software infrastructure, large-scale public infrastructure, service-oriented computing, security, interactional interface, dependability, reliability, specification, verification, types, type disciplines, behavioural types, static checking, dynamic properties

Modern software systems operate on a large scale. They are distributed, collaborative and communication-centred, and are an essential part of the technological infrastructure of society. Many critical services are offered via the Internet and depend on other network technologies such as Clouds. These services include commercial operations such as banking and e-commerce, as well as public-sector systems such as medical records and e-government. They run as large-scale distributed infrastructures, constantly collecting information and dynamically adding new functionalities, while network-aware devices that access these services adapt dynamically to their environment. Such devices themselves perform distributed computation internally in increasingly multi-core hardware, integrating information from diverse sources.

How can undesired behaviour be prevented in these complex and often socially critical distributed applications? Protocol incompatibilities, malicious resource usage, security breaches and deadlock/livelock can have wide-ranging consequences, from temporary service outage to information leakage to exploitation of security vulnerability by criminal organisations. The dynamic addition of functionalities must not compromise the safe and reliable behaviour of services. If software developers are to guarantee that their products are safe, they must have a solid methodological and infrastructural basis, including general programming abstractions that build on formal foundations. The sheer complexity of distributed software demands novel solutions, rather than existing general purpose ICT mechanisms. The development process needs languages and tools that can establish that devices and applications are indeed safe before they actually run in potentially dangerous open environments. It is essential to be able to specify desirable properties rigorously and validate them for concrete systems, assisted by automatic and semi-automatic software tools.

Against this background, the central research goal is to develop foundational methodologies for statically ensuring safety, liveness and critical security properties of communication-centred software, using the notion of “behavioural types”.

Behavioural types are abstractions of the dynamic behaviour of components, specified by simple yet expressive languages, that characterise the permitted interaction within a distributed system. The key idea is that some aspects of dynamic behaviour can be verified statically, at compile-time rather than at run-time, by analysing the behavioural types of components. Other aspects, intrinsically dynamic like adaptation or evolution, still benefit from the use of concise type languages, when they have decidable theories. The goal of this Action is to build on recent progress in the theory of behavioural types and embody that theory in practical programming languages and tools, which will then be deployed for the development of distributed software systems.

In order to achieve this goal, significant research challenges need to be tackled.

- How can mathematical theories of behavioural types be unified, to give a secure foundation for global service-oriented systems?

- How can behavioural types be used in practice to specify and verify the correctness of software components in large and long-lived distributed systems?

- How can the present programming language prototypes be developed into fully-fledged compilers and tools for widely used languages?

There have been some recent nationally-funded research projects in this area, mainly in France, Italy, Portugal, the UK and Ireland. Although the projects included some international collaboration, there was no overall co-ordination and the number of participants and countries involved was relatively small. There was also a more inclusive FP6 project, Sensoria (Software Engineering for Service-Oriented Overlay Computers), which proposed a software engineering approach to service-oriented architectures, integrating foundational theories, techniques and methods. The verification techniques included behavioural types, but at the time most of the results were still preliminary.

There is now an urgent need for more explicit and more focused co-ordination of research activity on this subject across Europe, in order to consolidate and expand the community. Many foundational theories and technologies are in place, but delivering them to the software industry and achieving the goal of more reliable large-scale distributed systems will require a co-ordinated effort to ensure a flow of results from foundations to programming languages to applications. A COST Action is the ideal mechanism for this co-ordination activity.

This Action will lead to a new generation of programming languages, tools and theories, to enable safety-assured large-scale distributed software infrastructures and to equip their components with formal certification of their good behaviour. The technologies will be usable for a wide range of applications, ranging from applications running inside a single device over multi-core chips to those providing global services. The central benefit for society is to make the computing systems on which we increasingly depend, more reliable, secure and safe, based on clear and rigorous criteria. This Action's contribution will consist of a deeper understanding and more precise modelling of communication-centred computing, and in feasible, automatic, certification technologies guaranteeing a component's correctness through its behavioural type, before and during execution. This will lead to new software development methodologies promoting safe, secure and highly dynamic services, and possibly to a new international standardisation for quality assurance and certification of software components, a basis for new curricula for education in ICT, and new contributions to the theory of computation.

Main objective: to develop the domain of certified software for global services, providing languages and tools for automatically checking behavioural properties of concurrent and distributed systems, specified with simple yet expressive type languages.

Sub-objectives:

O1. Co-ordinate European research activity on the theory and application of behavioural type systems, and the deployment of programming languages and tools based on them, organized into the following themes.

- Theoretical Foundations

- Security

- Programming Languages

- Tools for Analysis and Verification

- Applications

O2. Build an effective working community of European researchers in this area, by means of the following activities:

- Annual workshops (following a successful workshop in April 2011)

- Training schools for PhD students and early-career researchers

- Extended research visits between institutions, especially for PhD students and early-career researchers

- Enlarging the research network

O3. Encourage the industrial adoption of advanced programming languages and tools, by working with existing industrial contacts and developing new ones.

These objectives will be realized in the following deliverables, in addition to the activities themselves.

D1. Published proceedings of annual workshops

D2. Reports or survey papers produced by each Working Group

D3. Published tutorial material from training schools

D4. A web site presenting an up-to-date and comprehensive view of the field

D5. Open-source implementations of programming languages and tools

D6. Open-source implementations of exemplar distributed software applications

Successful research in this area will have a deep and broad impact on the practice of software development, and on the scientific theories underlying our understanding of distributed computing systems.

This Action involves five themes: Foundations, Security, Languages, Tools, Applications. These are defined above and reflected in the structure of Working Groups. The following are key topics, most of which are relevant to all themes.

- Improved support for service-oriented programming in object-oriented programming languages.

- Fairness and liveness properties for global services.

- Negotiation, adaptation, extension and evolution within long-lived environments for service-oriented software.

- Frameworks and meta-theories, enabling description of the features and relationships of a range of theories without duplication of effort.

- Choreography, orchestration and global types, to specify and analyze the collective interaction among software components.

- Sessions, roles and relationships, generalizing from an identity-based view to a role-based view of the behaviour of session participants.

- Fault tolerance and error recovery, which are essential in service-oriented distributed systems and should be specified alongside high-level functional requirements.

- Quantitative behavioural type theory, to allow specification and analysis of non-functional properties such as response time or resource cost.

- Support for multi-core architectures in service-oriented programming, based on communication oriented technology developed for distributed systems.

Each Working Group will co-ordinate work on these topics as they relate to its theme, and communication between Working Groups will ensure that each topic is treated in a consistent way across all themes. Significant scientific innovations are expected through a close collaboration of the best experts in the field, in unification of foundational theories and their transfer into practical technologies and tools for software development.

The following Working Groups will co-ordinate activity.

WG1 Foundations

WG2 Security

WG3 Languages

WG4 Tools

WG5 Applications

Each WG will promote its theme, ensure consistency and avoid duplication of effort, and form links across themes and with industry.

1. Is COST the best mechanism?

5.60

2. Does the proposal address real current problems / scientific issues?

4.80

3. Is the proposal innovative?

4.80

4. Impact?

5.20

5. Are networking aspects well motivated and developed in the proposal?

4.80

6. Presentation

4.60

Total: 29.80 (out of 36)

The comments below are not very coherent and seem to be a combination of comments from several reviewers.

put lines between seemingly different reviewers … and put emphasis on what may be useful for the full proposal

The objectives of the proposed Action are not well motivated. The research community seems to already exist, the networking aspects are not convincing. The novel aspects of the action are not clearly described.

—

Your interesting proposal addresses recent problems in software engineering. However, the working group description could be significantly improved by clear declaration of the role of each working group, highlighting the interactions between them, and giving the expected outcomes of each of them.

—

The proposal intends to obtain increased reliability and security from formality for service engineering. This is neither easy for real scenarios nor for laboratory ones. Therefore it may be worth while its attempt. If it succeeds, thanks to cooperation and ideas exchange, the step ahead would be huge; therefore, it is a high-risk proposal with potential high returns.

—

In current software development, there is an acknowledged urgent need to enable safe and dependable distributed software infrastructures. It is essential to provide for their autonomous components some formal certification of component`s expected behaviour. Deeper understanding and adequate formal modelling of interactive (e.g. communication-centered) computing, in particular by behavioural type systems and, deployment of according programming tools is an interesting and promising direction for R&D of new, adequate software development methodologies. A COST action really seems to be the best choice to coordinate these activities. If succesful, the proposed Action could have significant impact on the theory and practice of nowadays networked software systems as well as cognitive artificial systems research and development.

—

The proposal addresses a relevant topic, namely the validation of large-scale software systems. The proposed approach, type theory, is very promising. Unfortunately, type theory has been promising for the last few decades and its impact in practical applications has been surprisingly limited. The main weakness of the proposal is that it does not sufficiently make clear why and how the consortium will turn type theory from a promising technique into a widely-used technique. Industry involvement and commitment is essential in this respect, however the proposal merely mentions industry without explaining how they will involve industry. A final comment is that the proposal contains quite some buzz words without explaining which role they will actually play in the project proposal. An example is the frequent use of the term `security` without explaining how this can be better treated with type theory than with more conventional techniques and without explaining how security relates to the list of key topics mentioned in the proposal.