Compositional Algebra of CONNECTors

The CONNECT project aims to develop a novel network infrastructure to allow heterogeneous networked systems to freely communicate with each other via on-the-fly synthesis of emergent connectors. The role of Work Package 2 (WP2) is to investigate the foundations and verification methods for composable connectors, so that support is provided for composition of networked systems, whilst enabling automated learning, reasoning and synthesis. In the second year, we focused our attention on providing an underpinning for a framework capable of supporting the dimensions of interest to the project, and the generalisation of assume-guarantee properties beyond probabilistic safety properties, in addition to supporting the automated learning of assumptions. In this deliverable, we report on work carried out in two streams, compositional theory of connector behaviours and compositional assume-guarantee verification for probabilistic automata, which we are beginning to bring together. At the theory level, we first considered several probabilistic models, focusing on their interactive behaviour and asynchronous parallel composition. We then conducted a survey of the different formalisms of component models from the viewpoint of whether they supported a number of operators (e.g. parallel composition, conjunction and quotient) and a refinement relation. Based on this, we concluded that interface automata were one of the most amenable formalisms for basing an algebra of CONNECTors upon. We have formulated a preliminary (non-quantitative) connector algebra for resolving protocol mismatches based on interface automata. A software tool IAAnalyzer was implemented to allow users to create interface automata models using the connector algebra. In order to address the need for a quantitative extension, we have proposed a specification theory based on a probabilistic extension of interface automata. In the second stream, we continued our work on compositional assume-guarantee verification for probabilistic automata, extending the framework to allow, as assumptions and guarantees, a broader class of quantitative multi-objective properties which include probabilistic liveness and expected rewards. We also proposed a novel learning technique based on the L* algorithm, which automatically generates probabilistic (safety) assumptions using the results of queries executed by a probabilistic model checker. These two techniques have been implemented for PRISM, a well-known probabilistic model checker. Finally, we have laid the foundations for a comprehensive framework capable of modelling the quantitative (in particular the probabilistic) behaviour of arbitrary components and associated compositional assume-guarantee proof rules. Connectors arise as certain types of components. This framework is intended to integrate the two streams of work.