|
Research Goals
One dimension spans the
The other dimension is intended to highlight the complementary competences of the researchers and will be explained in detail below:
The themes are enumerated in increasing order of difficulty and risk; similarly the extensions of discrete techniques to stochastic and continuous ones are in increasing order of difficulty. While all combinations of properties and themes are part of the project, we do not expect within a five-year period to be able to fully answer all combinations of stochastic and continuous properties on the one hand and themes 2 and 3 on the other. Nonetheless we find the complete picture a useful guide for our research within MT-LAB. We conclude this section by identifying the key milestones of the project. These identify the importance of the prototypes developed within the project for testing the viability of our results on well-chosen scenarios. Theme 1: Static Analysis and Model Checking In static analysis [NNH99] the properties are often expressed by rather simple formulae. Usually the truth of such a formula can be determined trivially from an explicit representation: in the case of classical data flow analysis this is simply a (constant time) lookup whereas in more sophisticated analyses of cryptographic communication protocols, it may involve a limited (linear time) effort. Hence the main challenge is to compute a useful explicit representation of the program within reasonable time and space. This is where the powerful tool box of static analysis offers methods and techniques for the efficient (polynomial time) construction of explicit program representations. In model checking [CGP00] one usually considers the entire transition system of the program. The properties are expressed as formulae in powerful logics (e.g. CTL [CGP00]), possibly including probabilistic or stochastic behaviour (e.g. PCTL or CSL [KNP07]).The truth of such a formula is determined by a (polynomial time) compositional procedure on the explicit representation (exponentially larger than the program). This is where the powerful tool box of model checking offers methods and techniques for the compaction of explicit program representations (e.g. using Binary Decision Diagrams [Bry86]). Our hypothesis is that static analysis and model checking fundamentally solve the same problem – but using a different repertoire of techniques that must be combined in order to produce more powerful analysis techniques.
We will lift these studies to more general discrete models and to stochastic and continuous process models in order to validate the properties of interest. This may include the use of interval analysis for validating priced time automata, the use of slicing for a better treatment of continuous clocks when model checking UPPAAL [LPY97], and the development of over- and under-approximating analyses [NNN07] for the specification language of PRISM [KNP07]. The development of refinement techniques [BV01] may allow us to deal with the problems of scalability and it may be necessary to develop techniques that currently apply for integer-valued programs to also apply for real-valued programs. Our hypothesis will be validated if we are are successful in our approaches – also for applications to stochastic and continuous properties; alternatively it may be disproved if we can identify fundamental properties where the techniques provide complementary answers. Theme 2: Embedded Systems and Service Oriented Architectures Embedded systems are primarily concerned with relatively small, closed, and tightly coupled IT systems, where real-time performance and low resource usage pose hard requirements. The main points of interest are the synchronisation between components and their interfaces to the underlying hardware platform and the surrounding physical environment. The process algebras that have been used for describing them tend to have a more limited set of features where it is usually not too difficult to identify the components that should interact. In contrast, service oriented architectures are primarily concerned with relatively large, open, distributed, and loosely coupled IT systems where “Quality of Service” guarantees, such as expected response times and average resource consumption, pose soft requirements, which are naturally dealt with using stochastic models and analyses. The main focus is on the orchestration and choreography of services, the modelling of business processes [IBMbpm], and on avoiding unwanted interactions. The process algebras that have been used for describing them tend to have a rather rich set of features where it is often problematic to identify the components that are intended to interact. Our hypothesis is that there is no fundamental difference between embedded systems and service oriented architectures with respect to the techniques and properties required for their analysis and verification. We will demonstrate the hypothesis by identifying and aligning existing techniques used within the two areas with the purpose of identifying common techniques at an abstract level. Judging from our partners in the key European projects in these areas, ARTIST2 [ART2, BS05] for embedded systems and SENSORIA [SEN] for service oriented architectures, there currently is a fundamental gap between existing methods and techniques:
We hope to bridge this gap by developing a consistent family of formal methods and tools allowing for the modelling and analysis of both hard and soft requirements for open and dynamic systems. We will combine modelling formalisms allowing for multiple, quantitative properties to be expressed (e.g. stochastic as well as timing phenomena) and develop data structures and algorithms allowing for efficient analysis of these combined formalisms when applied to realistic case-studies. We will use and extend existing process models [LPS07] and tools [LPY97, DJJL02, HKM+03] supporting distinct quantitative aspects within a unifying logical framework. Our hypothesis will be validated if we are able to bridge the gap identified above; alternatively it may be disproved if we can demonstrate that the richness of process algebras for service oriented architectures make them fundamentally harder to analyse and reason about. Theme 3: Components and Global Characteristic Features
In contrast, characteristic features study a system as a whole in order to learn the global properties of interest. For example in the area of IT systems, complex security properties [Gol99] (e.g. privacy) are good examples because the overall security of a system is not realized by individual components alone but by their overall interaction. To deal with open systems the concept of “Hardest Attacker” [NNH02] (akin to the Dolev-Yao attacker in cryptographic protocols) enables a succinct encoding of the possible interaction of the environment. In an explicit confirmation of de Bono's considerations, Computer Science observes a continuous opposition between properties and systems that are decomposable and those that can only be analyzed globally. Numerous specific techniques and specific theories, struggle to combine the two aspects while balancing their efficacy and efficiency. Our hypothesis is that neither compositional methods nor characteristic features fully suffice for the effective analysis of complex IT systems – but that the analysis of systems can be fruitfully decomposed into a compositional component and a less demanding characteristic feature reducing the perceived cost of analysis. This hypothesis is the most far reaching and difficult of all we described above. It is our long term goal to advance its verification – a perspective that necessarily extends beyond the 5 year period. Within the scope of MT-LAB we intend to advance the understanding of the relation between global and compositional analysis by studying several more concrete problems. First, how far one can apply “Assume/Guarantee”, type and effect systems, compositional backwards reachability [SAH+00] and other compositional methods to hybrid and stochastic model checking and static analyses, and how the choice of a language, a decomposition and an analysis influences the size of induced abstractions. Furthermore, we will investigate the use of “counter-example guided refinement” [CGJLV00] to decrease the computational effort needed for static analyses of large models, and, finally, we shall design new static analyses for finding suitable decompositions for model checking algorithms. Milestones After 2 years MT-LAB will be conducting research at international level within combinations of discrete, stochastic and continuous models. This involves the use, modification or development of tools that can be used to evaluate the strength and weaknesses of the research results obtained, and a well chosen selection of application scenarios that have been identified with industrial collaboration (including the collaborators of the above mentioned projects). As a result, MT-LAB will have formulated a well-defined strategy for the development of prototype tools (possibly related to existing tools like MATLAB), as well as an educational program at the PhD and advanced MSc levels (in collaboration with the affiliated PhD schools: BRICS for AAU, FIRST for ITU and DTU, and ITMAN for DTU). After 3½ years MT-LAB will be internationally leading in research within combinations of discrete and continuous models. A palette of prototype tools will be available that have been used on the application scenarios in order to evaluate strengths and weaknesses of the research results obtained. Furthermore, MT-LAB will have formulated a strategy for creating larger and more applied research projects – funded by agencies such as the Danish Council for Strategic Research or the Danish National Advanced Technology Foundation – where the tools and methods can be applied to industrial case studies. After 5 years the applications to industrial case studies will have given fruitful feedback to the refinement and improvement of the methods and techniques developed in MT-LAB. Finally, we have established a plan for integration of the expertise gained among the participating universities (this includes the plans for future cooperation with industry and for the PhD educational program). Note: Research Task 7.2.A is a key for task for assessing the likelihood of disproving our hypothesis. |
The research plan is organised into three themes that challenge the complementary knowledge of the individual researchers of MT-LAB; this "matrix-structure" is illustrated in the diagram.
We will advance the state of the art in validation of properties of models of IT systems by developing a combined approach where the strengths of static analysis and model checking can interact. This will build on the pioneering work of [SS98] that recasts classical data flow analysis as an instance of model checking and on recent insights on the benefits of combining static analysis and model checking [BHT07]. Example developments may include:
The visible trend for future IT systems is the construction of service oriented architect-tures for mobile systems incorporating a number of embedded components. This may be exemplified by companies like IBM “bringing to embedded systems their expertice on open-standards architecture, systems integration and business process management” [IBMwp].
Compositionality focuses on structured design, where systems are built out of components. In compositional analysis the properties of a system are deduced from the properties of its components – see the figure. Taking a compositional approach often enables analysis of complex, otherwise intractable, models. As an example we mention the “Assume/Guarantee” reasoning [MC81, LNW06], where a component is analyzed with respect to a property under certain assumptions. Another example is the type and effect systems of e.g. [ANN99] that offers a compositional way of analysing intentional as well as extensional properties of systems.