In this paper we offer an efficient controller synthesis algorithm for assume-guarantee specifications of the form \(\varphi _1 \wedge \varphi _2 \wedge \cdots \wedge \varphi _n \rightarrow \psi _1 \wedge \psi _2 \wedge \cdots \wedge \psi _m\). Here, \(\{\varphi _i,\psi _j\}\) are all safety-MTL\(_{0, \infty }\) properties, where the sub-formulas \(\{\varphi _i\}\) are supposed to specify assumptions of the environment and the sub-formulas \(\{\psi _j\}\) are specifying requirements to be guaranteed by the controller. Our synthesis method exploits the engine of Uppaal-Tiga and the novel translation of safety- and co-safety-MTL\(_{0, \infty }\) properties into under-approximating, deterministic timed automata. Our approach avoids determinization of Büchi automata, which is the main obstacle for the practical applicability of controller synthesis for linear-time specifications. The experiments demonstrate that the chosen specification formalism is expressive enough to specify complex behaviors. The proposed approach is sound but not complete. However, it successfully produced solutions for all the experiments. Additionally we compared our tool with Acacia+ and Unbeast, state-of-the-art LTL synthesis tools; and our tool demonstrated better timing results, when we applied both tools to the analogous specifications.

(1) CISS, CS, Aalborg University, Alborg, Denmark; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (3) Google Inc., Zurich, Switzerland, CA, United States

We present a new technique for verifying Weighted Metric Temporal Logic (WMTL) properties of Weighted Timed Automata. Our approach relies on Statistical Model Checking combined with a new monitoring algorithm based on rewriting rules. Contrary to existing monitoring approaches for WMTL ours is exact. The technique has been implemented in the statistical model checking engine of Uppaal and experiments indicate that the technique performs faster than existing approaches and leads to more accurate results.

This chapter contains sections titled: Introduction UPPAAL UPPAAL-CORA UPPAAL-TIGA TAPAAL ROMÉO: a tool for the analysis of timed extensions of Petri nets Bibliography

We consider the problem of controller synthesis under imperfect information in a setting where there is a set of available observable predicates equipped with a cost function. The problem that we address is the computation of a subset of predicates sufficient for control and whose cost is minimal. Our solution avoids a full exploration of all possible subsets of predicates and reuses some information between different iterations. We apply our approach to timed systems. We have developed a tool prototype and analyze the performance of our optimization algorithm on two case studies.

This paper studies the problem of computing Nash equilibrium in wireless networks modeled by Weighted Timed Automata. Such formalism comes together with a logic that can be used to describe complex features such as timed energy constraints. Our contribution is a method for solving this problem using Statistical Model Checking. The method has been implemented in UPPAAL model checker and has been applied to the analysis of Aloha CSMA/CD and IEEE 802.15.4 CSMA/CA protocols.

We present a novel approach and implementation for analysing weighted timed automata (WTA) with respect to the weighted metric temporal logic (WMTL≤). Based on a stochastic semantics of WTAs, we apply statistical model checking (SMC) to estimate and test probabilities of satisfaction with desired levels of confidence. Our approach consists in generation of deterministic monitors for formulas in WMTL≤, allowing for efficient SMC by run-time evaluation of a given formula. By necessity, the deterministic observers are in general approximate (over- or under-approximations), but are most often exact and experimentally tight. The technique is implemented in the new tool Casaal. that we seamlessly connect to Uppaal-smc. in a tool chain. We demonstrate the applicability of our technique and the efficiency of our implementation through a number of case-studies.

In this paper we propose a general framework for distributed statistical model checking of networks of priced timed automata. The first contribution is a new algorithm to distribute sequential hypothesis testing without introducing bias in the results. The second contribution is an implementation of this algorithm in Uppaal. The major contribution is an experimental and analytical evaluation of the approach through case studies, including an analysis of the SMC algorithm itself.

This paper offers a survey of UPPAAL-SMC, a major extension of the real-time verification tool UPPAAL. UPPAAL-SMC allows for the efficient analysis of performance properties of networks of priced timed automata under a natural stochastic semantics. In particular, UPPAAL-SMC relies on a series of extensions of the statistical model checking approach generalized to handle real-time systems and estimate undecidable problems. UPPAAL-SMC comes together with a friendly user interface that allows a user to specify complex problems in an efficient manner as well as to get feedback in the form of probability distributions and compare probabilities to analyze performance aspects of systems. The focus of the survey is on the evolution of the tool - including modeling and specification formalisms as well as techniques applied - together with applications of the tool to case studies.

Statistical Model Checking (SMC) is a trade-off between testing and formal verification. The core idea of the approach is to conduct some simulations of the system and verify if they satisfy some given property. In this paper we show that SMC is easily parallelizable on a master/slaves architecture by introducing a series of algorithms that scale almost linearly with respect to the number of slave computers. Our approach has been implemented in the UPPAAL SMC toolset and applied on non-trivial case studies.

Model checking is one of the most commonly used methods for checking program correctness. In this method, one verifies a program model given by the Kripke structure (labeled transition system) rather than the program itself. The specification is usually given as a temporal logic formula. In many subtasks of model checking, it is necessary to use relations that are defined on the set of program models and preserve the satisfiability of temporal logic formulas. There exist many relations of this kind, which are called simulation relations. In the present paper, we introduce a tool designed to check a wide class of simulation relations between finite models of programs. This tool is based on the simulation checking game-theoretic approach. The tool consists of two components. The first component is the formal language, which allows one to define various simulation relations in terms of an antagonistic two-player game. The second component is a software tool that, given two labeled transition systems and simulation definition, is able to check whether this simulation is satisfied between these labeled transition systems.

A term t is called a template of terms t 1 and t 2 iff t 1 = tη 1 and t 2 = tη 2, for some substitutions η 1 and η 2. A template t of t 1 and t 2 is called the most specific iff for any template t′ of t 1 and t 2 there exists a substitution ξ such that t = t′ξ. The anti-unification problem is that of computing the most specific template of two given terms. This problem is dual to the well-known unification problem, which is the computing of the most general instance of terms. Unification is used extensively in automatic theorem proving and logic programming. We believe that anti-unification algorithms may have wide applications in program analysis. In this paper we present an efficient algorithm for computing the most specific templates of terms represented by labelled directed acyclic graphs and estimate the complexity of the anti-unification problem. We also describe techniques for invariant generation and software clone detection based on the concepts of the most specific templates and anti-unification.

This paper describes an algorithm for finding software clones, which works at the level of abstract syntax trees and is thus conceptually independent of the source language of the analyzed programs. We use a notion of clones which captures replacement of subtrees in the program AST, and is formally based on the notion of anti-unification. This allows us to capture syntactic structural similarity with increased accuracy and express it in metrics. We have implemented this algorithm in a tool named Clone Digger, freely available under the GPL license, and which currently supports the Python, Java and Lua languages. We report on initial experimental results and comparisons with similar tools.

In this paper we focus on property-preserving preorders between timed game automata and their application to control of partially observable systems. We define timed weak alternating simulation as a preorder between timed game automata, which preserves controllability. We define the rules of building a symbolic turn-based two-player game such that the existence of a winning strategy is equivalent to the simulation being satisfied. We also propose an on-the-fly algorithm for solving this game. This simulation checking method can be applied to the case of non-alternating or strong simulations as well. We illustrate our algorithm by a case study and report on results.

This paper describes a new algorithm for finding software clones.It is conceptually independent of the source language of the analyzed programs, working at the level of abstract syntax trees.The algorithm considers that two sequences of statements form a clone if one of them can be obtained from the other by replacing some subtrees.To our knowledge this notion was not previously employed in the literature.It allows to take into account all information on the syntactic structure of a program.We have implemented this algorithm in the tool Clone Digger.It currently supports the Python and Java languages.

The main goal of model checking is to verify whether a model of a given program satisfies some given specification. In this paper models are regarded as fair or ordinary Kripke structures whereas specifications are represented by formulae branching-time temporal logics (CTL*x or ACTL*x). Model checking can be substantially enhanced by reducing the size of models under consideration. Usually this is achieved by using binary relations on the set of Kripke structures that preserve the satisfiability of temporal formulae. It is known that stuttering bisimulation (simulation) relation preserves CTL*x (respectively ACTL*x) for ordinary Kripke structures. In this paper we present a fair game stuttering bisimulation(simulation) relation which preserves CTL*x (ACTL*x) for fair Kripke structures, and algorithms for computing stuttering (bi)simulation which utilize usual and parity games. If n is the number of states and m the number of transitions in a finite states transition system then our algorithms for computing stuttering simulation and bisimulation for ordinary Kripke structures is proved to have O(m^2) time and space complexity, and our algorithms for computing the same relations for fair Kripke structures appear to have O(m^2n^2) time and O(m^2) space complexity. Thus the verification of CTL*x-formulae on a model M (ordinary or fair) can be reduced to the verification of these formulae on a smaller model.