We have so far surveyed existing connector modelling formalisms, covering not only classical connector algebra formalisms, but also, where appropriate, their corresponding quantitative extensions. The survey includes a selection of existing formalisms (Wright, Reo, Kell Calculus, BIP, Bigraphical reactive systems, Reo) for the specification and analysis of software connectors and components. First, through broad project discussions, we identified eight key dimensions for an ideal modelling formalism for CONNECT (compositionality, incrementality, scalability, compositional reasoning, re-usability, evolution, extra-functionality and tool support), paying particular emphasis to non-functional aspects. In the survey, we briefly summarised and evaluated the selected formalisms with respect to the eight dimensions. In addition, 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. The conclusion from the survey is that none of the modelling formalisms satisfies all eight dimensions of CONNECT.
As a result, we have decided to progress the work at two levels. At the high-level, we continue working on a high-level formalism for CONNECTors that meets the eight dimensions identified in CONNECT. In particular, we focus on interaction types and composition operators. Moreover, we aim for such a formalism to have 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). This requires that we investigate relations between the defined high-level formalism for CONNECTors and formalisms available for non-functional analyses as well. In parallel, 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
We have developed the first compositional verification technique, i.e., assume-guarantee method, for probabilistic systems. In this work, we suppose that both assumptions and guarantees are safety properties. A regular safety property
represents a set of infinite words, denoted
, which is characterised by a regular language of bad prefixes, that is, finite words whose extension is not in
. We usually write
to represent the fact that the component
is guaranteed to satisfy the quantitative safety property
under the quantitative safety assumption
. Verification of
requires the use of multi-objective model checking. The conventional single-objective approach allows us to check whether, for all adversaries (or, dually, for at least one adversary), the probability of some property is above (or below) a given bound. Multi-objective queries allow us to check the existence of an adversary satisfying multiple properties of this form by a reduction to a linear programming (LP) problem. The quantitative compositional verification is achieved by the following assume-guarantee rules:
Our compositional verification approach has been implemented in PRISM, and demonstrated experimentally that its performance is superior to non-compositional verification. This work serves as the foundation of future research concerning the more general, quantitative, compositional reasoning framework for components and connectors. As a means of addressing scalability, we have investigated an automated abstraction-refinement technique for probabilistic real-time systems. Probabilistic Timed Automata (PTAs) are a probabilistic model combining probabilistic choice, nondeterminism and dense time. The semantics of a PTA is defined as an (infinite-state) Markov decision process (MDP). Stochastic two-player games extend MDPs by allowing two types of nondeterministic choice, controlled by separate players. Each transition of a stochastic game 
comprises three choices: first, player 1 picks an available action; next, player 2 selects a distribution for the action; finally, a successor state is chosen at random according to the distribution. We use a stochastic game 
to represent an abstraction of an MDP 
. In 
, player 2 choices represent nondeterminism present in 
and player 1 choices represent additional nondeterminism introduced through abstraction. In a symbolic state of the game abstraction of a PTA, player 1 first picks a concrete PTA state and then player 2 makes a choice over the actions that become enabled after letting time pass from the concrete state. By quantifying over strategies for players 1 and 2, we can obtain both lower bounds and upper bounds on the minimum and maximum reachability probabilities of 
. The game-based abstraction approach has been extended with refinement techniques. Inspired by non-probabilistic counterexample-guided abstraction refinement, the idea is that an initially coarse abstraction is iteratively refined until it is precise enough to yield useful verification results. Crucial to this approach is the use of the lower and upper bounds provided by a stochastic game abstraction as a quantitative measure of the precision of the abstraction.
