To gain a thorough insight into the arena of connector modelling, we surveyed a number of existing connector algebra formalisms and, where appropriate, their quantitative extensions. The surveyed formalisms (Wright, Kell Calculus, BIP, Bigraphical reactive systems, and Reo) were evaluated against eight key dimensions deemed to be important for an ideal CONNECTor modelling formalism, as agreed by the project consortium. The dimensions of interest were compositionality, incrementality, scalability, compositional reasoning, re-usability, evolution, extra-functionality, and tool support, with a particular emphasis on non-functional aspects. Besides the survey, we contributed to the implementation of the Reo modelling toolkit, developed an approach to dynamically synthesise a service behaviour protocol, and discussed non-functional parameters to be captured by the connector model, useful to perform dependability/QoS analysis. However, despite this extra experimentation, the survey still concluded that none of the surveyed modelling formalisms satisfied all eight dimensions.
As a result, we decided to progress the work at two levels. At the high-level, we continued working on a high-level formalism for CONNECTors to meet the eight dimensions of interest. This involved looking at a number of automata-based models combining interface theories. In particular, we examined interface automata, I/O automata, interactive Markov chains and interval Markov chains, together with quantitative extensions of the former two. Our motivation for studying these models related to the emphasis they have on interaction types and compositional operators, which are of direct relevance to CONNECT. Subsequently, we developed a basic algebra capable of modelling mediators for functionally equivalent yet behaviourally mismatching protocols. The semantics of terms of the algebra are given in terms of interface automata. Tool support for this algebra is well underway, and we are currently looking to extend the algebra with quantitative attributes.
It is imperative that our formalism has an intuitive semantic mapping onto labelled transition system models, such as deterministic automata (used for learning from scenarios and synthesis) or probabilistic automata (used for QoS analysis). Therefore, we are also investigating relations between the defined high-level formalism for CONNECTors and formalisms available for non-functional analyses as well. In parallel with this, we continue to develop automated verification techniques in the context of parameterised LTSs (or their finite-state variants known as automata), as sketched below .
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 the case of non-probabilistic models, assume-guarantee reasoning has proved successful. For probabilistic systems, compositional approaches have also been studied, but a distinct lack of practical progress has been made. We address this limitation, presenting a fully-automated technique for compositional verification of systems exhibiting both probabilistic and nondeterministic behaviour. We also augment these models with one or more reward structures that assign real values to certain transitions of the model. In fact, these can associate a notion of reward with the executions of the model and can be used to check a wide range of quantitative measures of non-functional properties.
A natural extension of these techniques is to consider multiple objectives. For example, rather than verifying two separate properties such as "loss of connection occurs with probability at most 0.001" and "the expected total latency is below 50 units of time", we might ask whether it is possible for a CONNECTed system to satisfy both properties simultaneously, or to investigate the trade-of between the two objectives as some parameters of the system are varied.
