Maximum 2-3 pages

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, e-commerce, social networking and document sharing applications, as well as public-sector systems such as infrastructures for local, national and trans-national e-governments, e-healthcare and e-science. They are long-lived and run continuously, constantly collecting information and dynamically acquiring new functionalities, while network-aware devices that access these services, including mobile phones and tablets, adapt dynamically to their environment.

Recent years have seen the development of a new paradigm for the development of distributed software systems, based on the internalisation of the concept of a distributed service, often called service-oriented computing. In this paradigm, the computational behaviour of a system is organised into a collection of services, which run concurrently and interact with each other, instead of being organised into a collection of functions which run sequentially. This collection of services implements another service. For example, a login service for a popular web portal is usually implemented by multiple distributed components realising more specialised functions, such as an external identity provider, a browser, an internal identity registry, and an internal authentication service.

How can improper, undesired behaviour be prevented in complex and 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, affecting a large number of users.

In traditional sequential programming, the systematic and rigorous application of data types and type checking has yielded huge improvements in software reliability and programmers' productivity. The pinnacles, so far, of type theory in mainstream programming languages are the sophisticated generic type systems of Java and C#, where programming abstractions are built in at a fundamental level. Data types abstract and specify the behaviour of permitted operations on data. Even if types are not used for static checking, they often play a fundamental role in runtime checking (as in Python, a language widely used for server-side applications). Because data types offer basic abstraction of programs' behaviour, cutting edge logical verification tools such as Java Modelling Language (based on Java) and Spec# (based on C#) articulate their logical assertions for programs by building on the type abstractions of the respective programming languages.

Thus data types offer an effective basis of programming and verification for sequential data processing. For building distributed, service-oriented computing software, a corresponding structural view requires behavioural types, which specify the permitted interaction within a distributed system. The behavioural type of a service specifies its expected patterns of interaction using a simple, expressive type language, in a way that can be used to determine automatically whether a service interacts correctly with other applications. At present, although there is a significant body of theoretical work on behavioural types and a growing collection of prototype programming language designs, it is not yet possible for industrial software developers to exploit behavioural types in the design, analysis and implementation of service-oriented computing systems.

The goal of this Action is to transform the theory and practice of service-oriented software development by the systematic application and unification of behavioural type systems. The result will be new foundations for service-oriented systems, new programming languages whose designs are informed by behavioural types, new program analysis tools based on behavioural types, and new software development methodologies based on these foundations, languages and tools.

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

- How can mathematical theories of behavioural types be unified, capturing different aspects of software behaviour at levels ranging from bare protocols to more refined properties such as security policies, and together offering a consistent, comprehensive foundation for large-scale distributed infrastructure which constitute global service-oriented computing?

- How can behavioural types be integrated into fully-fledged language designs, compilers and tools, both as new production-level programming languages and as enhancements of widely used programming languages, so that software developers can effectively structure their code around behavioural types?

- How can behavioural types be used in practice as a basis for specifying and verifying the correctness of software components in large-scale, long-lived distributed systems, both at development time and at runtime, so that effective validation of components and services is possible?

Recently there has been a rapid growth of activity in the field, and an accelerated expansion of the research community. There is a danger that a proliferation of alternative and incompatible approaches will lead to duplication of effort, hindering the transition from foundational theories and prototype programming languages to industrial-strength tools and methodologies. There is therefore a need for direction and co-ordination. On the basis of a large number of research groups and many national research projects, these activities will reach a tipping point towards their practical world-wide adoption by having a supporting structure within which to organise the community, with funding for strategic meetings and scientific exchanges. A COST Action is an excellent mechanism for this purpose.

Some of the better known existing large-scale distributed infrastructures include the backends of Amazon, Google and Microsoft Windows Live. Widely-practised methods for building distributed services in such large-scale infrastructures include:

• Remote procedural call (RPC), or its object-oriented variant, remote method invocation (RMI). For example, a major part of Google's backend is implemented in C++ with RPC, together with the serialisation formats of Google Protocol Buffer.

• Web service technologies through HTTP/SOAP (Simple Object Access Protocol), which often use WSDL (Web Service Decription Language, a simple interface language). While the shape of interactions is essentially the same as RPC, all resources are accessible through HTTP, a single application-level protocol.

• Messaging, which often uses messaging brokers, centring on a publish-subscribe model. This is based on asynchronous message passing and is especially useful when rapid and reliable dissemination of data is necessary.

Another traditional method for integrating distributed components is to have implicit data flow through shared state. However, the explicit communication-based frameworks listed above have the merit that the infrastructure is clearly divided into distributed components with explicit interfaces; this makes it easier to export services, change service interfaces, and transplant a system into a new computing environment such as clouds. For example, during the last decade Amazon converted all of the software components in its infrastructure so that they are based on explicit communication interfaces centring on RPC/RMI, HTTP/SOAP and messaging. The framework Amazon has achieved is commercially known as SOA (Service Oriented Architecture).

RPC, RMI and HTTP are all based on the request-reply interaction pattern, which is a distributed version of a function call to data structures and objects. The restriction to the request-reply pattern causes several problems when, like Amazon, one imposes strict communication interfaces among distributed components. These problems include the lack of description or abstraction for overall interaction patterns (e.g. a sequence of interactions constituting a workflow is divided into numerous request-reply interactions) and latency due to the waiting time needed in request-reply. They are closely related to the lack of uniform programming abstractions capturing, among others, the above three forms of communication interfaces and beyond, and the lack of clean programming language support for distributed computing.

There are also ongoing efforts for standardising frameworks for developing large-scale distributed service-oriented systems, mainly focusing on high-level modelling languages, including the RUP standard by IBM (the RUP standard), Microsoft and others, based on existing notations such as UML and BPMN (which are originally intended for business process modelling). Their main aim is to deal with the challenges of how we can capture compatibility of interfaces of heterogeneous distributed components and their causal dependencies. These efforts currently lack a unifying basis by which we can model a general class of communication behaviours and then ground the resulting models onto programming abstractions, hence source code and runtime. Such a grounding is precisely what has made the existing modelling artifact, such as UML class diagrams, an effective basis for development.

In major programming languages usable for production-level application development, such as Java, C#, Python, Javascript and C++, there is no language-level support for distributed communication except as libraries (APIs). An exception is remote method invocation (RMI), which is part of the language specification in Java and C#, but this is one of the lowest-level communication primitives. This lack of language-level support means that communication patterns are not easily visible to the compiler or to program analysis tools. For example, implementing a login service requires complex sequence of RMIs on constituent services. If this sequence is represented only as a series of API calls, with no explicitly-defined high-level structure, then programming errors are easy to make and difficult to detect.

The only relatively widely-used production-level programming language which centres on message passing is Erlang, which is roughly based on Hewitt's actor model. The main programming-level abstraction is the queue, which concerns only messages to a single actor. Another widely-used system, especially in scientific computing, is MPI (Message-Passing Interface). MPI is provided as an API (procedure library) for standard languages such as C and Fortran, and so it suffers from the lack of high-level abstractions mentioned above in relation to RMI. Furthermore, the MPI libraries are tailored for typical computational patterns in scientific number-crunching and are unsuitable for general-purpose distributed programming. Finally, although it is a research programming language, Occam-Pi is highly efficient but is again essentially based on synchronous handshake communication.

Recently Google has been developing two general-purpose programming languages based on its analysis of internal large-scale distributed software development. The Go programming language (http://golang.org/) is a system-level, garbage-collected, type-safe programming which incorporates hand-shake communication. It is intended as an advance from the C programming language. Dart (http://www.dartlang.org/) is a class-based object-oriented language with pluggable static typing and with actor-like queue-based message passing communication. It is intended as an advance from Javascript, and is being developed as part of a large programming environment project. In both languages, communication is provided by language primitives, not by libraries. The underlying communication model used by Dart, based on asynchronous communication, is close to the lower-level communication model adopted in many languages based on behavioural types (see below).

Go and Dart show that in the context of the development of large-scale distributed applications, engineers have started to realise the need to treat communication seriously. But even in these latest programming languages, there is no language-level abstraction or specification mechanism for communication patterns beyond handshake or request-reply.

Types articulate computation in a given paradigm. The traditional notion of types offers abstractions for data, objects and operations on them, which are the key building blocks of computation in traditional programming languages. The basic form of behavioural types, specifying interaction patterns in distributed services, articulates the ways in which interactions are programmed and performed. From this basis, it is possible to specify more refined behavioural types and logical assertions. Thus behavioural types are not only a basis for verification, but also a way to organise computation in service-oriented, distributed computing systems. By centring on interaction, behavioural types are often automatically compositional. The strategy is to first verify whether or not the interactions of each service satisfy their behavioural types. After that, the behavioural type of a composite service, built from interactions between components, can be verified without re-examining the components.

Type theories for distributed computing systems are a new field largely initiated by the study of behavioural types. They are built on the formal foundations provided by process calculi, such as ACP, CSP, CCS, pi-calculus, and higher-order pi-calculus. Process calculi offer a rigorous mathematical basis upon which communication behaviours of software systems are represented, reasoned about and analysed. Combined with other formalisms such as Petri Nets, they offer a general framework in which to mathematically capture diverse forms of interaction, rigorously and in a distilled form, including synchronous, asynchronous, untimed, timed, and others.

For theories of behavioural types, process calculi with channel passing capability, starting from pi-calculus and higher-order pi-calculus, play a central role. They offer a rich basis for behavioural types because their tiny syntax (a fully expressive asynchronous version of the pi-calculus can be defined by a standard BNF-style grammar in six lines) can nevertheless express fully the whole range of interactional behaviours realisable by programming languages, thus serving as a rich basis for investigation.

However, calculi and programming languages differ in that the latter also need to offer programming abstractions (structuring principles for software) and efficient executions, among other pragmatic concerns. Calculi offer a basis upon which these ideas can be formally expressed and examined, but it is also necessary to build a comprehensive programming framework which offers effective structuring principles and other foundations for building distributed, service-oriented computation.

Research into behavioural types and the associated programming primitives has been addressing these concerns.

Representative technical approaches to behavioural types include:

• Types for sessions (session types), which are based on the idea that interactions among distributed components and services can naturally be divided into multiple conversations (sessions), each with a specific protocol. The division into sessions enables tractable type-abstraction, making it easy to specify protocols and validate programs.
• Contracts for interactions, which give fine-grained specifications stipulating reciprocal responsibilities among interacting parties, often using labelled transition relations. Contracts can be combined using various algebraic operators to obtain larger contracts.
• Behavioural security specifications, where security properties are specified as behavioural types, often elaborating simpler notions of behavioural types. This enables an explicit specification of information flow as reciprocal responsibilities among communicating parties in a conversation, offering a uniform framework to specify distinct security properties such as secure information flow and access control, centring on types for interaction.

There are diverse sub-approaches in each domain: for example, conversation types offer an alternative way to describe sessions, as a set of interactions inside a scope, giving an abstraction of interaction in a common medium. There are also many notions of contract, capturing diverse behavioural properties. Note that contracts differ from simply specifying (say) temporal logical formulae for interactions. They are specified as reciprocal responsibilities among communicating parties, and this global form of contract can be related to individual responsibilities by a process known as projection, which is also used in session types for more than two participants.

Thus behavioural types and their associated theories offer a new shape of specification languages centring on interactions and reciprocal responsibilities. But they also enjoy a rich linkage with traditional theories. Contracts are closely related to existing temporal and modal logics, as well as their ramifications. The type structure of a session type is related to an automaton for communicating systems, since it specifies a series of actions among two or more parties. Furthermore, behavioural types give rise to the diversity of type structures cultivated in logics and programming theories, such as polymorphism and dependent types.

All approaches to behavioural types have commonality in that they are closely associated with programming primitives. This is also a key factor for the effective validation of programs against specifications given by behavioural types because the programming primitives offer linkage between programs and type specifications. For example, session types are associated with primitives to initiate a session, communicate through sessions, receive through sessions, and so on. This linkage then leads to a type discipline (a method to validate programs against given types), and its key properties such as principal typing and type/protocol safety (i.e. interactions follow a stipulated protocol), is established. The development of type disciplines closely follows that of traditional typed lambda-calculi and programming languages such as ML and Java. Contracts and logical specifications can then offer richer specifications by elaborating the base type disciplines, which may also make use of spatial localities and their composition for modular specifications.

Many of these studies were initiated in the context of the Sensoria project (Software Engineering for Service-Oriented Overlay Computers), which ran from 2005 to 2010 as part of the EU FP6. The Sensoria Consortium consisted of 14 universities, 1 research institute and 4 companies from 7 countries: Italy, Germany, United Kingdom, Portugal, Denmark, Hungary and Poland. Several of its members are also participants in this Action.

These studies give a foundation for the design of new programming languages based on and supporting behavioural types, and for an enhancement of traditional programming languages with behavioural types. From the development viewpoint, the key merits of using behavioural types may be summarised as follows.

• Clean and general structuring principles for implementing, composing and managing communicating distributed systems (distributed services). Given the nature of distributed programming, this aspect covers not only a source program for each endpoint but a configuration of many components, which may be written in different programming languages.
• Suggestions for the design of execution machinery (runtime system) for programming languages for distributed services, through the linkage between programming primitives and behavioural types.
• Simple and intuitive specifications of key properties, which are validated either statically (at compilation time) or dynamically (at runtime), the latter enabling a change of specifications over time. Both static and dynamic validation can make use of efficient algorithms whose correctness is established through the underlying theories.

In recent years, several research projects have started to develop new prototype programming languages based on behavioural types, as well as extensions to existing programming languages. In the latter thread, the languages being extended include Java (the SJ project), ML, BPEL, Scala (the Session Scala project) and C. Microsoft has developed the language Sing#, which uses elements of behavioural types (session types) for systems level programming in the Singularity operating system.

Research prototype languages are often equipped with a full type checker, as well as a lightweight runtime system. Reflecting their experimental nature, runtime and tool support is often elementary. However, through their development, many important results have been obtained regarding, among others: programmability; type checking and type inference algorithms; runtime design; integration of behavioural types with traditional programming language constructs and their validation methods; dynamic validation mechanisms; and design and development experience. Some of these experiments are being further developed to offer more robust production-level support of safety assurance based on behavioural types, often associated with existing frameworks and languages, such as SOA, BPEL, and messaging infrastructure.

Society is becoming dependent on large-scale distributed software systems, and there is an urgent economic and societal need for improved technologies and methodologies for designing, analysing and building such systems. These technologies and methodologies must be based on a sound theoretical foundation. 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.

Specific objectives of the Action, at the co-ordination level, include:

• Developing a clear picture of where particular expertise is located, in order to be able to link problems with solutions.
• Supporting short-term scientific missions, especially for PhD students and early-career researchers, in order to facilitate the development of lasting research collaborations which can be supported by national funding.
• Organising scientific meetings and workshops.
• Maximising the value of existing industrial collaborators by putting them into contact with a wider range of participants in the Action.

The networking activities of the Action will result in a strengthened and consolidated European research community with effective working practices to ensure that foundational research informs and is incorporated into effective programming languages and tools, which are in turn delivered to the software industry for use in practical projects.

The Action will co-ordinate research that is taking place in around 20 current nationally-funded projects in various European countries.

Three current EU FP7 projects have concerns that are connected with those of this Action to some extent.

• ANIKETOS (Secure Development of Trustworthy Composable Services, 2010 - 2014)

ANIKETOS has a very practical focus on the security of service-oriented systems. Its consortium does not include any of the participants who have been involved in planning this Action. It is likely that the Action will be able to offer appropriate theory to support some of the work of ANIKETOS; conversely, the industrial members of the ANIKETOS consortium should be a good source of practical case studies and potential application areas for the results of this Action. It will therefore be important to develop a relationship between this Action and the ANIKETOS project.

• ASCENS (Autonomic Service-Component Ensembles, 2010 - 2014)

The ASCENS project aims to design methodologies to build “ensembles” of components in which there is a strong emphasis on both service-oriented architectures and a high degree of autonomy, self-awareness and adaptability on the part of components. The project includes the development of theoretical foundations and formal verification techniques, and these goals are very much in line with those of this Action. In particular, there is a clear possibility of applying behavioural type theory to the application domains considered by ASCENS. Some of the participants in this Action are also members of the ASCENS project. It will be useful to build on this connection in order to develop mutually beneficial collaboration.

• HATS (Highly Adaptable and Trustworthy Software using Formal Models, 2009 - 2013)

HATS also aims to improve the reliability of large-scale software systems. Its approach is to develop a rigorous foundation for informal software engineering practices based around the concept of software product families. Behavioural specification formalisms, and tools based on them are important aspects of this project, but it contrasts with the approach of this Action: it does not propose behavioural types as a new structuring concept for programs. Some members of the HATS consortium are participants in this Action, and this will be helpful in understanding the results of HATS during the initial stages of this Action.

• Define the research topic in such a way that it is clear that the network will address real current problems or scientific issues.

• Inform about the wider relevance of the Action (why is it desirable to launch it as COST Action).

• Explain why COST, which funds only networking and capacity-building activities and not research, is the best mechanism for support. State reasons why COST seems to offer the appropriate framework for the Action, compared to other research frameworks such as ESF, ESA, EUREKA! or the EU Framework Programme.

• Describe the advantages or benefits which should arise from carrying out your project within the COST framework.

Behavioural types can be applied in two complementary ways: (1) as the basis for static analysis, so that components can be certified as safe before being deployed; (2) as the basis for runtime monitoring, so that deviations from desired behaviour can be detected. The runtime approach is particularly useful when a static analysis of the total system is impossible, such as when a distributed service is realised through interactions among components located at different sites. In both approaches, different behavioural type systems may be used at different levels of abstraction to describe not only properties of individual components but also emergent properties of larger subsystems and ultimately the complete system.

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 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, as well as infrastructure to support runtime monitoring of systems' behaviour. 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.

The following text is from the outline proposal.

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”. We shouldn't say “statically” because we are also interested in dynamic monitoring.

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? We should explain 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?

Some thoughts on other research frameworks and why we have chosen COST

ESF (European Science Foundation) funds some research activities:

• Exploratory Workshops: I think we are beyond this stage. Maybe our workshop in Lisbon could have been an ESF Exploratory Workshop, but at this point we have identified our community and problem area.
• Research Networking Programmes: I think these are very similar to what we want, but ESF is revising the scheme and it isn't open for applications at the moment.
• EUROCORES Programmes: these operate at a different level. If a theme is proposed and accepted, it may then be developed into a programme. Various funding agencies may then join a programme and provide funding for projects within it. It sounds quite interesting but there isn't a call for themes at the moment, and none of the existing programmes are relevant to us.

ESA:

• I don't know what they mean by this; the only ESA I can find is the European Space Agency.

EU Framework Programme:

• At an earlier stage in our discussions, it was noted that there is an open call with a deadline in January 2012. We decided to go for a COST Action. There is also a FET Open Call. What can we say about why we have chosen COST?

EUREKA!

• EUREKA! is complementary to COST. From a Wikipedia article: ”…the two focus on different aspects of R&D with COST's efforts geared towards more socially focused areas of public interest while EUREKA's mandate is to provide funding for projects envisaged, developed, and executed by private industry.” I think it's clear that our approach is more in line with COST.

• Summarise the previous research in the field of the proposal.

• Describe the current state of the art, including relevant research within the EU Framework Programmes and other EU fora, comparison of EU research with that in other parts of the world.

• Explain how the Action will be innovative in addressing either a new problem or a new approach to an existing problem.

Recent years have seen the development of a new paradigm for the development of distributed software systems, based on the concept of a service. This paradigm is known as service-oriented computing. The computational behaviour of a system is organised into a collection of services, which run concurrently and interact with each other, instead of into a collection of functions which run sequentially. Service-oriented computing demands new foundational theories, new programming languages, new software development methodologies, new approaches to testing, and new deployment strategies.

European researchers have taken the lead in this area, especially in relation to the theoretical foundations. This is at least partly because the foundations of service-oriented computing are best formulated in the language of process calculus, which is itself an area in which European research has been dominant for many years.

The current state of the art is exemplified by the results of the Sensoria project, which was part of the EU FP6. (Sensoria is summarised below). More recently, it has become increasingly clear that behavioural types have a key role to play in the design and implementation of service-oriented systems. The basic idea is that the behavioural type of a service classifies its expected interaction with other services, in a way that can be used to determine automatically whether or not services are compatible. The latest developments in the theory of service-oriented systems place behavioural types in a position of central importance as the basic means of defining the structure of interaction within a system. This is analogous to the central structuring role of data types in traditional sequential computing.

The purpose of the Action is to co-ordinate further work in this direction. In comparison with Sensoria, we now have a much larger community of research groups. With such a large number of sites, most of which are well-funded by national research projects, another EU Framework project does not seem to be the most appropriate strategy. It is, however, essential to have a mechanism for co-ordination of the community, with funding for planning meetings and scientific exchanges. This is where a COST Action is ideal.

• Reasons for launching the Action, indicating the need for an experts network in the area and the added value of the Action networking. Emphasise immediate and future benefits and envisaged applications (understandable for non-specialists readers).

• Indicate whether the Action is mainly aimed at European economic/societal needs, or at scientific/technological advance, or both.

• Clearly distinguish between objectives, expected results and the means that are needed to achieve them. The impact of COST comes from concrete outcomes, not just activity; so indicate how the Action will aim for maximally productive outcomes.

• If this is a Trans-Domain proposal… (ours isn't)

Society is becoming dependent on large-scale distributed software systems, so the need for improved theories and methodologies for designing, analysing and building such systems is an urgent economic/societal need. Advances in science and technology will be necessary in order to satisfy this need. So the Action is aimed in both directions.

There have been some recent nationally-funded research projects in this area. We should say what these were, and list any current projects. 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. Give more details about Sensoria, who was involved and what it produced.

Sensoria

The main result of the SENSORIA Project was a novel, comprehensive approach to deal with Service-Oriented Computing (SOC). In this approach, foundational theories and proof techniques and are fully integrated in a pragmatic tool-supported software-engineering approach, addressing, for example, early verification and validation, semi-automatic development and deployment of self-adaptable (composite) services. This approach generalizes the concept of service in such a way that:

• it is independent from the particular global computer and from any programming language;
• it can be described in a modular way, so that security issues, quality of service measures and behavioural guarantees are preserved under composition;
• it supports dynamic, ad-hoc, “just-in-time” composition;
• it can be made part of an integrated service-oriented approach to business modeling.

For this new concept of service for overlay computers the SENSORIA Consortium developed new semantically well-defined and powerful

• modeling and programming primitives
• mathematical foundations
• techniques for qualitative and quantitative analysis
• tools for model-driven development and deploying service-oriented systems
• methods for transformation of legacy systems
• pattern-based engineering techniques.

The verification techniques included behavioural types, but at the time most of the results were still preliminary.

The SENSORIA Consortium consisted of 14 universities, 1 research institutes and 4 companies (2 SMEs) from 7 countries: Italy, Germany, United Kingdom, Portugal, Denmark, Hungary and Poland.

The complete list of participants is the following:

• Ludwig-Maximilians-Universitat Munchen (Coordination)
• Università di Trento
• University of Leicester
• Warsaw University
• Technical University of Denmark at Lyngby
• Università di Pisa
• Università di Firenze
• Università di Bologna
• Istituto di Scienza e Tecnologie della Informazione “A. Faedo”
• University of Lisbon
• University of Edinburgh
• ATX II Tecnologias de Software SA
• Telecom Italia S.p.A.
• Imperial College London and University College London
• Cirquent GmbH / FAST GmbH
• Budapest University of Technology and Economics
• S&N AG
• School of Management of Politecnico di Milano

National Projects

• UK (Honda, Yoshida), Multiparty Session Types: Theory and Conversation-Oriented Programming, July 2009 - December 2012 (417k Euros).
• UK (Gay, Honda, Yoshida), Engineering Foundations of Web Services: Theories and Tool Support, June 2008 - November 2011.
• UK (Honda, Yoshida) Ocean Observatories Initiative (Nov 2011- Oct 2013) (376k Euros)
• UK (Yoshida) VMWare PhDship (Distributed governance architecture) (Oct 2011–April 2015) (106k Euros)
• UK (Yoshida) EPSRC PhD PLUS (Distributed Session Java) (Oct 2010–Sep 2011) (100k Euros)
• Portugal (Ravara, Vasconcelos, Vieira), Liveness, statically, April 2012 - March 2015 (132k Euros).
• Portugal (Caires, Ravara, Vasconcelos), Space-Time-Types: Behavioural and Spatial Type Systems, July 2005 - June 2008.
• Portugal (Vasconcelos, Lopes), QUEST - a quest for reliability in generic software components, May 2009 - April 2012 (105k Euros).
• Portugal-Germany (Ravara, Nestmann), MONACO: MOdels for New Applications of COncurrency, 2008 - 2009.
• Portugal-UK (Vasconcelos, Martins, Yoshida, Honda), Language Design for Web Services, 2008 - 2009.
• Portugal-USA (Caires, Vasconcelos, Aldrich, Pfenning), INTERFACES - Certified Interfaces for Integrity and Security in Extensible Web Based Applications, May 2009 - May 2012 (289k Euros).
• Italy (Bruni, Dezani-Ciancaglini, Sangiorgi, Bugliesi), IPODS: Interacting Processes in Open-ended Distributed Systems, January 2010- September 2012 (86.600 euros).
• Italy (Acciai post-doc within ASCENS): 23k Euros / year.
• Italy-France (Dezani-Ciancaglini, Capecchi, Castellani, Rezk) MATYSS: Models and Types for Secure Sessions, 2009 - 2010.
• France (Castellani, +…) PARTOUT: PARallélisme parTOUT, ANR-08-EMER-010, Jan 2009 - Dec 2012 (403k Euros). Partners: INRIA, LRI, CNAM.
• Ireland (Hennessy) Foundations of Global Computing, Science Foundation Ireland, Feb 2008 - Feb 2013 (1.800k Euros).
• Denmark (Hildebrandt, Exformatics A/S), Technologies for Flexible Cross-organizational Case Management Systems (FLExCMS) Industrial PhD Project, January 2012 - December 2014.
• Denmark (Hildebrandt), Trustworthy Pervasive Healthcare Services (TrustCare), January 2008 - June 2012.
• Denmark (Hildebrandt), Context-Sensitive Services Developed in Global Collaboration Project, 2009 - 2013 (81k Euros).
• Denmark (Hildebrandt), Computer Supported Mobile Adaptive Business Processes (CosmoBiz), January 2007 - December 2011.
• Sweden (Parrow, Victor, +…) ProFuN: A Programming Platform for Future Wireless Sensor Networks, 2009 - 2013 (2834k Euros).
• Sweden (Parrow, Victor, Borgström) UPMARC: Uppsala Programming for Multicore Architectures Research Center, http://www.it.uu.se/research/upmarc, 2008-2017, say 100 kEuros/year on related activities
• Sweden (Parrow) A Framework for Parallel Programming Models, 2009-2011+, 90 kEuros/year
• France (Castagna, +…) CODEX: Efficiency, Dynamicity and Composition for XML: Models, Algorithms and Systems, 2009 - 2012 (108k Euros).
• France (Castagna, + …) TYPEX: “Intégration des approches langage, logique et orientée données pour un traitement XML certifié, dirigé par les types”, 2012 - 2015 (359k Euros).
• France (Hirschkoff, +…) Complice: Implicit complexity and concurrency: 84k Euros in Lyon (more at other sites).
• France (Hirschkoff, +…) PiCoq: process calculi and theorem prover formalisations: 21k Euros in Lyon (more at other sites)
• France (Hirschkoff) CoGip: process calculi, coalgebras, games: 6k Euros
• Serbia (Ghilezan) PROJECT ON 174026: Representations of logical structures and formal languages and their application in computing, 2011 - 2014 (1000k Euros)
• Serbia (Ognjanović, Ghilezan, +…) PROJECT III 044006: Development of new information and communication technologies, based on advanced mathematical methods, with applications in medicine, telecommunications, power systems, protection of national heritage and education
• France-Serbia-Italy-USA (Saurin, Ghilezan, Ariola) SEMACODE - Stratégies d'Évaluation, Machines Abstraites et COntrôle DElimité, INRIA équipe associée

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.

• Relevant links to and complementarity with any current and/or planned European research projects, such as ESF, FP, EUREKA! (bear in mind that avoiding duplication is one of the goals of COST)

We don't know about any, do we? So there is no duplication? Perfect! We should check to see if there are any projects of a more practical nature. If there are, then our emphasis on starting from a good theoretical foundation means that we will be complementary.

• ANIKETOS : Secure and Trustworthy Composite Services 2010 - 2014 Project web site

It seems to be much more practical in the sense that it doesn't mention theoretical foundations. We want to work on foundations and derive everything else from that.

• ASCENS: autonomic service-component ensembles 2010 - 2014 Project web site

The goal of the ASCENS project is to design methodologies to build “ensembles” of components in a way that combines the maturity and wide applicability of traditional software engineering approaches with the assurance about functional and non-functional properties provided by formal methods and the flexibility, low management overhead, and optimal utilization of resources promised by autonomic, adaptive, self-aware systems. The main topics of the project are:

- the definition of a Service-component ensemble language expressive enough to render self-awareness and autonomic aspects of the components. The language will integrate behavioural description with knowledge representation and reasoning about the environment;

- the definition of theoretical foundations and models for reliable and predictable system behaviour while exploiting the possibilities of highly dynamic, autonomic components (Clearly, this topic includes the application of behavioural type theory to this particular setting).

• SENSORIA 2005 - 2010 Project web site

It's more difficult to distinguish ourselves from SENSORIA, as many of the same people are involved. However, SENSORIA has finished but we believe there is more work to be done. The modelling languages and methodologies produced by SENSORIA were based on the theoretical state-of-the-art at the beginning of the project. There has been significant progress during the last few years, and the next stage of research is to incorporate new theory into a new generation of languages and tools. Maybe the work plan should explicitly mention ways in which we are going to build on the results of SENSORIA.

Also, we have been discovering a wider group of researchers who are working in this area (for example, at the workshop in Lisbon). A COST Action has the flexibility to expand the community as we find more people.

Simon: please precede remarks with your name.

Simon: I have put the text from the outline proposal into this section. Please improve it!

Simon: I have added some notes in each section.

Lucia: I have added a paragraph about the SENSORIA Project (achieved results and participants) in B.3 and some notes about the ongoing project ASCENS in B.4

Simon: I have started transferring and editing material from the notes section into the version at the top of the page.

Simon: This now more or less a draft of the background section. I'm sure it can be improved. At the moment it is a little long.

Kohei: I am in the middle, will come back soon. Two points I wish to (and started to) augment:

– We need to say what novelty / new impact this networking is intended to achieve. I believe one of the merits we can say is to consider integration of different behavioural types technologies into consistent whole. This is because the assessment criteria says so, and the successful proposals emphasises this point.

– We may have to compare with other methods for software safety assurance, such as logic. Best to say logical approaches become effective when software is structured (statically or dynamically), for which we may refer to verification of unstructured assemblers, or refinement/Liquid types, or whatever, and we can say we are offering key principles.

I hope I can come back soon to do these changes. This also relates to Section C.

Kohei: I added a bit, cannot do this further now. I added a bit about comparisons with Sensoria, trying to spell out how it builds on it and how it differs from it. This part is certainly (1) too verbose and (2) not as clear as I wish it to be, but I hope some hints are there, and later we can elaborate.

I could not touch Section C, but along this line, we hope we can refer to novelties of the project: which gives a ground for why this Action is necessary.

My apologies that I could not fully expand this in this and other sections. I believe we can very convincingly argue, because it is a plain fact, that: Sensoria gives a basis and a fertile ground upon which, as one of the specific but promisingly high impacting directions, we are focusing in this Action on behavioural types.

Luca: I am unsure on the interpretation of the phrase ”…both because of the strongly tie…” in section B.1 (but it may be me)

Hans: The paragraph beginning with “Behavioural types are abstractions of the dynamic behaviour of components…” and the one that follows are a bit too long in my opinion. It would be better to first mention Java and C# and only then relate to behavioural types. Here is a shorter version:

There has been a steady increase in the sophistication of the data type systems of standard programming languages, culminating in, for example, the sophisticated generic type systems of Java and C#, which greatly enhance programmers' productivity and software reliability. Behavioural types go beyond this in that they can specify the permitted interaction within a distributed system. The behavioural type of a service specifies properties of interaction using a simple, expressive type language in a way that can be used to determine automatically if the service can satisfy desirable properties when it interacts with other services. This is analogous to the central structuring role of data and object types and associated interfaces in traditional sequential computing. Behavioural types can be applied in two complementary ways: (1) as the basis for static analysis, so that components can be certified as safe before being deployed; (2) as the basis for runtime monitoring, so that deviations from desired behaviour can be detected. In each case, the desirable properties of the components can be checked by cross-checking their interfaces. (2) is particularly useful when a static analysis of the total system is impossible, such as when a distributed service is realised through interactions among components located in different governing bodies and universities. In both (1) and (2), a given property may be described over different layers of behavioural types: for example, services are articulated by protocols through which different components interact, over which we may specify refined behavioural constraints, both being specified in different languages of behavioural types.

Ilaria: I noticed some typos + possible style improvements, listed next (page numbers refer to Simon's pdf version of Jan 23):

p 3, line -1: adding new functionalities → acquiring new functionalities

p 4, l 6: “instead of into” doesn't sound very nice

p 4, l 7: a collection or distributed nodes → … of …

        In the same line, I would take off "located inside or outside of the infrastructure", which seems a bit out of place here
                  

p 4, l -5: whether or not combination … can satisfy → whether or not a combination … will satisfy

p 5, l 8: not very nice to start a sentence with (2)

p 5, l 9: for components due when → for components when

p 5, l 11: over which we may specify … constraints → over which … constraints may be imposed

         (the passive form seems preferable here, and there is a "specified" occurring right afterwards)
         

p 5, l -12: there are two differences → … two main differences

p 5, l -10: a syntactic descriptions → … description

p 5, l -7: the research … make it clear → … makes it clear

p 5, l -3: “b.t. may be used in all stages of software development, including in development.” Something missing here ???

p 5, l -3: what does “the latter” refer to here? Actually, this whole sentence should be more carefully rephrased: the syntax it is not fully correct and the semantics not entirely clear to me

p 6, l 1: should we really mention POPL panel discussions?

p 6, l 2: programming language → … languages

p 6, l 2: distribute computing → distributed …

Ilaria: One further comment, about the comparison with Sensoria. I would formulate it a bit differently. Instead of explaining the differences between Betty and Sensoria, as if they were competing projects, I would present Betty as a natural evolution of Sensoria, clearly benefitting from the network of people and body of research put together by Sensoria, but also moving further in several respects and with a sharper focus on types.