Maximum 3-4 pages

• Describe the most important research tasks to be coordinated by the Action.

• Provide a structured, but not too detailed work plan flexible enough to permit the inclusion, at the implementation stage, of disciplinary perspectives and activities not foreseen during the preparation of the proposal. Keep the framework of the Action open and flexible.

• Explain the human and technical means to achieve the objectives described in section C.

• Remember that this section must be clear to non-specialists (even if the description may be more “technical”).

The following specific tasks provide a focus for research aimed at addressing the challenges presented by large-scale distributed software systems.

* Develop further theories of behavioural types so that behavioural types wich treat different properties (such as interaction patterns, safety, liveness, information flow) can be uniformly specified, integrated and assured.

* Develop meta-theories of behavioural types, enabling description of the features and relationships of a range of theories without duplication of effort.

• Extend behavioural type theory with quantitative features, to allow specification and analysis of non-functional properties such as response time or resource cost, giving a uniform basis for policy specifications and enforcement including service-level agreements.

* Further develop theoretical and practical understanding of sessions, roles and relationships, generalising from an identity-based view to a role-based view of the behaviour of session participants, so that theories can offer solid foundations of a broad range of programming language methodologies.

• Develop theories, tools and methodologies for the specification and implementation of fault tolerance and error recovery, which are essential in service-oriented distributed systems.

• Further develop theories, programming methodologies and tools based on choreography, orchestration and global types, to specify, analyse and assure properties of the collective interaction among software components.

• Develop theories and tools for the analysis of fairness and liveness properties in service-oriented systems.

• Develop theories and tools for the integrated specifications of security properties including secure information flow in a broad sense, and access control based on behavioural types, so that it enables effective runtime verifications.

• Design, develop and examine the dynamic runtime enforcement mechanism for behavioural types, so that we can specify new properties for distributed services at runtime and they can be enforced, with a formal assurance coming from theories of behavioural types.

• Develop mechanisms for negotiation, adaptation, extension and evolution of behavioural contracts and policies within long-lived environments for service-oriented software.

• Develop new production-level programming languages and programming environments based on behavioural types, building on the preceding experiments on prototype programming languages, with formal support for safety assurance and with emphasis on efficiency and scalability.

• Improve support for service-oriented programming in traditional programming paradigms, in particular object-oriented programming languages.

• Develop support for programming methodologies with many-core architectures following communication-oriented programming framework developed based on behavioural types, centring on the paradigm of communicating processes.

The Action is structured into four themes, each with a Working Group to co-ordinate its activity. These themes are (1) Foundations, (2) Security, (3) Languages, (4) Tools & Applications. Most of the topics listed above need to be addressed in relation to every theme, and the WGs will communicate to 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, as well as theories stimulated by use cases and requirements from the engineering practice.

• Do not mention explicitly the names of individual scientists, specific research institutions or other bodies (only exceptionally, if the Action cannot be implemented without the participation of a specific Institution, you should clearly mention this with the relevant explanation); Always remember that scientists who have not participated in the preparation are also entitled to join if their countries accept the MoU.

• Focus on work plan and methods of the Action and not on its organisation.

• If you plan Working Groups, you may mention their objectives and what they will achieve.

As mentioned above, the scientific work of the Action will be co-ordinated by four Working Groups. Each WG will promote its theme, ensure consistency and avoid duplication of effort, and form links across themes and with industry.

Communication-centred software and service-oriented computing raise new theoretical challenges, involving different research fields and cultural experiences. One of the central issues is the need to specify for and validate systems whose components are developed and maintained by third parties who are not necessarily trustworthy, which are dynamically searched and assembled, and which evolve in time. Another central point is the nature of the properties users and administrators wish to ensure for such systems, which are often interactional, reciprocal and global in nature (e.g. developers wish to build a distributed application whose individually developed components interact without deadlock; or users wish to maintain fair and safe usage of a service as a whole).

These problems have been attacked on the basis of several different theories, mainly process algebras, logic and type theory. The main issue of the WG is that of putting on the same footing these apparently heterogeneous aspects of software development and verification, including concurrent and distributed programming disciplines, specification and verification of software components, static and dynamic checking of protocol and policy compliance.

The concepts of session, conversation and choreography have emerged as structuring principles for concurrent and distributed systems. Behavioural types merge ideas from process algebras and type theories, so that they provide a common foundation for structured software development and automatic verification, both statically and dynamically, which are well-suited to concurrent and dynamic systems. The tasks of this WG include:

1. To develop the uniform and general theory of behavioural types clarifying how abstract process descriptions should be used as computational invariants and module interfaces.
2. To face the problem of expressivity of type languages w.r.t. safety, liveness and fairness of systems, in the context of both theoretical calculi and programming languages, investigated by WG3 of this Action, while keeping the effectiveness and efficiency of the verification procedures (including type systems) through which we can ensure such properties.
3. To define a theory of quantitative behavioural types, viewed as an abstract operational model accounting for non-functional aspects of the system's behaviour.

The present state of the art shows a plethora of formalisms, often sharing the same roots but with significant theoretical differences. The WG will aim at developing a common formal framework, allowing for comparison and study of different approaches currently developed by the participating teams. By focusing on the conceptual and technical problems emerging in the activity of the other WGs, WG1 is aimed at the integration and further development of different domain specfic approaches, especially with respect to qualitative and quantitave aspects of system behaviour, and the development of new solutions taking advantage of their strengths in the respective domains of application.

Enforcement of security properties is an important application domain of behavioural types. In particular, analyses of information flow, which is an essential aspect of both data confidentiality and data integrity and requires a dependency analysis, can greatly benefit from the use of behavioural types, since these also allow for a direct description of the causal dependencies in interprocess communication and the order in which data will flow between processes. From a different viewpoint, instead of specifying safety properties for individual, disparate messages, their specifications become much more amenable in terms of specifiability and effective validations when they are given based on protocols.

Information flow and associated technologies can also serve as a basis of other important security concerns such as privacy protections, authenticity and integrity (access control), for many of which behavioural types will allow a uniform basis for specifications, validations and runtime enforcement.

Applications of behavioural types to concrete case studies and development of type theories that target specific application domains are among the concrete results and unifying themes of the Action. They are therefore also the focus of this WG. The Action will achieve its objectives through the joint development of theoretical foundations and tools.

The activities include:

1. The development of type theories that make it possible to reason about security properties such as secrecy, authenticity, confidentiality and integrity for communication protocols, and the identification of other forms of security properties that are amenable to type-based analyses using new type theories.
2. The development of algorithmic techniques for type-based analyses of such security properties, for both static and dynamic validations.

The type theories and resulting algorithmic techniques should apply both to pure mathematical models of interaction-based computation (such as process calculi), new programming languages based on behavioural types, and to existing programming and specification languages.

The WG will build on experience gained from the following past successes of its experts:

• leading major efforts in the development of type theories for security issues;
• developing specialized tools for reasoning using types to reason about security issues.

The Action is therefore in a unique position to develop type theories of this kind and to foster collaboration within the community. It is important that WG2 coordinates its activities with the other WGs of the Action; this will happen through joint meetings and via the involvement of working group members in other working groups.

The infrastructure of WG2 will consist of a repository of type theories for security properties. These type theories will be applied and validated by tool development and case studies within WG4.

The study and development of behavioural type theories aims at the integration of behavioural types into mainstream programming languages and at their use as a guideline to design new languages that incorporate them. The working group focuses on research in which we develop theories, principles and key runtime mechanisms for programming with behavioural type systems as intrinsic structures. Actual development of programming environments and tool chains which can be used by developers is covered by WG4 described below. The Languages working group will pursue two distinct lines of research, aimed at the integration of behavioural types in:

1. Mainstream, general-purpose languages;
2. Domain-specific languages.

Concerning mainstream languages, it is necessary to consider two orthogonal aspects, namely the programming paradigm and the degree of integration of behavioural types within the languages.

Regarding the former, this WG will target different programming paradigms, including, but not restricted to, object-oriented languages and functional languages. As programs are meant to manipulate data, of particular interest to WG3 are the XML and the JSON data formats.

• Object-oriented languages are relevant for their widespread adoption in the current development of software, for the wealth and popularity of tools that are available, and because objects nicely fit a distribution model to which behavioural types can be applied naturally.
• Functional languages are relevant for their qualities of being easily endowed with high-level type-theoretic and concurrent extensions, for their natural support to parallelism, and since they permit rapid prototyping.
• XML/JSON/YAML data formats are interesting for the role of XML and JSON as the de facto standard exchange paradigms in distributed, service-oriented computing, and need be integrated as part of description languages for protocols and other global properties.

Within each of these programming paradigms, the WG will investigate the following, increasingly invasive ways to integrate the support for behavioural types:

• By means of explicit code annotations in the form of comments or pragma directives. In this way, (fragments of) behavioural type disciplines can be plugged into existing languages without requiring unreasonable changes to their syntax and semantics. Tools can then be developed for analysing and processing explicitly annotated code, in a similar way to what currently happens with many IDEs for program development. In order to maintain the amount of information provided by the programmer to a minimum, it may be desirable to confine the use of explicit annotations to APIs dedicated to communication and synchronisation, and to devise suitable type inference techniques for automatically deriving type information in code that uses the APIs.
• By means of syntax extensions to be handled by pre-processing. In this way, high-level programming constructs (for communication, synchronisation, coordination) are more easily associated with high-level type information than the corresponding implementations in terms of low-level communication primitives.
• By means of conservative extensions of existing languages. Extensions of core research-oriented languages such as, for object-oriented programming, Featherweight Java, will be considered first. Then, results will be validated in fully-featured languages.

Regarding the first point, note the applicability of behavioural types to traditional languages include both statically and dynamically typed languages, such as Python, through runtime verifications.

Concerning domain-specific languages (DSLs), the WG will follow two distinct research tracks:

• The adoption of behavioural types within existing DSLs designed for application areas and use-cases to which behavioural types naturally apply, such as business process and workflow management systems, service-oriented programming, distributed security protocols, distributed queries for semi-structured data.
• The development of new domain specific languages explicitly targeted at exploiting the characteristics of behavioural types and aimed at the coordination and/or orchestration of wide-area distributed services.

This WG will co-ordinate work in two directions.

1. The development of software tools including programming language environments, as a linkage between behavioural type theories and development practice for large-scale distributed systems.
2. The organisation of case studies to apply theories, languages, methodologies and tools developed throughout the Action, to the practice of large-scale software development, centring on the above mentioned software tools.

The aim is to develop tools with which developers can build, analyse and maintain systems incorporating behavioural types. They include analysis tools that are applicable to already running applications built with standard languages and development methods e.g by automatically deriving and annotating code with type information in communication APIs as described in WG3 above. They also include tools for extensions of existing languages and new domain specific languages developed in WG3. Concrete examples of such software tools include:

• A concrete embodiment of developed programming principles as concrete programming environments. This includes, if it is a new programming language, production-level language processors (parsers) and runtime; or, if it is for existing programming languages, as APIs and runtime libraries. These environments include bindings to major communication transports such as TCP, UDP, HTTP, AMQP and 0MQ, as well as messaging formats such as XML, JSON and Google protocol buffer.
• A tool chain in which a developer can specify contracts for inter-component communications, project such a contract onto each endpoint through projection algorithms, and, through multiple language bindings, use these endpoint constraints to validate source code written in a concrete programming language, to ensure that, when these components are executed and interact with each other, they conform to the original contract.
• A complementary tool chain for regulating behaviours of distributed applications, which enable specifications of behavioural constraints at various levels, starting from bare protocols to more complex policies, and generates data for runtime monitoring, so that interaction behaviours of applications can be monitored at runtime, through their injection into run-time systems in order to check compliance with the specified contracts.

The central point of having these software tools is to make it possible for developers to effectively benefit from the safety and liveness guarantees for the constructed software systems provided by the theories of behavioral types without having to deal with the complexity of understanding the theories themselves.

Regarding the second point, we will first identify the main strengths and application areas of the tools developed in research projects lead by members of the Action. This effort will produce a suit of case-studies emphasising the benefits of the various tools, at the same time contrasting and comparing them. Afterwards, we will organise use-case explorations, development/industrial experiments and feedback from industry, through the contacts that have been cultivated by participants in the Action during their own nationally-funded research projects during the last several years. Involving these development partners in the Action, via the activities of this WG, will maximise the benefit for them and for the Action, by putting them into contact with a broader group of researchers that will provide valuable feedback on each existing application and/or tool.

The programming languages developed or adapted by WG3, and the tools and software development environments developed by this WG, will be channelled towards the industrial partners for trial in suitable case studies and large-scale explorations; conversely, the requirements of application domains such as healthcare, financial services, e-science and development of large-scale distributed software infrastructure, will be fed into the activities of all WGs in order to maintain a focus on the needs of end-users.

Simon: Please precede remarks with your name.

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

kohei: Thank you for putting Application section, Simon. I will edit a bit, will discuss with Thomas and Nobuko. Still not getting how long each section should be (reading the preceding full proposals).

kohei: I have done with a first draft, will discuss with Thomas and Nobuko.

Simon: I think the length is OK at the moment; that is a rough guide.

Luca: At the end of D1 it is stated that ”…WGs will communicate…”. I wonder whether it would make sense to use a slightly different verb (like cooperate or collaborate) that more explicitly suggests the need of a cost action.

Pawel: Working Group 1: “The main issue of the Action is that”; I think this text should only describe the goals of the WG, not the whole Action (and there is a bit of repetition here, with respect to the intro of the whole proposal).

Joachim: WG1 the enumeration on top p 13: item 1: omit the last words “namely as types”

item 2: “effectiveness and efficiency” is there a difference?

The following para, middle “WG1 is issued at” perhaps better “aimed at”

WG2 same page end of first para: “well-suited” no hyphen

last words of that para “for them” omit, it is unclear what “them” refers to

Hans: I have revised the description of WG2.

Ugo I made the editings. I also deleted “effectiveness”, although this is not the same as efficiency. Indeed it means just computable in the recursion theoretic literature. Also there are undecidable type systems (system F, intersection types, F-bounded polymorphism etc.), and not every safety or liveness property is itself decidable. But Joachim's point could be that we are not addressing such kind of logically untractable problems. Moreover, since this has been confusing for us, it would be surely missleading for the referees. Hence deleted.

Luca: Revised WG3

Simon: I think this section is very good now. Please read the discussion in II.C for suggestions about how we can use that section.

Thomas: I would propose adding a 4th bullet point to WG1: 4: Adaptation, extension and evolution

Thomas: WG 2 on security talks about case studies in bullet 3 and producing tools in the last paragraph. This is of course the way to validate the theories experimentally - but shouldn't that be covered in WG4 in order to have a clear separation of the deliverables of the WGs? If so, one could remove bullet point 3 and change the last line about tools to say that the theories developed in the WG will be validated experimentally by the development of tools and performing case studies within WG4.