At the core of the methodology we propose is the notion of type, intended as information associated with some computational entity for which the type provides a formal specification of its behavior at a high level of abstraction. There are two key aspects in this definition:
1. the fact that types have a formally defined meaning. It is our belief that the analysis of large and complex systems can be pursued exclusively through the application of rigorous techniques.
2. the fact that types raise the level of abstraction. Since the computational units and the systems that we want to describe are often infinite-state, they can be effectively analyzed only once they have been abstracted into manageable terms (the types). Also, the complexity and scale of the systems we target requires modular forms of analysis, which is naturally enabled by types.
For a long time types have been though of as information statically associated with computational entities. This contrast with the nature of the systems we target in two respects. Firstly, because interacting entities evolve over time as they synchronize with each other. Consequently, they can be accurately described only by types that evolve along with the entity they describes. Second, we want to consider scenarios in which computational entities misbehave with respect to the type they declare to respect. The first problem has been recently addressed by the introduction of the notion of behavioral type, namely of type describing a process (for example, in terms of the messages sent and received) as opposed to an expression. For the second problem, we propose an evolution of behavioral types from being operational and prescriptive to being declarative and normative. This will be achieved by giving types the ability to describe the nature and constituents of environments at a higher-level of abstraction and by specifying more detailed information on the characteristics of environments and on the relationship between events occurring in them.
The project is articulated by considering two scenarios of increasing complexity, which will be addressed in temporal order:
Scenario A. In this scenario computational units are considered trusted and respectful of their types. It is expected that in this setting stronger correctness properties can be enforced.
Scenario B. Computational units may misbehave, in the sense that their observed behaviours can diverge from that described in their type. This setting makes the (realistic) assumption that some components of a system have been developed/provided by third parties which are not necessarily trusted.
Within each scenario we will work along the following three steps, which are expected to be inter-dependent:
1. Develop types for describing computational units and their environments.
2. Develop type-based analysis techniques (type systems, type inference, monitoring, etc.) for the enforcement of correctness properties.
3. Implement proof-of-concepts tools for validating the developed theories.
The project goals will be realized through parallel work on both sites coordinated during the joint visits and the short meetings during the simultaneous participation to scientific venues. Researchers from Novi Sad and Turin will jointly work on the fist two steps of both scenarios, while the third step will be done mainly by researchers from Turin. The first visit of Novi Sad research team in Turin is planned for the autumn 2013, when participants will present relevant topics, emphasizing open questions and common ground for the joint work. Another meeting of representatives of the two groups will take place on 25-26 September, in Madrid, during the WG meetings of the COST action IC1201. The visit of Turin representatives to Novi Sad is planned for the December 2013, when researchers will report on the progress made and set up work plan for the following two years.