ABSTRACT. Given the highly dynamic and extremely heterogeneous software systems composing the Future Internet, automatically achieving interoperability between software components without modifying them is more than simply desirable, it is quickly becoming a necessity. Although much work has been carried out on interoperability, existing solutions have not fully succeeded in keeping pace with the increasing complexity and heterogeneity of modern software, and meeting the demands of runtime support. On the one hand, solutions at the application layer target higher automation and loose coupling through the synthesis of intermediary entities, mediators, to compensate for the differences between the interfaces of components and coordinate their behaviours, while assuming the use of the same middleware solution. On the other hand, solutions to interoperability across heterogeneous middleware technologies do not reconcile the differences between components at the application layer. In order to allow for interoperability across layers, the “emergent middleware” paradigm was introduced. Emergent middleware leverages formal methods so as to be able to rigorously abstract and concretize protocols, and further reason about protocol mismatches so as to synthesize the necessary mediators that reconcile the differences between software components from the application down to the middleware layers. In this talk, I will review the foundations of emergent middleware and will then concentrate on its application to the development of distributing software systems contributing to the realization of the smart city vision, which involves the composition of highly heterogeneous systems.

ABSTRACT. This paper presents a technique for the certification of Cubicle, a model checker for proving safety properties of parameterized systems. To increase the confidence in its results, Cubicle now produces a proof object (or certificate) that, if proven valid, guarantees that the answer for this specific input is correct. The main challenges addressed in this paper are (1) the production of such certificates without degrading the performances of the model checker and (2) the construction of these proof objects so that they can be independently and efficiently verified by an SMT solver. Since the burden of correctness insurance now relies on this external solver, a stronger guarantee is obtained by the use of multiple backend automatic provers for redundancy. Experiments show that our approach does not impact Cubicle's performances and that we were able to verify certificates for industrial size verification problems. As a byproduct these certificates allowed us to find subtle and critical implementation bugs in Cubicle.

ABSTRACT. Loop under-approximation is a technique that enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique can speed up the detection of bugs significantly, it introduces redundant execution traces which may complicate the verification of the program. This holds particularly true for verification tools based on Bounded Model Checking, which incorporate simplistic heuristics to determine whether all feasible iterations of a loop have been considered.

We present a technique that uses \emph{trace automata} to eliminate redundant executions after performing loop acceleration. The method reduces the diameter of the program under analysis, which is in certain cases sufficient to allow a safety proof using Bounded Model Checking. Our transformation is precise---it does not introduce false positives, nor does it mask any errors. We have implemented the analysis as a source-to-source transformation, and present experimental results showing the applicability of the technique.

ABSTRACT. We present QPMC (Quantum Program/Protocol Model Checker), an extension of the probabilistic model checker ISCASMC to automatically verify quantum programs and quantum protocols. QPMC distinguishes itself from the previous quantum model checkers proposed in the literature in that it works for general quantum programs and protocols, not only those using Clifford operations.

ABSTRACT. Compositional verification techniques aim to decompose the verification of a large system into the more manageable verification of its components. In recent years, compositional techniques have gained significant successes following a breakthrough in the ability to automate assume-guarantee reasoning. However, automation is still restricted to simple acyclic assume-guarantee rules.

In this work, we focus on automating circular assume-guarantee reasoning in which the verification of individual components mutually depends on each other. We use a sound and complete circular assume-guarantee rule and we describe how to automatically build the assumptions needed for using the rule. Our algorithm accumulates joint constraints on the assumptions based on (spurious) counterexamples obtained from checking the premises of the rule, and uses a SAT solver to synthesize minimal assumptions that satisfy these constraints. To the best of our knowledge, our work is the first to automate circular assume-guarantee reasoning.

We implemented our approach and compared it with an established learning-based method that uses an acyclic rule. In all cases, the assumptions generated for the circular rule were significantly smaller, leading to smaller verification problems. Further, on larger examples, we obtained a significant speedup as well.

ABSTRACT. Constraint satisfaction problems can be expressed very elegantly in state-based formal methods such as B. However, can such specifications be directly used for solving real-life problems? We will try and answer this question in the present paper with regard to the university timetabling problem. We report on an ongoing project to build a formal model-based curriculum timetable validation tool where we use a formal specification as the basis to validate timetables from a student’s perspective and to support incremental modification of timetables. In this article we focus on expressing the problem domain, the formalization in B and our approach to execute the formal model in a production system using ProB.

ABSTRACT. In the theory of abstract interpretation, narrowing operators are used to improve the precision of the analysis after a post-fixpoint has been reached. This is especially true on numerical domains, since they are generally endowed with infinite descending chains which may lead to a non-terminating analysis in the absence of narrowing. We provide an abstract semantics which improves the analysis precision and show that, for a large class of numerical abstract domains over integer variables (such as intervals, octagons and template polyhedra), it is possible to avoid infinite descending chains and omit narrowing. Moreover, we propose a new family of narrowing operators for real variables which improves the analysis precision.

ABSTRACT. Networks are increasingly controlled by software, and bad updates can bring down an entire network. Network operators therefore need tools to determine the impact of changes. To address this, we present static differential analysis of software-defined network (SDN) controller programs. Given two versions of a controller program our tool, Chimp, builds atop Alloy to produce a set of concrete scenarios where the programs differ in their behavior. Chimp thus enables network developers to exploit the power of formal methods tools without having to be trained in formal logic or property elicitation. Furthermore, we show that there are many interesting properties that one can state about the changes themselves. Our evaluation shows that Chimp is fast, returning scenarios in under a second on several real applications.

ABSTRACT. Synchronous data flow graphs (SDFGs) are widely used to model digital signal processing and streaming media applications. In this paper, we present exact methods for static optimal scheduling and mapping of SDFGs on a heterogenous multiprocessor platform. The optimization criteria we consider are throughput and energy consumption, taking into account the combination of various constraints such as auto-concurrency and buffer sizes. We present a concise and flexible (priced) timed automata semantics of system models, which include an SDFG and a multiprocessor platform, and formulate the optimization goals as temporal logic formulas. The optimization and scheduling problems are then transformed to model checking problems, which are solved by UPPAAL (CORA). Thanks to the exhaustive exploration nature of model checking and the facility of the tools, we obtain throughput-optimal schedules that have a best energy consumption, and energy consumption-optimal schedules that have a best throughput. The approach is applied to two real applications, which shows that our approach can deal with moderate models within reasonable execution time and reveal the impacts of different constraints on optimization goals.

ABSTRACT. A feature model is a graphical structure presenting a hierarchical decomposition of features, called a feature diagram, with some possible crosscutting constraints between them. Cardinality-based feature models provide the most expressive language among the existing feature modeling languages. In this paper, we provide a reduction process, which allows us to go from a cardinality-based feature diagram to an appropriate regular expression. As for crosscutting constraints, we propose a formal language interpretation of them. In this way, we provide a formal language-based semantics for cardinality-based feature models. Accordingly, we describe a computational hierarchy of feature models, which guides us in how feature models can be constructively analyzed. We also characterize some existing analysis operations over feature models in terms of on languages and discuss the corresponding decidability problems.

ABSTRACT. Orchestration provides a general model of concurrent computations, although it is more often referred to in the context of service orchestrations describing the composition and management of (web) services. A minimal yet expressive theory of orchestration is provided by Orc, in which computations are modeled by site calls and their orchestrations through a few combinators. Using Orc, formal verification of correctness of orchestrations amounts to devising an executable formal semantics of Orc and leveraging existing tool support. Despite its simplicity and elegance, giving formal semantics to Orc capturing precisely its intended behaviors is far from trivial and has been of interest since Orc's inception primarily due to the challenges posed by concurrency, timing and the distinction between internal and external actions.

This paper presents a semantics-based approach for formally verifying Orc orchestrations using the K framework. Unlike previously developed operational semantics of Orc, the K semantics is not directly based on the interleaving semantics given by the reference SOS specification of Orc. Instead, the K semantics takes full advantage of true concurrency enabled by K. It also utilizes various K facilities to arrive at a clean, minimal and elegant semantic specification. To demonstrate the usefulness and applicability of the proposed approach, we also describe a specification for a robotics case study and provide initial formal verification results.

ABSTRACT. This paper contributes to the theory of typed first-order logic. We present a sound and complete axiomatization lifting restriction imposed by previous results. As a second contribution this paper provides complete axiomatizations for the type predicates instance_T, exactInstance_T, and functions cast_T indispensable for reasoning about object-oriented programming languages.