Differences

This shows you the differences between two versions of the page.

fullcost-programme [2012/01/27 14:54]
kohei [D.1 Scientific focus]
fullcost-programme [2012/01/27 15:21] (current)
kohei [D.2 Scientific work plan – methods and means]
Line 55: Line 55:
 === Working Group 1: Foundations === === Working Group 1: Foundations ===
  
-Communication-centred software and service-oriented computing raise new theoretical challenges, involving different research fields and cultural experiences. central point is the need to specify and validate systems whose components are developed and maintained by third parties who are not necessarily trustworthy, are dynamically searched and assembled, and evolve in time.+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 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 compliance.+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: 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:
  
-   - To develop the theory of behavioural types clarifying how abstract process descriptions should be used as computational invariants and module interfaces. +   - To develop the uniform and general theory of behavioural types clarifying how abstract process descriptions should be used as computational invariants and module interfaces. 
-   - To face the problem of expressivity of type languages w.r.t. safety, liveness and fairness of systems when specified both by theoretical calculi and by the languages investigated by WG3 of this Action, while keeping the efficiency of the type systems capturing such properties.+   - 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.
    - To define a theory of quantitative behavioural types, viewed as an abstract operational model accounting for non-functional aspects of the system's behaviour.    - 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 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.+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.
  
 === Working Group 2: Security === === Working Group 2: Security ===
  
-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.+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.  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. 
Line 76: Line 78:
  
   - 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.   - 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.
-  - The development of algorithmic techniques for type-based analyses of such security properties.+  - 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 mathematical models of computation (such as process calculi) and to existing programming and specification languages.+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: The WG will build on experience gained from the following past successes of its experts:
Line 98: Line 100:
   - Domain-specific languages.   - 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.+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. 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.
Line 104: Line 106:
   * 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.   * 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.   * 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 data formats are interesting for the role of XML and JSON as the de facto standard exchange paradigms in distributed, service-oriented computing.+  * 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: Within each of these programming paradigms, the WG will investigate the following, increasingly invasive ways to integrate the support for behavioural types:
Line 111: Line 113:
   * 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 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.   * 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: Concerning domain-specific languages (DSLs), the WG will follow two distinct research tracks:
Line 133: Line 137:
 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. 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.+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.
 ====== SCIENTIFIC PROGRAMME: discussion ====== ====== SCIENTIFIC PROGRAMME: discussion ======
  
 
fullcost-programme.txt · Last modified: 2012/01/27 15:21 by kohei
 
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