Strict Standards: Declaration of Doku_Renderer_metadata::table_open() should be compatible with Doku_Renderer::table_open($maxcols = NULL, $numrows = NULL, $pos = NULL) in /var/www/operationalsemantics.net/public_html/behaviouralwiki/inc/parser/metadata.php on line 24

Strict Standards: Declaration of Doku_Renderer_metadata::table_close() should be compatible with Doku_Renderer::table_close($pos = NULL) in /var/www/operationalsemantics.net/public_html/behaviouralwiki/inc/parser/metadata.php on line 24

C. PRELIMINARY WORK PROGRAMME

Especially if the proposal is very complex and based on participation of research teams from different fields of research interacting in a specific way, you may wish to explain how this has been envisaged, at a more concrete level than that indicated in the draft Technical Annex.

Relationships between the Working Groups

The sequence of Working Groups: WG1 (Foundations), WG3 (Languages) and WG4 (Tools & Applications) forms a chain from theory to practice. As such, there will be significant interaction between WG1 and WG3, and between WG3 and WG4.

WG2 (Security) addresses a cross-cutting concern, and a result it will have significant interaction with the other three Working Groups.

What this amounts to is strong interaction between every pair of Working Groups, with the exception that WG1 (Foundations) will have less direct interaction with WG4 (Tools & Applications). Most of the interaction between WG1 and WG4 will be mediated through WG2 (Security) and WG3 (Languages).

Work Programme and Schedule

WG1: Foundations

Year 1

During the first year of the Action, WG1 will prepare a state-of-the-art report on behavioural type theory and its existing use as a foundation for programming languages. The report will provide a comprehensive picture of the research community and its achievements to date, and identify areas in which different approaches to behavioural type theory are conflicting, overlapping or deficient. This knowledge will be used both to plan further foundational research and as a basis for responding to the needs of WG2 (Security) and WG3 (Languages), during subsequent years.

Year 2

The second year will be devoted to expressivity issues, by promoting a workshop on the themes of safety, liveness and fairness properties of concurrent and mobile systems, as well as information flow analysis, and by discussing ideas about how such properties can be expressed by means of behavioural types. This involves the question of how experience and knowledge gathered by means of different models than process algebra and type theory, like true concurrency models and model checking, can be imported in terms of behavioural types, and to what extent known problems from the world of distributed computing can be faced in the setting of type systems.

At the end of the second year of the Action, the language designs developed in WG3, possibly applied to important scenarios/case studies arising from WG4 (Tools), will be used as test beds to check the effectiveness and suitability of the formal techniques developed in WG1. This will generate topics for WG1's activity during the second half of the Action, e.g. modifications/extensions to the models considered or to the verification techniques.

Year 3

The third year will be primarily dedicated to the problems of probabilistic and quantitative properties of concurrent and distributed systems, and of their formalizations within the theory of behavioural types. The work will start with the pereparation of a report on the most promising attempts at embodying such aspects into process algebras and behavioural type systems, and will be concluded by a meeting on the same themes. Quantitative and probabilistic analysis are relevant both to WG2 (Security) and to WG4 (Tools), giving the opportunity of testing the results from WG1 against case studies and concrete applications.

Year 4

In the final year, WG1 will work towards an overall assessment of the results obtained both theoretically and practically. This will lead to a final report surveying the achievements as well as collecting the most interesting open questions that the scientific community working in the area should address in the future.

WG2: Security

Year 1

During the first year of the Action, WG2 will prepare a state-of-the-art report on security mechanisms for large-scale distributed and service-oriented systems. The report will consider security from the perspective of each of the other three Working Groups, in consultation with them: (1) what are the practical security issues in large service-oriented systems, and how well are they handled at present? (2) how is security supported by the programming languages presently used for large-scale distributed software development, and is this support considered to be adequate? (3) to what extent does the theoretical basis for security analysis in large-scale distributed and service-oriented systems allow security to be reliably certified? This report will form the basis for detailed planning of the activities of WG2 and its interaction with the other Working Groups during subsequent years.

Year 2

In its study of new type theories for security properties, WG2 will build on the foundational work in WG1 and keep interacting with WG1 throughout the project. Security properties such as authenticity and secrecy can be understood as secure information-flow properties based on the notion of non-interference. There is already work on information flow in the related area of control flow analysis and also type-based analyses that use correspondence assertions. Also, there is a considerable body of work on the relationship between secure information flow and trust management. In the second year of the Action and onwards, WG2 will therefore examine how behavioural types can be used to give more precise analyses of the secure information flow properties that have been identified in Year 1. WG2 will also address security issues that are not easily understood as information flow properties, and investigate how these they can be captured by type theories. Finally, WG2 will relate its work on type theories to that pursued in WG1 and to existing work on security analyses that use a type-like approach, including control flow analyses.

The practical usefulness of behavioural types for security will depend on their algorithmic properties. In Year 2 and onwards, WG2 will therefore interact with WG4 to determine how security properties can be checked algorithmically. In particular, type checking must be decidable within reasonable complexity bounds and type reconstruction should be possible.

Year 3

Security properties, and in particular those based on non-interference, are important in actual program development. In Year 3, WG2 will therefore examine how behavioural types can be used to guarantee security properties in real programming languages, both when designing new languages, which should be security-minded from their very inception, and when extending existing ones. This work will benefit and interact with the work on type theories for session calculi based on the pi-calculus or the psi-calculus. More specifically, WG2 will examine how behavioural types can be used to guarantee security properties in real programming languages, both when designing new languages, which should be security-minded from their very inception, and when extending existing ones. As such, the work of WG2 will be strongly connected with that on programming language design developed by WG3, which takes correctness concerns into consideration.

Starting in Year 3, WG2 will also work in close connection with WG4 to discover the security requirements of specific application domains, and match these requirements with suitable formalisms for security. An important activity will be to investigate concrete cases (including ones studied by WG4 in Year 2) and determine how behavioural types can be used to reason about security properties for them.

Year 4

The final year of the Action will be devoted to developing software tools that make use of the algorithmic properties of behavioural types. A litmus test for the usefulness of behavioural types for security will be the possibility of applying them to the domains and case-studies studied in Year 3.

WG3: Languages

Year 1

During the first year of the Action, WG3 will prepare a state-of-the-art report on behavioural types in programming languages. This will be approached from two directions: (1) a survey of current experiments and prototypes in adding behavioural types to existing languages or designing new languages that incorporate behavioural types; (2) an assessment of current practice in software development for distributed and service-oriented systems, in the absence of support for behavioural types, and identification of the areas in which behavioural types are most likely to prove beneficial. The report will provide a starting point for detailed planning of a strategy to exploit behavioural types in practical programming languages during the remainder of the Action.

Year 2

In year 2, WG3 will explore non-invasive ways of enriching existing programming and domain-specific languages with behavioural type disciplines allowing for a greater number of correctness properties to be automatically verified. Non-invasive means that behavioural types will not, at this stage, be deeply integrated into programming languages; rather, they will be handled at a pre-processing or external tool level. This work will include the study of program annotations (in the form of comments or pragma directives), the definition of program macros to be expanded during pre-processing, as well as the definition of APIs specialized to communication, synchronization, and co-ordination making use of the augmented expressiveness given by behavioural type disciplines.

Year 3

During the third year, WG3 will elaborate on the experience of the previous year and on the feedback received from WG4 regarding the application of behavioural type disciplines to the case studies. In doing so, it will identify the expressiveness gap between the constructs available in current programming languages and the needs that have emerged in the scenarios taken under consideration, and will devise high-level language constructs allowing, on the one hand, for a higher level of abstraction in designing and developing distributed and/or cooperative applications and, on the other hand, for more precise type checking.

Year 4

The final year of the Action will be devoted to studying conservative extensions of both general-purpose and domain-specific languages, with a particular focus on the implementation of (possibly pluggable) components for compilers and run-time environments. This work will also require the study of adapters and interfaces for inter-working between legacy code and programs using these new constructs. The increased expressiveness and precision provided by behavioural types will be exploited for the automatic or assisted generation of adapters and interfaces. The final report of WG3 will summarise and reflect on progress, and indicate directions for future work by continuing projects in this area.

WG4: Tools & Applications

Year 1

During the first year of the Action, WG4 will prepare a report on potential case studies that can be undertaken in collaboration with the industrial participants. This will begin with an assessment of real software systems and the problems that companies face in developing them, and then identify a range of systems or sub-systems that exemplify particular issues. If possible this will include case studies related to systems with a high social impact, such as integrated European health services or voter management systems for electronic elections. The report will be used to plan application-focused work during the remainder of the Action.

Year 2

During the second year, WG4 will select a few case studies based on systems identified during the first year, and try to use the available languages (identified in the state-of-the-art report by WG3) and tools to re-implement or re-structure them, or to implement exemplar systems that incorporate the key features, including security aspects, of the case studies. The second year report will use this experience as the basis for a critique of the available programming languages and tools for behavioural types, and will compile a wish-list for WG2 (Security) and WG3 (Languages) to work towards.

Year 3

By the beginning of year 3, WG3 will have produced designs for programming language extensions based on the idea of using annotations or pragma directives to express behavioural typing properties. WG4 will spend the third year developing compiler extensions and analysis tools based on these extensions. Towards the end of the year it will be possible to test these compilers and tools on the same case studies used in the previous year's work, and assess their effectiveness. The report at the end of this year will reach conclusions about the benefits and limitations of this non-invasive approach.

Year 4

The final year will be devoted to the implementation of programming languages in which behavioural type systems are an intrinsic aspect of the design. This stage will be closely connected to the results from WG3 during the third year, and also to the ongoing work of WG3 during the final year. As far as possible, prototype programming languages will be tested on the same case studies as before, and there will be considerable feedback from the experience of the case studies into the design and implementation of libraries and APIs. The final report, when combined with that of WG3, will present a comprehensive view of the experience of the design, implementation and test cycle for novel programming languages incorporating behavioural type systems.

In this last year, WG4 will organise a workshop to present to industrial partners the solutions to the case studies developed previously. This workshop will show how the tools and the language-based approaches selected in the other WGs can address the real problems and software development challenges the industry faces. Furthermore, WG4 will prepare joint pilot projects with the industrial partners to be developed in their companies and project applications to funding agencies to pursue the work of the Action.

Notes and raw material below this point

Some very quick notes by Simon.

I would like to explain how each WG will interact with the others. I am thinking of

WG1:Foundations —- WG3:Languages —- WG4:Tools & Applications

as a chain from foundations to applications, in which each WG will interact with its neighbours.

WG2:Security is a cross-cutting concern and will interact with each of the other three WGs.

We should say what each WG will produce:

Foundations will produce scientific papers covering general principles, and specific results about small calculi abstracted from language features being considered by WG3. PL designers within the Action will be able to ask foundational researchers to check consistency of proposed language features.

The activities of WG3 play a pivotal role on the Action, as they serve as a bidirectional interface between WG1 and WG4, and will foster a close collaboration with the units working on the foundations of behavioural type theories and those developing tools for analysis and development of software. On the one hand, WG3 will base the development of new programming language designs (in the form of type languages, annotations, new programming constructs) on the formalisms and theories studied by WG1 and will make them available for use in trial tools and applications in WG4. On the other side, language designs will also be driven by the needs of application domains, communicated by WG4, and will be validated by work in WG1. Since some research units of the proposed collaboration network are already exploring the development of concrete prototypes relying on sophisticated behavioural type theories using currently available programming languages, the Action will enable participating researchers to benefit from the reciprocal exchange of proposals and feedback concerning the integration of behavioural types in mainstream and domain-specific languages.

Tools & Applications will provide a forum to help coordinating, integrating, and disseminating the various tools developed by the researchers in the action. In particular, we are interested in comparing and identifying the strengths of the tools, by finding an adequate suit of problems. Moreover, we will look for application areas and case studies for the results achieved in the context of the other working groups. Finally, it will find out what industry needs in various application domains and communicate the requirements back to WG3. Members of this WG will include those who already have the best industrial contacts, and they will act as matchmakers between industrialists and other participants in the action. The objectives listed will be pursued as follows: in year 1 we will first identify the applications and tools we will work with, and then characterise their aims and strengths, comparing their common aspects; in year 2 we shall develop an adequate suit of problems to express the usability, complementarity, and benefits of the various tools; in years 3 and 4 we will organise exchange sessions with software companies to present the tools, receive feedback on usability and requirements, and to look for and select concrete problems and joint pilot projects.

WG2: Security

The focus of WG2 is a cross-cutting concern that is relevant for each of the remaining working groups. As a consequence, the results of WG2 will be visible both as publications that relate behavioural types to security issues and as transversal work arising from joint efforts by different working groups. The scientific programme of WG2 ranges from theoretical studies on security type systems to language design and investigation of case-studies and tools, along the following lines:

1) General type theories for security properties.

Security properties such as authenticity and secrecy can be understood as secure information-flow properties based on the notion of non-interference. There is already work on information flow in the related area of control flow analysis and also type-based analyses that use correspondence assertions. Also, there is a considerable body of work on the relationship between secure information flow and trust management. WG2 will examine if and how behavioural types can be used to give more precise analyses of secure information flow properties, develop new behavioural type theories for these properties and relate them to existing work, including control flow analyses. Moreover, WG2 will also address security issues that are not easily understood as information flow properties, and investigate how these they can be captured by type theories.

In its study of new type theories for security properties, WG2 will build on the foundational work in WG1 and keep interacting with WG1 throughout the project.

2) Programming language design for security.

Security properties, and in particular those based on non-interference, are important to ensure in actual program development. This work will benefit from the foundational work on type theories, some of which will deal with session calculi based on the pi-calculus or the psi-calculus, and will carry over the same principles to the setting of actual programming languages. More specifically, WG2 will examine how behavioural types can be used to guarantee security properties in real programming languages, both when designing new languages, which should be security-minded from their very inception, and when extending existing ones.  As such, the work of WG2 will be strongly connected with that on programming language design developed by WG3, which takes correctness concerns into consideration.

3) Application domains

WG2 will also work in close connection with WG4 to discover the security requirements of specific application domains, and match these requirements with suitable formalisms for security. An important activity will be to investigate concrete cases and determine how behavioural types can be used to reason about security properties for them.

4) Software tools

The practical usefulness of behavioural types for security will depend on their algorithmic properties. In particular, type checking must be decidable within reasonable complexity bounds and type reconstruction should be possible. As these are also concerns for WG4, WG2 will interact with WG4 to determine how security properties can be checked algorithmically and how the proposed algorithms can be incorporated into actual software tools. A litmus test for the usefulness of behavioural types for security will be the possibility of applying them to the domains and case-studies identified in 3).

PRELIMINARY WORK PROGRAMME: discussion

Simon: Please precede remarks with your name.

Hans: I added a short description of the programme for WG2.

Simon: I think we can write a substantial amount here, if we want to. Several pages. We don't have to, but I am worried that if we don't write more, it will look as if we don't have plans. Can we write anything about how the work of each WG will evolve during the 4 years of the Action?

Antonio: I added some text to the description of the programme for WG4. If you think the contribution is in the right direction, I can extended it.

Luca: Changed a bit description of the programme for WG3. :?: I am unsure how to fit what follows into the programme Example: ML-style datatypes can be included in a language, but could alternatively be used as the input to a tool that generates corresponding class definitions in a language like Java. Similar examples with contracts or session types.

Simon: I was trying to express the idea that programming language concepts can be used as the basis for tools, as well as (or instead of) integrating them into new or existing languages. So this could be a point of contact between WG3 and WG4. What I wrote in this section initially was some very quick notes, suggesting ideas for expanding on Sec.D and especially the relationship between the WGs.

Simon: I think it would be good to use this section to give an impression of (1) how the WGs will interact with each other (this part has already been started); (2) how the activity of each WG will evolve during the course of the Action. Can we give an approximate idea of what will be the focus during each year?

We have written somewhere else that each WG will produce an annual report on its activity, but that also at the end of Year 1, each WG will produce a state-of-the-art report on its theme. So that can be the focus for Year 1. What comes after that? For example, if we want WG1 to try to unify foundations, then the state-of-the-art survey is the obvious first step; next it should try to find ways to remove redundancy or inconsistency between approaches, or maybe organise work on foundational aspects that are missing from current approaches.

WG3 could try to take new behavioural typing concepts, first use them as the basis for tool designs, and later try to produce new PL designs in which behavioural types are deeply integrated. This involves collaboration with WG4.

I hope that the colleagues who have written Sec.D can be inspired to write a similar length here, along the lines of the existing draft and my suggestions above.

Thomas: I think the above description of how the different work packages are connected is important, but wondered if it should be given already in the section describing the work packages..? In any case, I think a figure illustrating the interaction between work packages would be good to have along with this text.

Thomas: Simon, when you propose describing evolution of each WG do you think of giving (types of) deliverables/milestones for each year for each WG? I would assume the initial focus of WG4 is to collect existing tools (and tool proposals), case studies and overview of industrial partners in one place - and organize a workshop for the presentation and discussions of such. The next year there will be some input from WG3 on the basis of which new tools can be developed and case studies be performed. The final milestone must be to have tools and case studies successfully demonstrating the applicability of behavioural types in the development of large-scale and/or production distributed systems developed by indudstrial partners.

Ugo: I have written the WG1 workplan by eliging a main theme each year. This is a debatable idea and the choosen thems are put into an order which reflects my personal view. I invite differently minded writers to propose anithing better if they will.

 
fullcost-additional-work.txt · Last modified: 2012/01/26 20:40 by simon
 
Except where otherwise noted, content on this wiki is licensed under the following license:CC Attribution-Share Alike 3.0 Unported
Recent changes RSS feed Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki