Models, Algorithms, Logics and Tools

One of the key demands of cyberphysical systems is that they meet their safety goals. Timed Automata has established itself as a formalism for modelling and analysing the real-time safety aspects of cyberphysical systems. Increasingly it is also demanded that cyberphysical systems meet a number of security goals for confidentiality and integrity. Information Flow Control is an approach to ensuring that there are no flows of information that violate the stated security policy.We develop a language based approach to the modelling and analysis of timed systems that allows to incorporate considerations of information flow control. We define a type system for information flow that takes account of the non-determinism and clocks of timed systems. The adequacy of the type system is ensured by means of a non-interference result.

We derive a Nivat theorem for weighted unranked tree automata which states that their behaviors are exactly the functions which can be constructed from recognizable unranked tree languages and behaviors of very simple weighted unranked tree automata by using operations like relabelings and intersections. Thereby we prove the robustness of the weighted unranked tree automata model introduced recently. Moreover, we derive a similar theorem for weighted ranked tree automata. The characterizations work for valuation monoids as weight structures; they include all semirings, bounded lattices, and computations of averages of weights.

We survey the specification formalism of modal transition systems (MTS). We discuss various extensions of MTS, their relationships and modelling capabilities. The extensions include more involved modalities, quantitative aspects, or infinite state spaces. Further, we discuss problems arising in verification and analysis of these systems. We cover refinement checking, model checking and synthesis, standard logical and structural operations as used in specification theories as well as the respective tool support.

Quantitative regular expressions (QREs) have been recently proposed as a high-level declarative language for specifying complex numerical queries over data streams in a modular way. QREs have appealing theoretical properties, and each QRE can be compiled into an efficient streaming algorithm for its evaluation. In this paper, we generalize the notion of Brzozowski derivatives for classical regular expressions to QREs. Such derivatives immediately lead to an algorithm for incremental evaluation of QREs. While this algorithm does not have better time or space complexity than the previously known evaluation technique, it has the benefit of being simpler to explain and easier to prove correct.

Biological systems such as regulatory or gene networks can be seen as a particular type of distributed systems, and for this reason they can be modeled within the Timed Automata paradigm, which was developed in the computer science context. However, tools designed to model distributed systems often require a computer science background, making their use less attractive for biologists. ANIMO (Analysis of Networks with Interactive MOdeling) was built with the aim to provide biologists with access to the powerful modeling formalism of Timed Automata in a user friendly way. Continuous dynamics is handled by discrete approximations.In this paper we introduce an improved modeling approach that allows us to considerably increase ANIMO’s performances, opening the way for the analysis of bigger models. Moreover, this improvement makes the introduction of model checking in ANIMO a realistic feature, allowing for reduced computation times. The user interface of ANIMO allows to rapidly build non-trivial models and check them against properties formulated in a human-readable language, making modeling a powerful support for biological research.

We construct bicategories of Markov processes where the objects are input and output sets, the morphisms (one-cells) are Markov processes and the two-cells are simulations. This builds on the work of Baez, Fong and Pollard, who showed that a certain kind of finite-space continuous-time Markov chain (CTMC) can be viewed as morphisms in a category. This view allows a compositional description of their CTMCs. Our contribution is to develop a notion of simulation between processes and construct a bicategory where the two-cells are simulation morphisms. Our version is for processes that are essentially probabilistic transition systems with discrete time steps and which do not satisfy a detailed balance condition. We have also extended the theory to continuous space processes.

We propose a systematic approach to generate highly parallel benchmark systems with guaranteed temporal properties. Key to our approach is the iterative property-preserving parallel decomposition of an initial Modal Transition System, which is based on lightweight assumption commitment. Property preservation is guaranteed on the basis of Modal Contracts that permit a refinement into a component and its context while supporting the chaining of dependencies that are vital for the validity of considered properties. We illustrate our approach, which can be regarded as a simplicity-oriented variant of correctness by construction, by means of an accompanying example.

We present a generic algorithmic scheme for learning languages defined over large or infinite alphabets such as bounded subsets of $$\mathbb {N}$$ and $$\mathbb {R}$$, or Boolean vectors of high dimension. These languages are accepted by deterministic symbolic automata that use predicates to label transitions, forming a finite partition of the alphabet for every state. Our learning algorithm, an adaptation of Angluin’s $$L^*$$, combines standard automaton learning by state characterization, with the learning of the static predicates that define the alphabet partitions. We do not assume a helpful teacher who provides minimal counter-examples when the conjectured automaton is incorrect. Instead we use random sampling to obtain PAC (probably approximately correct) learnability. We have implemented the algorithm for numerical and Boolean alphabets and the preliminary performance results show that languages over large or infinite alphabets can be learned under more realistic assumptions.

Milner’s CCS is a cornerstone of concurrency theory. This paper presents CCS as a cornerstone of concurrency practice. CCS is the semantic footing of pseuCo, an academic programming language designed to teach concurrent programming. The language features a heavily simplified Java-like look and feel. It supports shared-memory as well as message-passing concurrent programming primitives, the latter being inspired by the Go programming language. The behaviour of pseuCo programs is described by a formal translational semantics mapping on value-passing CCS and made executable using compilation to Java. pseuCo is not only a language but an interactive experience: provides access to a web application designed for first hands-on experiences with CCS and with concurrent programming patterns, supported by a rich and growing toolset. It provides an environment for students to experiment with and understand the mechanics of the fundamental building blocks of concurrency theory and concurrent programming based on a complete model of the program behaviour. Altogether this implements the TACAS (Teaching Academic Concurrency to Amazing Students) vision.

This paper studies the decidability and small model property of process equations of the form $$\begin{aligned} (P|\varPi _{i=1}^{n}C_i(X_i))\backslash L\equiv (Q|\varPi _{j=1}^{m}D_j(Y_j))\backslash K \end{aligned}$$ where P, Q are finite state processes, $$X_i,Y_j$$ are process variables, and $$C_i(X_i)$$ , $$D_j(Y_j)$$ are process expressions linear in $$X_i$$ and $$Y_j$$ respectively. It shows that, when $$n+m>1$$ , the equation problem is not decidable and does not have small model property for any equivalence relation $$\equiv $$ which is at least as strong as complete trace equivalence but not stronger than strong bisimilarity.

Since the early 1990’s, classical temporal logics have been extended with timing constraints. While temporal logics only express contraints on the order of events, their timed extensions can add quantitative constraints on delays between those events. We survey expressiveness and algorithmic results on those logics, and discuss semantic choices that may look unimportant but do have an impact on the questions we consider.

In this short note, we establish a link between the theory of Moore Interfaces proposed in 2002 by Chakraborty et al. as a specification framework for synchronous transition systems, and the Assume/Guarantee contracts as proposed in 2007 by Benveniste et al. as a simple and flexible contract framework. As our main result we show that the operation of saturation of A/G contracts (namely the mapping $$(A,G)\mapsto (A,G{\vee }{\lnot }A)$$), which was considered a drawback of this theory, is indeed implemented by the Moore Game of Chakraborty et al. We further develop this link and come up with some remarks on Moore Interfaces.

Variational systems (system families) allow effective building of many custom system variants for various configurations. Lifted (family-based) verification is capable of verifying all variants of the family simultaneously, in a single run, by exploiting the similarities between the variants. These algorithms scale much better than the simple enumerative “brute-force” way. Still, the design of family-based verification algorithms greatly depends on the existence of compact variability models (state representations). Moreover, developing the corresponding family-based tools for each particular analysis is often tedious and labor intensive.In this work, we make two contributions. First, we survey the history of development of variability models of computation that compactly represent behavior of variational systems. Second, we introduce variability abstractions that simplify variability away to achieve efficient lifted (family-based) model checking for real-time variability models. This reduces the cost of maintaining specialized family-based real-time model checkers. Real-time variability models can be model checked using the standard UPPAAL. We have implemented abstractions as syntactic source-to-source transformations on UPPAAL input files, and we illustrate the practicality of this method on a real-time case study.

In cyber-physical applications many programs have hard real-time constraints that have to be stringently validated. In some applications, there are programs that have hard deadlines, which must not be violated. Other programs have soft deadlines where the value of the response decreases when the deadline is passed although it is still a valid response. In between, there are programs with firm deadlines. Here the response may be occasionally delayed; but this should not happen too often or with too large an overshoot. This paper presents an extension to an existing approach and tool for checking hard deadline constraints to the case of firm deadlines for application programs written in Safety-Critical Java (SCJ). The existing approach uses models and model checking with the Uppaal toolset; the extension uses the statistical model checking features of Uppaal-smc to provide a hold on firm deadlines and performance in the case of soft deadlines. The extended approach is illustrated with examples from applications.

Probabilistic timed automata are a formalism for modelling systems whose dynamics includes probabilistic, nondeterministic and timed aspects including real-time systems. A variety of techniques have been proposed for the analysis of this formalism and successfully employed to analyse, for example, wireless communication protocols and computer security systems. Augmenting the model with prices (or, equivalently, costs or rewards) provides a means to verify more complex quantitative properties, such as the expected energy usage of a device or the expected number of messages sent during a protocol’s execution. However, the analysis of these properties on probabilistic timed automata currently relies on a technique based on integer discretisation of real-valued clocks, which can be expensive in some cases. In this paper, we propose symbolic techniques for verification and optimal strategy synthesis for priced probabilistic timed automata which avoid this discretisation. We build upon recent work for the special case of expected time properties, using value iteration over a zone-based abstraction of the model.

Runtime Verification is a light-weight approach to systems verification, where actual executions of a system are processed and analyzed using rigorous techniques. In this paper we shall narrow the term’s definition to represent the commonly studied variant consisting of verifying that a single system execution conforms to a specification written in a formal specification language. Runtime verification (in this sense) can be used for writing test oracles during testing when the system is too complex for full formal verification, or it can be used during deployment of the system as part of a fault protection strategy, where corrective actions may be taken in case the specification is violated. Specification languages for runtime verification appear to differ from for example temporal logics applied in model checking, in part due to the focus on monitoring of events that carry data, and specifically due to the desire to relate data values existing at different time points, resulting in new challenges in both the complexity of the monitoring approach and the expressiveness of languages. Over the recent years, numerous runtime verification specification languages have emerged, each with its different features and levels of expressiveness and usability. This paper presents an overview and a discussion of this design space.

We revisit model-based testing for labelled transition systems in the context of specifications that may contain divergent behaviour, i.e., infinite paths of internal computations. The standard approach based on the theory of input-output conformance, known as the ioco-framework, cannot deal with divergences directly, as it restricts specifications to strongly convergent transition systems. Using the model of Quiescent Input Output Transition Systems (QIOTSs), we can handle divergence successfully in the context of quiescence. Quiescence is a fundamental notion that represents the situation that a system is not capable of producing any output, if no prior input is provided, representing lack of productive progress. The correct treatment of this situation is the cornerstone of the success of testing in the context of systems that are input-enabled, i.e., systems that accept all input actions in any state. Our revised treatment of quiescence also allows it to be preserved under determinization of a QIOTS. This last feature allows us to reformulate the standard ioco-based testing theory and algorithms in terms of classical trace-based automata theory, including finite state divergent computations.

In the analysis of reactive systems a quantitative objective assigns a real value to every trace of the system. The value decision problem for a quantitative objective requires a trace whose value is at least a given threshold, and the exact value decision problem requires a trace whose value is exactly the threshold. We compare the computational complexity of the value and exact value decision problems for classical quantitative objectives, such as sum, discounted sum, energy, and mean-payoff for two standard models of reactive systems, namely, graphs and graph games.

Heterogeneous hardware/software systems that include many components with different characteristics offer great potential for high performance and energy-efficient computing. To exploit this potential, adaptive allocation and scheduling algorithms are needed for selecting software variants and mapping them to processing elements that attempt to achieve a good balance between resource-awareness and performance. The evaluation is typically carried out using simulation techniques. However, the space spanned by the possible combinations of hardware/software variants and management strategies is huge, which makes it nearly impossible to find an optimum using simulation-based methods. The purpose of the paper is to illustrate the general feasibility of an alternative approach using probabilistic model checking for families of systems that are obtained by varying, e.g., the hardware-software combinations or the resource management strategies. More precisely, we consider heterogeneous multi-processor systems based on tiled architectures and provide a tool chain that yields a flexible and comfortable way to specify families of concrete systems and to analyze them using the probabilistic model checker PRISM and ProFeat as a front end. We illustrate how the family-based approach can be used to analyze the potential of heterogeneous hardware elements, software variants and adaptive resource management and scheduling strategies by applying our framework to a simplified model of the multi-processor Tomahawk platform that has been designed for integrating heterogeneous devices.

In this paper, we study the notion of admissibility in timed games. First, we show that admissible strategies may not exist in timed games with a continuous semantics of time, even for safety objectives. Second, we show that the discrete time semantics of timed games is better behaved w.r.t. admissibility: the existence of admissible strategies is guaranteed in that semantics. Third, we provide symbolic algorithms to solve the model-checking problem under admissibility and the assume-admissible synthesis problem for real-time non-zero sum n-player games for safety objectives.

This paper presents an abstraction-refinement framework for Segala’s probabilistic automata (PA), a slight variant of Markov decision processes. We use Condon and Ladner’s two-player probabilistic game automata extended with possible and required transitions—as in Larsen and Thomsen’s modal transition systems—as abstract models. The key idea is to refine player-one and player-two states separately resulting in a nested abstract-refine loop. We show the adequacy of this approach for obtaining tight bounds on extremal reachability probabilities.

In 1966 Arto Salomaa gave a complete axiomatisation of regular expressions. It can be viewed as a sound and complete proof system for regular processes with respect to the behavioural equivalence called language equivalence. This proof system consists of a finite set of axioms together with one inductive proof rule.We show that the behavioural preorder called language containment or trace inclusion can be characterised in a similar manner, but using a coinductive rather than an inductive proof rule.

In chemical reaction networks (CRNs) with stochastic semantics based on continuous-time Markov chains (CTMCs), the typically large populations of species cause combinatorially large state spaces. This makes the analysis very difficult in practice and represents the major bottleneck for the applicability of minimization techniques based, for instance, on lumpability. In this paper we present syntactic Markovian bisimulation (SMB), a notion of bisimulation developed in the Larsen-Skou style of probabilistic bisimulation, defined over the structure of a CRN rather than over its underlying CTMC. SMB identifies a lumpable partition of the CTMC state space a priori, in the sense that it is an equivalence relation over species implying that two CTMC states are lumpable when they are invariant with respect to the total population of species within the same equivalence class. We develop an efficient partition-refinement algorithm which computes the largest SMB of a CRN in polynomial time in the number of species and reactions. We also provide an algorithm for obtaining a quotient network from an SMB that induces the lumped CTMC directly, thus avoiding the generation of the state space of the original CRN altogether. In practice, we show that SMB allows significant reductions in a number of models from the literature. Finally, we study SMB with respect to the deterministic semantics of CRNs based on ordinary differential equations (ODEs), where each equation gives the time-course evolution of the concentration of a species. SMB implies forward CRN bisimulation, a recently developed behavioral notion of equivalence for the ODE semantics, in an analogous sense: it yields a smaller ODE system that keeps track of the sums of the solutions for equivalent species.

Wireless technology has been widely used in various wireless network scenarios and applications. To model and analyze wireless systems, a calculus of wireless system called CWS has been introduced. In this paper, we put forward an assertion-based reasoning method for this calculus in order to support the verification of the correctness and some interesting properties of wireless system. To simplify the complexity of verification, we first present the assertion-based verification rules for processes separately. Due to the features of wireless system (e.g., broadcast, synchrony, interference), cooperation rules are introduced to combine the processes into a complete system. Finally, there is a case study about using our method to analyze and prove the correctness of Stop-and-Wait ARQ Protocol as well as some properties.

One of the goals of synthetic biology is to build genetic circuits to control the behavior of a cell for different application domains, such as medical, environmental, and biotech. During the design process of genetic circuits, biologists are often interested in the probability of a system to work under different conditions. Since genetic circuits are noisy and stochastic in nature, the verification process becomes very complicated. The state space of stochastic genetic circuit models is usually too large to be handled by classical model checking techniques. Therefore, the verification of genetic circuit models is usually performed by the statistical approach of model checking. In this work, we present a workflow for checking genetic circuit models using a stochastic model checker (Uppaal) and a stochastic simulator (D-VASim). We demonstrate with experimentations that the proposed workflow is not only sufficient for the model checking of genetic circuits, but can also be used to design the genetic circuits with desired timings.

Partial order reduction has traditionally been based on persistent sets, ample sets, stubborn sets, or variants thereof. Recently, we have presented a strengthening of this foundation, using source sets instead of persistent/ample/stubborn sets. Source sets subsume persistent sets and are often smaller than persistent sets. We introduced source sets as a basis for Dynamic Partial Order Reduction (DPOR), in a framework which assumes that processes are deterministic and that all program executions are finite. In this paper, show how to use source sets for partial order reduction in a framework which does not impose these restrictions. We also compare source sets with persistent sets, providing some insights into conditions under which source sets and persistent sets do or do not differ.

There exists a large variety of schedulability analysis tools based on different, often incomparable timing models. This variety makes it difficult to choose the best fit for analyzing a given real-time system. To help the research community to better evaluate analysis tools and their underlying methods, we are developing a framework which consists of (1) a simple language called RTSpec for specifying real-time systems, (2) a tool chain which translates a system specification in RTSpec into an input for various analysis tools, and (3) a set of benchmarks. Our goal is to enable users and developers of schedulability analysis tools to compare such tools systematically, automatically and rigorously.

We address the problem of computing the worst-case execution-time (WCET) of binary programs using a real-time model-checker. In our previous work, we introduced a fully automated and modular methodology to build a model (network of timed automata) that combined a binary program and the hardware to run the program on. Computing the WCET amounts to finding the longest path time-wise in this model, which can be done using a real-time model checker like Uppaal.In this work, we generalise the previous approach and we define a generic framework to support arbitrary binary language and hardware.We have implemented our new approach in an extended version of Uppaal, called Wuppaal. Experimental results using some standard benchmarks suite for WCET computation (from Mälardalen University) show that our technique is practical and promising.

We propose the formal study of blockchains that are owned and controlled by organizations and that neither create cryptocurrencies nor provide incentives to solvers of cryptographic puzzles. We view such approaches as frameworks in which system parts, such as the cryptographic puzzle, may be instantiated with different technology. Owners of such a blockchain procure puzzle solvers as resources they control, and use a mathematical model to compute optimal parameters for the cryptographic puzzle mechanism or other parts of the blockchain. We illustrate this approach with a use case in which blockchains record hashes of financial process transactions to increase their trustworthiness and that of their audits. For Proof of Work as cryptographic puzzle, we develop a detailed mathematical model to derive MINLP optimization problems for computing optimal Proof of Work configuration parameters that trade off potentially conflicting aspects such as availability, resiliency, security, and cost in this governed setting. We demonstrate the utility of such a mining calculus by applying it on some instances of this problem. We hope that our work may facilitate the creation of domain-specific blockchains for a wide range of applications such as trustworthy information in Internet of Things systems and bespoke improvements of legacy financial services.

To balance the fluctuations of renewable energies, greater flexibility on the consumption side is required. Moreover, solutions are required to handle the uncertainty related to both production and consumption. In this paper, we propose a probabilistic extension to FlexOffers to capture both the interval in which a given energy resource can be operated and the uncertainty that surrounds it. Probabilistic FlexOffers serve as a support for a method to forecast energy production and consumption of stochastic hybrid systems. We then show how to generate a consumption strategy to match a given consumption assignment within a given flexibility interval. The method is illustrated on a building equipped with solar cells, a heat pump and an ice bank used to feed the air conditioning system.

We consider a Cyber-Physical System (CPS) as a network of components that are either physical plants with continuous behaviors or discrete controllers. To build CPS’s in a systematic manner, the TIMES-Pro tool is designed to support modeling, analysis and code generation for real-time simulation and final deployment. In this paper, we present our decisions in designing the modeling language, the tool architecture and features of TIMES-Pro, and also a case study to demonstrate its applicability.

In previous work, we used an extended version of timed automata to build safe controllers for autonomous car manoeuvres like changing lanes or crossing an intersection. These automata use formulae of Multi-lane Spatial Logic as guards and invariants and have special controller actions for car manoeuvres. As a case study, we now adapt our approach to formalise a multi-hop communication protocol for hazard warning for highway traffic scenarios. We prove that, if a car detects a hazard, this information timely reaches all cars for which it is relevant via a communication chain so that they can avoid colliding with the hazard.