       
@ 2013 - Site Map - Credits |
 |
Formal Foundations for CONNECTors |
| |
|
| Objectives |
|
Our research on the foundations and verification methods for composable CONNECTors aims at providing support for composition of networked systems, whilst enabling automated learning, reasoning and synthesis. We specifically investigate a modelling framework for CONNECTors so that complex interaction behaviours can be expressed (with respect to both functional and non-functional properties), and formulate algorithms for quantitative and qualitative verification and their proof-of-concept implementation. |
Our works spans :
- Formalising the notions of connector and component, characterising the types of interaction and identifying a verification approach, capable of capturing non-functional properties.
- Formulating a compositional modelling and reasoning framework for components and CONNECTors.
- Formulating techniques for interoperability checking, in the presence of dynamic behaviours and non-functional properties.
- Implementing a prototype for a quantitative verification framework for connectors and components, capable of handling dynamic scenarios and non-functional properties
|
| Modelling Framework for CONNECTors |
To model components and connectors we have formulated a fully compositional specification theory based on a component model conceptually similar to interface automata. Components support asynchronous communication in which outputs are non-blocking. Further, they are not required to be input-enabled, which allows for stronger environmental assumptions. The framework admits a substitutive refinement preorder for safely interchanging connectors and components, and provides the operations of parallel composition, for examining the structural behaviour of systems, conjunction (or shared refinement) for independent development, and quotient to synthesise components thus supporting incremental development. The inclusion of disjunction and hiding is also straightforward. Besides this, an extension with data has additionally been provided for the specification theory.
To greater support the objectives of Connect, a mediator synthesis methodology based on the specification theory has been developed by making use of the quotient operator. Unlike existing applications of quotient, we do not require that the components needing to communicate have common interaction primitives; we allow for the relationships to be specified in an ontology. Our framework can be automated in the sense that we use an abstract goal not requiring user intervention in its specification. That is, the goal specifies desirable principles of communication, such as avoidance of communication mismatches and deadlock-freedom, rather than specifying how the mediator should be synthesised. Integration with synthesis in WP3 has been demonstrated by linking the algorithmic approach to connector synthesis developed in that work package with the quotient operator of the specification theory. |
| Automated Verification Framework |
Quantitative verification techniques have been developed for several years and numerous successful applications have been reported in the literature. However, applying these techniques to verify CONNECTed systems built from CONNECTors and components remains challenging. Compositional verification is a promising technique for a system comprising multiple interacting components, since it enables us to analyse each component in isolation, instead of verifying the much larger model of the whole system.
In Year 3, we developed a complete assume-guarantee technique, which can generate probabilistic assumptions automatically by a new L*-style learning methods. This technique includes an assume-guarantee framework for verifying probabilistic safety properties of synchronous probabilistic systems modelled as discrete-time Markov chains (DTMC). Assumptions about system components are represented as probabilistic finite automata (PFAs) and the relationship between components and assumptions is captured by weak language inclusion. More concretely, PFAs represent weighted languages, mapping finite words to probabilities. An assumption about a system component M is represented by a PFA that gives upper bounds on the probabilities of traces being observed in M. This is an inherently linear-time relation, which is well-known to be difficult to adapt to compositional techniques for systems that exhibit both probabilistic and nondeterministic behaviour. Therefore, we restrict our attention to fully probabilistic systems. To do so, we model components as probabilistic I/O systems (PIOSs), which, when combined through synchronous parallel composition, result in a DTMC. The relation between a PIOS M and a PFA A representing an assumption about M is captured by weak language inclusion. Based on this, we formulated a symmetric proof rule for verifying probabilistic safety properties on a DTMC composed of two PIOSs.
In order to implement our approach, we gave an algorithm to check weak language inclusion, reducing it to the existing notion of (strong) language inclusion for PFAs. Although checking PFA language equivalence (that each word maps to the same probability) is decidable in polynomial time, checking language inclusion is undecidable. We proposed a semi-algorithm to check language inclusion; in the case where the check fails, a minimal counterexample is produced. We also developed a novel technique for learning PFAs, which we used to automatically generate assumptions. Our algorithm, like L*, is based on active learning, posing queries in an interactive fashion about the PFA to be generated.
|
 |
|
Selected Publications
|
Further Information
More information about the work on formal foundations for CONNECTors can be found from the Publications page
|
|
