Search

In order to improve pedestrian safety, it is important to identify suitable routes for walking. This paper presents a real-time reactive system that aims to provide the safest route among all possible routes at a given time, based on intuitionistic fuzzy pedestrian risk modeling. It derives multi criteria decision making to support complex environments using membership and non-membership attributes to generate the intuitionistic fuzzy risk weighting graph based on risk measures. The proposed system involves the pgRouting open-source library that extends the PostGIS/PostgreSQL geospatial database, to provide geospatial routing capabilities. Therefore, we offer a web-location based service allowing pedestrians to enter their destination; then select a route using an intelligent algorithm; providing them with the safest route possible instead of the fastest route. This service will certainly help save lives and reduce pedestrian accidents to some extent.

AALpy is an extensible open-source Python library providing efficient implementations of active automata learning algorithms for deterministic, non-deterministic, and stochastic systems. We put a special focus on the conformance testing aspect in active automata learning, as well as on an intuitive and seamlessly integrated interface for learning automata characterizing real-world reactive systems. In this manuscript, we present AALpy’s core functionalities, illustrate its usage via examples, and evaluate its learning performance.

Runtime verification allows validation of systems during their operation by monitoring crucial system properties. It is common to generate monitors from temporal specifications formulated in languages like MTL or LTL. However, writing formal specifications might be an obstacle for practitioners. In this paper we present an approach and a tool for generating software monitors for reactive systems from a set of Generalized Test Tables (GTTs)—a table-based, user-friendly specification language specially designed for engineers. The tool is a valuable addition to the already existing static verifier for GTTs since assumptions made in specifications can thus be validated at runtime. Moreover, it makes software and specifications amenable for formal validation that cannot be verified statically. Moreover, the approach is particularly well-suited for the specification of workflows as a collection of tables since it supports dynamic, trigger-based spawning of monitors. The tool produces monitor code in C++ for tables provided in an existing table definition format. We show the usefulness of our approach using characteristic examples.

In this paper, a data bus-based software architecture is designed to provide standardized, transparent software interfaces, to reduce coupling between software modules, and shield the complexity of operating system for synchronous reactive system software design. First of all, based on synchronous theory, a data bus-based software architecture is designed. And then, common data space is designated, it is open to all application layer software module, each application layer software module can directly access the common data space. At the same time, a data protection mechanism has been established to ensure that every data has single source and all data are updated uniformly. Finally, the software architecture is applied in wind turbine control software, and the wind turbine control software architecture is reconstructed.

A major breakthrough for multiscale reactive simulations is the ReaxFF reactive force field [#471] developed by van Duin and me in 2001. ReaxFF has enabled the simulations of wide-ranging reactive systems, including shock impact on an energetic materials polymer composites (model for a plastic bonded explosive, PBX) with 3.7 million atoms for 60 ns (see [#951]), the simulation of the effect of hydration on the strength of concrete [#978], elucidation of the mechanism of complex ammoxidation catalysts [#934], and the product distributions from hypervelocity impact with molecular clusters [1004]. Recently, we have developed a new generation, RexPoN that may provide even higher accuracy.

Timed games are an essential formalism for modeling time-sensitive reactive systems that must respond to uncontrollable events triggered by the (hostile) environment. However, the control synthesis problem for these systems is often resource-demanding due to the state space explosion problem. To counter this problem, we present an extension of partial order reduction, based on stubborn sets, into timed games. We introduce the theoretical foundations on the general formalism of timed game labeled transition systems and then instantiate it to the model of timed-arc Petri net games. We provide an efficient implementation of our method as part of the model checker TAPAAL and discuss an experimental evaluation on several case studies that show increasing (sometimes even exponential) savings in time and memory as the case studies scale to larger instances. To the best of our knowledge, this is the first application of partial order reductions to a game formalism that includes time .

Software systems are complicated, and the scientific and engineering methodologies for software development are relatively young. We need robust methods for handling the ever-increasing complexity of software systems that are now in every corner of our lives. In this paper we focus on asynchronous event-based reactive systems and show how we start from the requirements, move to actor-based Rebeca models, and formally verify the models for correctness. The Rebeca models include the details of the signals and messages that are passed at the network level including the timing, and can be mapped to the executable code. We show how we can use the architecture design and structured requirements to build the behavioral models, including Rebeca models, and use the state diagrams to write the properties of interest, and then use model checking to check the properties. The formally verified models can then be used to develop the executable code. The natural mappings among the models for requirements, the formal models, and the executable code improve the effectiveness and efficiency of the approach. It also helps in runtime monitoring and adaptation.

We introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, guarantees, or other behavioral constraints in synchronous reactive system models. This new version of Kind 2 can identify minimal sets of design elements, known as Minimal Inductive Validity Cores, which are sufficient to prove a given set of safety properties, and also determine the set of MUST elements, design elements that are necessary to prove the given properties. In addition, Kind 2 is able to find minimal sets of design constraints, known as Minimal Cut Sets, whose violation leads the system to an unsafe state. We illustrate with an example how to use the computed information for tracking the safety impact of model changes, and for analyzing the tolerance and resilience of a system against faults.

In this paper, we show how to automatically generate hard verification tasks in order to support events like the Model Checking Contest or the Rigorous Examination of Reactive Systems Challenge with tailored benchmark problems for analyzing the validity of linear-time properties in parallel systems. Characteristic of the generated benchmarks are two hardness guarantees: (i) every parallel component is relevant and (ii) the state space of the analyzed system is exponential in the number of its parallel components. Generated benchmarks can be made available, e.g., as Promela code or Petri nets.

We present Tempest, a synthesis tool to automatically create correct-by-construction reactive systems and shields from qualitative or quantitative specifications in probabilistic environments. A shield is a special type of reactive system used for run-time enforcement; i.e., a shield enforces a given qualitative or quantitative specification of a running system while interfering with its operation as little as possible. Shields that enforce a qualitative or quantitative specification are called safety-shields or optimal-shields, respectively. Safety-shields can be implemented as pre-shields or as post-shields, optimal-shields are implemented as post-shields. Pre-shields are placed before the system and restrict the choices of the system. Post-shields are implemented after the system and are able to overwrite the system’s output. Tempest is based on the probabilistic model checker Storm, adding model checking algorithms for stochastic games with safety and mean-payoff objectives. To the best of our knowledge, Tempest is the only synthesis tool able to solve 2 Open image in new window -player games with mean-payoff objectives without restrictions on the state space. Furthermore, Tempest adds the functionality to synthesize safe and optimal strategies that implement reactive systems and shields.

Reinforcement learning algorithms discover policies that maximize reward. However, these policies generally do not adhere to safety, leaving safety in reinforcement learning (and in artificial intelligence in general) an open research problem. Shield synthesis is a formal approach to synthesize a correct-by-construction reactive system called a shield that enforces safety properties of a running system while interfering with its operation as little as possible. A shield attached to a learning agent guarantees safety during learning and execution phases. In this paper we summarize three types of shields that are synthesized from different specification languages, and discuss their applicability to reinforcement learning. First, we discuss deterministic shields that enforce specifications expressed as linear temporal logic specifications. Second, we discuss the synthesis of probabilistic shields from specifications in probabilistic temporal logic. Third, we discuss how to synthesize timed shields from timed automata specifications. This paper summarizes the application areas, advantages, disadvantages and synthesis approaches for the three types of shields and gives an overview of experimental results.

Reactive software is often deployed in long-running systems with high dependability requirements. Despite their safety- and mission-critical use, their functionalities must occasionally be adapted, for example to support new features or regulations. But software evolution bears the risk of introducing new malfunctions. Regression verification helps preventing the introduction of unintended, faulty behaviour.

This paper describes a component-based concurrent model of computation for reactive systems. The components in this model, featuring ports and hierarchy, are called reactors. The model leverages a semantic notion of time, an event scheduler, and a synchronous-reactive style of communication to achieve determinism. Reactors enable a programming model that ensures determinism, unless explicitly abandoned by the programmer. We show how the coordination of reactors can safely and transparently exploit parallelism, both in shared-memory and distributed systems.

We present a new approach to conformance testing of black-box reactive systems. We consider system specifications written as linear temporal logic formulas to generate tests as sequences of input/output pairs: inputs are extracted from the Buchi automata corresponding to the specifications, and outputs are obtained by feeding the inputs to the systems. Conformance is checked by comparing input/output sequences with automata traces to detect violations of the specifications. We consider several criteria for extracting tests and for stopping generation, and we compare them experimentally using both indicators of coverage and error-detection. The results show that our methodology can generate test suites with good system coverage and error-detection capability.

Variable automata with arithmetic enable the specification of reactive systems with variables over an infinite domain of numeric values and whose operation involves arithmetic manipulation of these values [9]. We study the synthesis problem for such specifications. While the problem is in general undecidable, we define a fragment, namely semantically deterministic variable automata with arithmetic, for which the problem is decidable. Essentially, an automaton is semantically deterministic if the restrictions on the possible assignments to the variables that are accumulated along its runs resolve its nondeterministic choices. We show that semantically deterministic automata can specify many interesting behaviors – many more than deterministic ones, and that the synthesis problem for them can be reduced to a solution of a two-player game. For automata with simple guards, the game has a finite state space, and the synthesis problem can be solved in time polynomial in the automaton and exponential in the number of its variables.

Many reactive processes with the purpose of modifying the structure of fiber polymers are applied in textile chemistry in order to change their properties. These processes depend on the chemical nature of the polymer and the type of modification, and these aspects are discussed with respect to alkalization, chemical crosslinking with bi- and multifunctional reagents, hydrolytic processes, deposition and grafting of polymers, as well as crosslinking with urea-based reactive systems (e.g. dry cure processes). The selection of process parameters are of decisive importance for the efficient development of a desired portfolio of properties in a certain fiber-based product. This chapter aims to analyze the recent advances in reactive modification of fiber polymer materials.

The container virtualization on the Kubernetes platform brings challenges that need to be addressed when a production or test load is running across the cluster. If applications running in containers are spread across the Kubernetes cluster, resource usage may be inefficient across the environment, which may result in overloading of individual nodes and inefficient load on others. One area where inefficiencies may occur is the load on network lines and network communications. This article discusses two algorithms and approaches that can be applied to the Kubernetes platform while helping to manage network traffic and lines across the cluster, which can make the cluster components more efficient. Both algorithms collect the monitored data from the cluster, but each one the data collected behaves differently, and data transformation and analysis takes place in another part of the system. The first algorithm is an agent-based algorithm that collects and performs basic data analysis and is capable of responding to detected information. The second is the algorithm that collects the data into the central element of the system and then analyzes it and, based on the information obtained, controls the individual components of the cluster.

Clinical pathways are multidisciplinary structured care plans that aim at increasing the quality of healthcare delivery. Despite the wide-spread adoption of clinical pathways by governments and healthcare authorities, works that associate formal semantics to clinical pathways do not model clearly the roles of health professionals during the care process. This has motivated us to propose a formal modelling approach for clinical pathways, based on Bigraphical Reactive Systems. We concentrate on showing graphically relationships among the healthcare stakeholders. To meet the control flow requirement of clinical pathways, we apply the Maude strategies language over a Maude implementation of Bigraphical reactive Systems key concepts.

Stochastic multiplayer games (SMGs) have gained attention in the field of strategy synthesis for multi-agent reactive systems. However, standard SMGs are limited to modeling systems where all agents have full knowledge of the state of the game. In this paper, we introduce delayed-action games (DAGs) formalism that simulates hidden-information games (HIGs) as SMGs, where hidden information is captured by delaying a player’s actions. The elimination of private variables enables the usage of SMG off-the-shelf model checkers to implement HIGs. Furthermore, we demonstrate how a DAG can be decomposed into subgames that can be independently explored, utilizing parallel computation to reduce the model checking time, while alleviating the state space explosion problem that SMGs are notorious for. In addition, we propose a DAG-based framework for strategy synthesis and analysis. Finally, we demonstrate applicability of the DAG-based synthesis framework on a case study of a human-on-the-loop unmanned-aerial vehicle system under stealthy attacks, where the proposed framework is used to formally model, analyze and synthesize security-aware strategies for the system.

We develop a compositional, algebraic theory of skipping refinement, as well as local proof methods to effectively analyze the correctness of optimized reactive systems. A verification methodology based on refinement involves showing that any infinite behavior of an optimized low-level implementation is a behavior of the high-level abstract specification. Skipping refinement is a recently introduced notion to reason about the correctness of optimized implementations that run faster than their specifications, i.e., a step in the implementation can skip multiple steps of the specification. For the class of systems that exhibit bounded skipping, existing proof methods have been shown to be amenable to mechanized verification using theorem provers and model-checkers. However, reasoning about the correctness of reactive systems that exhibit unbounded skipping using these proof methods requires reachability analysis, significantly increasing the verification effort. In this paper, we develop two new sound and complete proof methods for skipping refinement. Even in presence of unbounded skipping, these proof methods require only local reasoning and, therefore, are amenable to mechanized verification. We also show that skipping refinement is compositional, so it can be used in a stepwise refinement methodology. Finally, we illustrate the utility of the theory of skipping refinement by proving the correctness of an optimized event processing system.

Graph games and Markov decision processes (MDPs) are standard models in reactive synthesis and verification of probabilistic systems with nondeterminism. The class of \(\omega \)-regular winning conditions; e.g., safety, reachability, liveness, parity conditions; provides a robust and expressive specification formalism for properties that arise in analysis of reactive systems. The resolutions of nondeterminism in games and MDPs are represented as strategies, and we consider succinct representation of such strategies. The decision-tree data structure from machine learning retains the flavor of decisions of strategies and allows entropy-based minimization to obtain succinct trees. However, in contrast to traditional machine-learning problems where small errors are allowed, for winning strategies in graph games and MDPs no error is allowed, and the decision tree must represent the entire strategy. In this work we propose decision trees with linear classifiers for representation of strategies in graph games and MDPs. We have implemented strategy representation using this data structure and we present experimental results for problems on graph games and MDPs, which show that this new data structure presents a much more efficient strategy representation as compared to standard decision trees.

Reactive systems are composed of a well defined set of event handlers by which the system responds to environment stimulus. In concurrent environments, event handlers can interact with the execution of other handlers such as hardware interruptions in preemptive systems, or other instances of the reactive system in multicore architectures. The rely-guarantee technique is a suitable approach for the specification and verification of reactive systems. However, the languages in existing rely-guarantee implementations are designed only for “pure programs”, simulating reactive systems makes the program and rely-guarantee conditions unnecessary complicated. In this paper, we decouple the system reactions and programs using a rely-guarantee interface, and develop PiCore, a parametric rely-guarantee framework for concurrent reactive systems. PiCore has a two-level inference system to reason on events and programs associated to events. The rely-guarantee interface between the two levels allows the reusability of existing languages and their rely-guarantee proof systems for programs. In this work we show how to integrate in PiCore two existing rely-guarantee proof systems. This work has been fully mechanized in Isabelle/HOL. As a case study, we have applied PiCore to the concurrent buddy memory allocation of a real-world OS, providing a verified low-level specification and revealing bugs in the C code.

BIFROST is a persistent, shared design tool and simulation environment for Smart Cities, with a strong focus on powergrid infrastructure. Backed by a reactive server backend and powerful simulation engine, a browser-based, 2.5D user interface empowers researchers, network operators and planning experts to construct and analyze situations revolving around powergrid operations. The internal engine state representing the simulation world, including all physical dynamics and structures, is fully exposed to external applications, such as control algorithms or time series analysis tools. Thus, BIFROST can be employed as a virtual testbed for Smart Energy System installations, allowing for the evaluation of scenarios which would be hard or impossible to stage in-field.

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. GR(1) is an expressive assume-guarantee fragment of LTL that enables efficient synthesis and has been recently used in different contexts and application domains. A common form of providing the system’s requirements is through use cases, which are existential in nature. However, GR(1), as a fragment of LTL, is limited to universal properties.

Software systems undergo several changes along their life-cycle and hence, their models may become outdated. To tackle this issue, we propose an efficient algorithm for adaptive learning, called \(\mathtt {partial\text {-}Dynamic~L^*_M}\) (\(\mathtt {\partial L^*_M}\)) that improves upon the state of the art by exploring observation tables on-the-fly to discard redundant prefixes and deprecated suffixes. Using 18 versions of the OpenSSL toolkit, we compare our proposed algorithm along with three adaptive algorithms. For the existing algorithms in the literature, our experiments indicate a strong positive correlation between number of membership queries and temporal distance between versions and; for our algorithm, we found a weak positive correlation between membership queries and temporal distance, as well, a significantly lower number of membership queries. These findings indicate that, compared to the state-of-the-art algorithms, our \(\mathtt {\partial L^*_M}\) algorithm is less sensitive to software evolution and more efficient than the current approaches for adaptive learning.

Markov Decision Processes (MDPs) are a popular class of models suitable for solving control decision problems in probabilistic reactive systems. We consider parametric MDPs (pMDPs) that include parameters in some of the transition probabilities to account for stochastic uncertainties of the environment such as noise or input disturbances.

Graph-based games are an important tool in computer science. They have applications in synthesis, verification, refinement, and far beyond. We review graph-based games with objectives on infinite plays. We give definitions and algorithms to solve the games and to give a winning strategy. The objectives we consider are mostly Boolean, but we also look at quantitative graph-based games and their objectives. Synthesis aims to turn temporal logic specifications into correct reactive systems. We explain the reduction of synthesis to graph-based games (or equivalently tree automata) using synthesis of LTL specifications as an example. We treat the classical approach that uses determinization of parity automata and more modern approaches.

We study the reactive synthesis problem for hyperproperties given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to sets of sets of traces. Typical examples are information-flow policies like noninterference, which stipulate that no sensitive data must leak into the public domain. Such properties cannot be expressed in standard linear or branching-time temporal logics like LTL, CTL, or CTL\(^*\). We show that, while the synthesis problem is undecidable for full HyperLTL, it remains decidable for the \(\exists ^*\), \(\exists ^*\forall ^1\), and the \( linear \;\forall ^*\) fragments. Beyond these fragments, the synthesis problem immediately becomes undecidable. For universal HyperLTL, we present a semi-decision procedure that constructs implementations and counterexamples up to a given bound. We report encouraging experimental results obtained with a prototype implementation on example specifications with hyperproperties like symmetric responses, secrecy, and information-flow.

This paper is dedicated to the Rigorous Examination of Reactive Systems (RERS) Challenge 2018. We focus on changes and improvements compared to previous years. RERS again provided a large variety of verification benchmarks that foster the comparison of validation tools while featuring both sequential and parallel programs. In addition to reachability questions, the RERS Challenge is known for its linear temporal logic (LTL) properties, and RERS’18 extends the portfolio of verification tasks to computational tree logic (CTL). Modifications compared to the previous iteration include an enhanced generation of sequential benchmarks, an improved automation of the construction of parallel benchmarks, a redesigned penalty for wrong answers, and the addition of CTL properties. We illustrate our newly applied generation of parallel benchmarks in detail.

The reset of reactive systems in testing can be impossible or very costly, which could force testers to avoid it. In this context, testers often want to generate a checking sequence, i.e., a unique sequence of inputs satisfying a chosen test criterion. This paper proposes a method for generating a checking sequence with complete fault coverage for a given fault model of reactive systems. The systems are represented with an extension of Finite State Machines (FSMs) with symbolic inputs and outputs which are predicates on input and output variables having possibly infinite domains. In our setting, a checking sequence is made up of symbolic inputs and the fault domain can represent complex faults. The method consists in building and solving Boolean expressions to iteratively refine and extend a sequence of symbolic inputs. We evaluate the efficiency of the approach with a prototype tool we have developed.

In the late 1970s, Amir Pnueli suggested that functional properties of reactive systems be formally expressed in temporal logic. For model checking such a logic to be possible, it must have sufficient expressive power, its semantics must be formally defined in a rigorous way, and the complexity of model checking it must be well understood and reasonable. In order to allow widespread adoption in industry, there is an additional requirement: functional specification must be made easy, allowing common properties to be expressed intuitively and succinctly. But while adding syntax is simple, defining semantics without breaking properties of the existing semantics is a different story. This chapter is about the various extensions to temporal logic included in the IEEE standards PSL and SVA, their motivation, and the subtle semantic issues encountered in their definition.

Responsiveness—the requirement that every request to a system be eventually handled—is one of the fundamental liveness properties of a reactive system. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. We show how average response time can be computed on state-transition graphs, on Markov chains, and on game graphs. In all three cases, we give polynomial-time algorithms.

Graph games played by two players over finite-state graphs are central in many problems in computer science. In particular, graph games with \(\omega \)-regular winning conditions, specified as parity objectives, which can express properties such as safety, liveness, fairness, are the basic framework for verification and synthesis of reactive systems. The decisions for a player at various states of the graph game are represented as strategies. While the algorithmic problem for solving graph games with parity objectives has been widely studied, the most prominent data-structure for strategy representation in graph games has been binary decision diagrams (BDDs). However, due to the bit-level representation, BDDs do not retain the inherent flavor of the decisions of strategies, and are notoriously hard to minimize to obtain succinct representation. In this work we propose decision trees for strategy representation in graph games. Decision trees retain the flavor of decisions of strategies and allow entropy-based minimization to obtain succinct trees. However, decision trees work in settings (e.g., probabilistic models) where errors are allowed, and overfitting of data is typically avoided. In contrast, for strategies in graph games no error is allowed, and the decision tree must represent the entire strategy. We develop new techniques to extend decision trees to overcome the above obstacles, while retaining the entropy-based techniques to obtain succinct trees. We have implemented our techniques to extend the existing decision tree solvers. We present experimental results for problems in reactive synthesis to show that decision trees provide a much more efficient data-structure for strategy representation as compared to BDDs.

In scenario-based models of reactive systems complex specifications are divided into artifacts corresponding to separate aspects of overall system behavior, as they may appear, e.g., in a robot’s requirements document or user specifications. The advantages of scenario-based development include intuitiveness and clarity, the ability to execute or simulate specifications of early prototypes and of final systems, and the ability to verify the specification for early detection of conflicts, omissions, and errors. In this position paper we discuss two issues that emerge when applying scenario-based development in complex cases: (a) simple scenarios become unwieldy when subjected to a growing number of conditions, exceptions and refinements, and (b) it is hard to understand and maintain a large ‘flat’ specification, consisting of an unorganized list of independently-specified scenarios, simple as they may individually be. We address these issues by basing certain facets of scenario design on context, an increasingly popular foundational consideration in software engineering. We first show how one can incorporate context into the graphical language of live sequence charts (LSC) using existing LSC idioms. We then outline two other possibilities: (i) enriching the LSC language, or (ii) embedding LSCs within hierarchical state machines, namely, statecharts. We believe that this research can contribute to the broader goals of developing complex and powerful reactive systems in intuitive and robust ways.

Model checking and simulation are powerful techniques for developing and verifying the design of reactive systems. Here we propose the use of a complementary technique – automated theory formation. In particular, we report on an experiment in which we used a general purpose automated theory formation tool, HR, to explore properties of a model written in Promela. Our use of HR is constrained by meta-knowledge about the model that is relevant to hazard analysis. Moreover, we argue that such meta-knowledge will enable us to explore how safety properties could be violated.

International audience; Clouds are complex systems that provide computing resources in an elastic way. Elasticity property allows their adaptation to input workload by (de)provisioning resources as the demand rises and drops. However, due to the numerous overlapping factors that impact their elasticity and the unpredictable nature of the workload, providing accurate action plans to manage cloud systems’ elastic adaptations is a particularly challenging task. In this paper, we propose an approach based on Bigraphical Reactive Systems (BRS) to model cloud structures and their elastic behavior. We design elasticity strategies that operate at service and infrastructure cloud levels to manage the elastic adaptations. Besides, we provide a Maude encoding to permit generic executability and formal verification of the elastic behaviors. One step ahead, we show how the strategies can be combined at both levels to provide different high-level elastic behaviors. Finally, we evaluate the different cross-layer combinations using Queuing Theory.

When creating system models, further to system behaviour one should take into account properties of the environment in order to achieve more meaningful models. Here, we extend a strategy that formalises data-flow reactive systems as CSP processes to take into account environment restrictions. Initially, these restrictions are written in natural language. Afterwards, with the aid of case-grammar theory, they are formalised by deriving LTL formulae automatically. Finally, these formulae are used to prune infeasible scenarios from the CSP-based system specification, in the light of the environment restrictions. Considering examples from the literature, and from the aerospace (Embraer) and the automotive (Mercedes) industry, we show the efficacy of our proposal in terms of state space reduction, up to 61% in some cases.

We propose an alternative approach to the classical way of specifying algorithms, inspired by the scenario-based paradigm for reactive systems. Rather than being presented as a carefully ordered sequence of instructions, an algorithm is formalized as an unordered collection of rules or scenarios, specifying actions that must or must not be taken when certain conditions hold or after certain sequences of events. A successful implementation of such a methodology, which can be aligned with a natural language specification, can have many advantages, including naturalness, comprehensibility and incrementality. We believe that our approach can also accelerate the acquisition of problem-solving and analytical skills by children and students. This is because by writing (and reading) computer programs written in this way, people would have access to a broad base of instructions on how to solve problems, stated and organized in a way that can be readily understood and used in practice also by humans. We describe the principles of the approach, scenario-based algorithmics (SBA), provide some examples, and compare it to other techniques for algorithm specification and to human algorithmic or computational thinking.

Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of reactive systems from propositional specifications towards specifications over rich theories. We propose a novel, completely automated approach to program synthesis which reduces the problem to deciding the validity of a set of \(\forall \exists \)-formulas. In spirit of IC3/PDR, our problem space is recursively refined by blocking out regions of unsafe states, aiming to discover a fixpoint that describes safe reactions. If such a fixpoint is found, we construct a witness that is directly translated into an implementation. We implemented the algorithm on top of the JKind model checker, and exercised it against contracts written using the Lustre specification language. Experimental results show how the new algorithm outperforms JKind’s already existing synthesis procedure based on k-induction and addresses soundness issues in the k-inductive approach with respect to unrealizable results.

International audience; Elastic behaviors enable Cloud Systems to auto-adapt to their incoming workloads, by provisioning and releasing computing resources, in a way to ensure a controlled compromise between performance and cost-saving requirements. However, due to the highly fluctuating workloads tendencies, it makes it difficult to predict how a cloud system would behave and to provide precise auto-adaptation action plans. In this paper, we propose a BRS (short for Bigraphical Reactive Systems) based approach to provide a formal description for cloud systems structures and their elastic behaviors using bigraphs and bigraphical reaction rules. In addition, elasticity strategies are introduced to encode cloud systems’ auto-adaptation policies. Proposed approach is illustrated and evaluated through an example.

This chapter focuses on the problem of determining the reactive dynamics of the simplest prototypes of elementary chemical reactions starting from a general non-Born–Oppenheimer (mixed electron–nuclei) approach first and then formulating the problem using a separating from that of the nuclei. To this end, the problem of adopting coordinate sets suited for describing both the interaction and the dynamics of the simplest reactive systems is discussed. Typical features of the atomistic phenomenology of atom–diatom systems such as the effect of a different allocation of energy to the various degrees of freedom in promoting reactivity, the importance of providing an accurate representation of the potential energy, the merits and demerits of reduced dimensionality calculations, and the importance of periodic orbits are analyzed.

Synchronous languages have been introduced as programming languages that directly reflect the nature of reactive systems: Their execution is divided into discrete reaction steps such that in each reaction step, inputs are read from the environment and outputs are instantaneously computed. Reaction steps, which are also called macro steps, consist thereby of a set of atomic micro step actions that are executed in the variable environment associated with the macro step. At the beginning of the macro step, only the values of the input variables are known in this variable environment, and the values of the remaining variables have to be computed according to the data-dependencies. Since the micro step actions depend on the variable environment that they also create, it might be the case that there are cyclic dependencies. Whether such cyclic dependencies can be constructively resolved has to be checked by a compile-time causality analysis which will ensure that there is for all inputs a suitable schedule of the micro steps. If the synchronous programs are converted to guarded actions as done in the author’s Averest system, some relationships with logic programs can be found: In particular, the concepts of reaction-to-absence of synchronous languages and negation-to-failure of logic programs seem to be the same; another analogy is found for the generation of equation-based code of synchronous programs and the completion of logic programs, and also for the fix-point analyses defined in both paradigms. This paper outlines these analogies between the two paradigms of programming languages and discusses whether further known semantics of logic programs like well-founded and stable models may find useful counterparts in the synchronous world in future.

Software engineers frequently employ notations and tools based on transition systems, such as UML state machines and Statecharts, for specifying and reasoning about reactive behaviour. While these notations are typically supported by an operational semantics, they lack a formal underpinning of the incremental refinement practices of engineers who, e.g., place state machines inside states or add outer transitions to states during design. This note sketches how modal transition systems may be applied to formally capture such refinements along state hierarchies, using a hierarchical extension of labelled transition systems that permits engineers to explicitly allow or disallow state refinement and transition extension at each state. A small example testifies to the utility of this framework for hierarchically refining reactive systems.

In industrial practice today, correctness of software is rarely verified using formal techniques. One reason is the lack of specification languages for this application area that are both comprehensible and sufficiently expressive. We present the concepts and logical foundations of generalised test tables – a specification language for reactive systems accessible for practitioners. Generalised test tables extend the concept of test tables, which are already frequently used in quality management of reactive systems. The main idea is to allow more general table entries, thus enabling a table to capture not just a single test case but a family of similar behavioural cases. The semantics of generalised test tables is based on a two-party game over infinite words.

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.

Behavioral Programming (BP) is a modelling and programming technique proposed for specifying and for implementing complex reactive systems. While effective, we report on a weakness that stems from the verbosity and from the complexity of the programming constructs in BP. Our analysis, described in this paper, shows that developers who work with BP use specific patterns that allow them to control the complexity of their specification. Thus, the main contribution of this paper is a set of specification constructs that represent those patterns. We report on the design of the new idioms, termed structured constructs for behavioral programming and on an empirical evaluation in a controlled experiment that proved their effectiveness. In particular, the experiment examined the comprehensibility differences between behavioral specifications with non-structured BP programming idioms and with the structured ones. The results indicate that the new structures improve the comprehension of the behavioral specification.

Variants of the finite state machine (FSM) model have been extensively used to describe the behaviour of reactive systems. In particular, several model-based testing techniques have been developed to support test case generation and test case executions from FSMs. Most such techniques require several validation properties to hold for the underlying test models. In this paper, we propose an extension of the FSM test model for software product lines (SPLs), named featured finite state machine (FFSM). As the first step towards using FFSMs as test models, we define feature-oriented variants of basic test model validation criteria. We show how the high-level validation properties coincide with the necessary properties on the product FSMs. Moreover, we provide a mechanised tool prototype for checking the feature-oriented properties using satisfiability modulo theory (SMT) solver tools. We investigate the applicability of our approach by applying it to both randomly generated FFSMs as well as those from a realistic case study (the Body Comfort System). The results of our study show that for random FFSMs over 16 independent non-mandatory features, our technique provides substantial efficiency gains for the set of proposed validity checks. © Springer International Publishing AG 2017 VR Project - EFFEMBAC KKS Project - AUTO-CAAS