Search

Multi-agent systems are recognized as a major area of distributed artificial intelligence. In fact, MAS have found multiple applications, including the design and development of complex, hierarchical and critical systems. However, ensuring the accuracy of complex interactions and the correct execution of activities of a MAS is becoming a tedious task. In this work, we focus on the formal specification of interaction, holonic and sociotechnical concepts to the BRS-MAS model. The proposed approach, is based on Bigraphical reactive systems. Bigraphs, provide means to specify at same time locality and connectivity of different type of system ranging from soft systems to cyber physical systems. In addition, to its intuitive graphical representation, it provides algebraic definition. This, makes the resulted specifications more precise. Further, it enables the verification of the specified system at the design time (before the implementation) using verification tools.

Systematic model-driven design and early validation enable engineers to verify that a reactive system does not violate its requirements before actually implementing it. Requirements may come from multiple stakeholders, who are often concerned with different facets - design typically involves different experts having different concerns and views of the system. Engineers start from a specification which may be sourced from some domain model, while validation is often done on state-transition structures that support model checking. Two computationally expensive steps may work against scalability: transformation from specification to state-transition structures, and model checking. We propose a technique that makes the former efficient and also makes the resulting transition systems small enough to be efficiently verified. The technique automatically projects the specification into submodels depending on a property sought to be evaluated, which captures some stakeholder's viewpoint. The resulting reactive system submodel is then transformed into a state-transition structure and verified. The technique achieves cone-of-influence reduction, by slicing at the specification model level. Submodels are analysis-equivalent to the corresponding full model. If stakeholders propose a change to a submodel based on their own view, changes are automatically propagated to the specification model and other views affected. Automated reflection is achieved thanks to bidirectional model transformations, ensuring correctness. We cast our proposal in the context of graph-based reactive systems whose dynamics is described by rewriting rules. We demonstrate our view-based framework in practice on a case study within cyber-physical systems.

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. In this work we present just-in-time synthesis (JITS) for GR(1), a novel means to execute synthesized reactive systems. Rather than constructing a controller at synthesis time, we compute next states during system execution, and only when they are required. We prove that JITS does not compromise the correctness of the synthesized system execution. We further show that the basic algorithm can be extended to enable several variants. We have implemented JITS in the Spectra synthesizer. Our evaluation, comparing JITS to existing tools over known benchmark specifications, shows that JITS reduces (1) total synthesis time, (2) the size of the synthesis output, and (3) the loading time for system execution, all while having little to no effect on system execution performance.

Ubi-Interact is a framework designed to facilitate interactive applications consisting of a variety of individual systems and devices that are distributed over a (local) network. It is designed to allow easy integration of devices and exchange of data based on extendable common data formats. It features edge computing capabilities, allowing to analyze and transform device data. The same computing modules can also be used to manage an arbitrary number of devices in an abstract fashion, allowing ad-hoc handling of (dis-)connecting devices and making devices with similar components/capabilities interchangeable while lowering the necessity to re-implement parts of the overall system behaviour. Specification and implementation of these applications should be modular, extendable and re-usable so users can share and improve on the work of others. Performance, re-usability of once established capabilities and easy integration of devices are the main points of interest for developing this framework.

Ordering and replaying of execution traces of distributed systems is a challenging problem. State-of-the-art approaches annotate the traces with logical or physical timestamps. However, both kinds of timestamps have their drawbacks, including increased trace size. We examine the problem of determining consistent orderings of execution traces in the context of model-driven development of reactive distributed systems, that is, systems whose code has been generated from communicating state machine models. By leveraging key concepts of state machines and existing model analysis and transformation techniques, we propose an approach to collecting and reordering execution traces that does not rely on timestamps. We describe a prototype implementation of our approach and an evaluation. The experimental results show that compared to reordering based on logical timestamps using vector time (clocks), our approach reduces the size of the trace information collected by more than half while incurring similar runtime overhead.

A challenge that has gathered much attention in recent years is automated synthesis of correct-by-construction software systems from declarative specifications. The specification language is typically a subset of linear temporal logic called generalized reactivity of rank 1, for which there exists an efficient synthesis algorithm. Specifications in this language model the system as the interaction between an environment and a controller, the former satisfying a set of assumptions and the latter a set of guarantees. In order for a solution to exist, a sufficient set of assumptions implying the guarantees must be provided. The assumptions must be as general as possible and small enough to be intelligible by engineers that need to assess their consistency with the true environment where the synthesized controller will operate. The search for such assumptions is generally a refinement approach driven by counterstrategies, characterizations of undesirable environment behaviors that force the violation of the guarantees; assumptions are progressively refined in order to exclude such behaviors. In this work we provide a heuristic to drive this counterstrategy-guided search towards smaller refinements. We define a concept of minimality of refinements with respect to counterstrategies and provide an algorithm that provably finds minimal refinements with little time overhead. We show experimentally that it consistently produces one or more shorter solutions than state of the art for a set of popular case studies. We also demonstrate that in a popular case study (AMBA-AHB protocol) our heuristic finds a close-to-optimal solution that cannot be found by previous fully automated approaches.

Reactive IoT applications often have to deal with the data source Babel arising from their need to operate on context information originated from different data sources. Semantic knowledge bases can be fruitfully deployed to alleviate this problem: they provide a unified access point for context information including both long term (such as the structure of the environment) and transient (such as sensor readings) data thanks to their ability to host elements responding to different schemas within the same container. In previous works we introduced an architecture to create reactive IoT systems based on a semantic knowledge base that also hosts the definition of their behavior and on an accompanying reactive machinery. In this paper, we introduce the use of knowledge base overlays, i.e. containers providing a live, unified view over (parts of) different underlying knowledge bases, as a mechanism to enable interoperation between multiple IoT semantics-based systems. Specifically we explore the benefits of this approach in a case study in which a semantic IoT system governing a smart building interacts with the personal semantic systems of the people entering the building.

Realizability problems may emerge when specifications of complex distributed reactive systems are mapped to local distributed designs that may contain undesired behaviours, sometimes termed as implied scenarios. In this paper, we focus on resolving one of these realizability problems named as mixed initiative that occurs when independent and concurrent entities take uncoordinated initiatives autonomously. The mixed initiative problem is unavoidable in the execution of some distributed reactive systems and can normally not be prevented. Mixed initiative resolution guidelines have been proposed in the past that use UML activity diagrams and/or additional transitions in UML state machines. The novelty in our approach lies in the use of UML composite states for resolving the mixed initiative problem. However, UML does not have well-defined guidelines on serialization/unfolding of composite states. This paper, therefore, first proposes guidelines on how to serialize/unfold a UML composite state and then how to use it for addressing mixed initiative realizability problem using a case study named Call Centre.

As reactive systems, such as cyber-physical systems and the Internet of Things, become increasingly important, time-varying values, also known as signals, are playing an important role in software development. Although reactive systems require the change histories of some signals to be stored for various purposes such as post analysis and simulation, current programming languages do not provide a way to declare that signals are persistent. This paper proposes a method that realizes persistent signals in a reactive programming language, where (1) every update to each persistent signal is recorded in a time-series database, which can be seen as a part of the programming language runtime; and (2) persistent signals support a convenient time-oriented query mechanism. In this approach, each signal in the reactive programming language is seamlessly connected with the time-series database. This method is implemented as an extension of SignalJ, a Java-based reactive programming language that supports signals. In the implementation, the persistent signal mechanism is integrated with TimescaleDB, a PostgreSQL-based time-series database. In preliminary performance evaluations, our implementation had good responsiveness on most tests, indicating its feasibility for use in many applications.

Functional Reactive Programming is an approach to declarative programming of reactive systems by describing interactions between time-varying values. FRP implementations are often realised as an embedding in a functional host language, making for very expressive reactive programming frameworks. However, this expressiveness comes at a cost: current embedded FRP implementations incur substantial performance overheads, in particular for values that (notionally) vary continuously. The basic idea of FRP is closely related to synchronous data-flow and continuous system simulation languages. In contrast to FRP, these handle values that vary continuously efficiently, but are less expressive. This paper seeks to bridge this gap by proposing a novel approach to embedded FRP-implementation that uses the fundamental implementation approach of synchronous datalow and simulation languages for efficient handling of continuously varying values, while retaining the expressiveness normally associated with FRP, as well as paying attention to values that only change relatively infrequently. These ideas are applicable beyond FRP, for example for implementing flexible embedded simulation languages. We evaluate our approach on a range of benchmarks, including an existing full-fledged video game where using our new FRP implementation as a drop-in replacement for the old one gave a three-fold performance improvement.

Reactive molecular dynamics (MD) simulations are important for high-fidelity simulations of large systems with chemical reactions. Iterative linear solvers used to dynamically determine atom polarizations in reactive MD models and redundancies related to bond order calculations constitute significant bottlenecks in terms of time-to-solution and the overall scalability of reactive force fields. The objective of this work is to address these bottlenecks. To accomplish this goal, several optimizations are explored including acceleration of the charge model solver through an effective preconditioning technique and a numerical method with reduced communication overheads, as well as initialization and data structure changes for bond order calculations. Detailed scalability analysis of these optimizations and their overall impact is presented. A single-allreduce pipelined non-blocking conjugate gradient (PIPECG) solver coupled with a sparse approximate inverse (SAI) based preconditioner has been observed to yield significant speedups over the baseline standard CG solver with Jacobi preconditioner. These results are significant as they can facilitate scalable simulations of large reactive systems, and presented techniques can be used in other polarizable MD models.

Reactive Systems, especially in the Big Data Era, are undergoing a revolution. The increasing interest is due to their responsiveness, elasticity, resiliency and message-driven trait. In particular, a reactive message-driven system has one core feature asynchronous communication assuring a non-blocking behavior. A particular case of such systems is the use of actors to assure encapsulation and support fast decisions, failure handling and progess. The Actor Model meets the requirements for buiding a highly conccurent, scalable, distributed system, and Akka's tools provide the means to build it. However, to the best of our knowledge the effect of intra-actor asynchronous message processing on the routing strategies and the load balancing issue has not been addressed in the literature yet. The aim of this study is to analyse the behavior of the routers and routees over the existing routing strategies when each routee processes its messages asynchronously. Moreover, we study how the load is balanced among the routees and propose our own routing strategy that can reduce the processing time overhead by considering the complexity of the messages. For that, we build a distributed system to offline process massive trajectories, initially stored in HDFS, with Akka, the Play Framework, and MongoDB. Specifically, we leverage the Geolife projectâArZs GPS trajectory dataset.

Realizability checking is used to detect flaws in reactive system specifications that are difficult for humans to find. However, these checks are computationally costly. To address this problem, researchers have studied efficient methods for implementing such checking procedures. In this paper, we propose a new implementation method of realizability checking. While symbolic approaches have been adopted in many previous methods, we take a partially symbolic approach, in which binary decision diagrams (BDDs) are used partially. We developed a prototype realizability checker based on our method, and experimentally compared it to tools based on other implementation methods. Our prototype was efficient in comparison to the other tools.

International audience; This paper describes our experience in constructing a new Domain-Specific Language course at the graduate level whose objectives is to reconciliate concepts coming from Language Design as well as Modeling domains. We illustrate the course using the reactive systems application domain, which prevents us to fall back in a toy example pitfall. This paper describes the nine stages used to guide students through a journey starting at low-level C code to end with the usage of a language design workbench. This course was given as a graduate course available at Université Côte d'Azur (8 weeks, engineering-oriented) and École Normale Supérieure de Lyon (13 weeks, research-oriented).

While the object-orientation is the most used paradigm for developing general purpose software systems, the use of reactive systems has been growing lately. One of the differences between them is that while the first offers an imperative style, the latter focuses on a functional style. In this paper, we present the semantics for AsyncRFJ, an object-oriented language based on Featherweight Java, created to reason and to develop programs handling reactive data flow in the context of object-oriented programming. Additionally, we provide an interpreter for the proposed semantics and a set of examples designed to illustrate the language.

The task of a monitor is to watch, at run-time, the execution of a reactive system, and signal the occurrence of a safety violation in the observed sequence of events. While finite-state monitors have been studied extensively, in practice, monitoring software also makes use of unbounded memory. We define a model of automata equipped with integer-valued registers which can execute only a bounded number of instructions between consecutive events, and thus can form the theoretical basis for the study of infinite-state monitors. We classify these register monitors according to the number k of available registers, and the type of register instructions. In stark contrast to the theory of computability for register machines, we prove that for every k ≥ 1, monitors with k + 1 counters (with instruction set 〈+1, =〉) are strictly more expressive than monitors with k counters. We also show that adder monitors (with instruction set 〈1, +, =〉) are strictly more expressive than counter monitors, but are complete for monitoring all computable safety ω-languages for k = 6. Real-time monitors are further required to signal the occurrence of a safety violation as soon as it occurs. The expressiveness hierarchy for counter monitors carries over to real-time monitors. We then show that 2 adders cannot simulate 3 counters in real-time. Finally, we show that real-time adder monitors with inequalities are as expressive as real-time Turing machines.

The Gamma Statechart Composition Framework is an integrated tool to support the design, verification and validation as well as code generation for component-based reactive systems. The behavior of each component is captured by a statechart, while assembling the system from components is driven by a domain-specific composition language. Gamma automatically synthesizes executable Java code extending the output of existing statechart-based code generators with composition related parts, and it supports formal verification by mapping composite statecharts to a back-end model checker. Execution traces obtained as witnesses during verification are back-annotated as test cases to replay an error trace or to validate external code generators. Tool demonstration video: https://youtu.be/ng7lKd1wlDo

The article proposes an enhanced behavior model using graphs of state transitions. The properties and advantages of the proposed model are discussed, UML-based Cooperative Interaction of Automata Objects (CIAO) language is described, attribute approach on its parsing mechanism is introduced. The proposed model for describing behavior is aimed at achieving higher reliability and productivity indicators when designing the secure architecture and implementing reactive and distributed systems in comparison with traditional methods. A side-by-side goal is to create a convenient publication language for describing parallel algorithms and distributed reactive systems. The offered model has advantages under certain conditions in comparison with other models of behavior description in the field of the description of asynchronous distributed reacting systems.

Responsiveness -the requirement that every request to a system be eventually handled- is one of the fundamental liveness properties of a reactive system and lies at the heart of all methods for specifying and verifying liveness. Average response time is a quantitative measure for the responsiveness requirement used commonly in performance evaluation. The static computation of average response time has proved remarkably elusive even for finite-state models of reactive systems. We present, for the first time, a robust formalism that allows the specification and computation of quantitative temporal properties including average response time. The formalism is based on nested weighted automata, which can serve as monitors for measuring the response time of a reactive system. We show thatquantitative properties specified by nested weighted automatacan be computed in exponential space for nondeterministic finite-state models of reactive systems and in polynomial time for probabilistic finite-state models.The specific property of average response time can be computed in polynomial time in both cases.This work is joint with Krishnendu Chatterjee and Jan Otop.

Software-intensive systems often consist of cooperating reactive components. In mobile and reconfigurable systems, their topology changes at run-time, which influences how the components must cooperate. The Scenario Modeling Language (SML) offers a formal approach for specifying the reactive behavior such systems that aligns with how humans conceive and communicate behavioral requirements. Simulation and formal checks can find specification flaws early. We present a framework for the Scenario-based Programming (SBP) that reflects the concepts of SML in Java and makes the scenario modeling approach available for programming. SBP code can also be generated from SML and extended with platform-specific code, thus streamlining the transition from design to implementation. As an example serves a car-to-x communication system. Demo video and artifact: http://scenariotools.org/esecfse-2017-tool-demo/

We increasingly live in cyber-physical spaces -- spaces that are both physical and digital, and where the two aspects are intertwined. Such spaces are highly dynamic and typically undergo continuous change. Software engineering can have a profound impact in this domain, by defining suitable modeling and specification notations as well as supporting design-time formal verification. In this paper, we present a methodology and a technical framework which support modeling of evolving cyber-physical spaces and reasoning about their spatio-temporal properties. We utilize a discrete, graph-based formalism for modeling cyber-physical spaces as well as primitives of change, giving rise to a reactive system consisting of rewriting rules with both local and global application conditions. Formal reasoning facilities are implemented adopting logic-based specification of properties and according model checking procedures, in both spatial and temporal fragments. We evaluate our approach using a case study of a disaster scenario in a smart city.

In this paper we present CLTSA (Counting Fluents Labelled Transition System Analyser), an extension of LTSA (Labelled Transition System Analyser) that incorporates counting fluents, a useful mechanism to capture properties related to counting events. Counting fluent temporal logic is a formalism for specifying properties of event-based systems, which complements the notion of fluent by the related concept of counting fluent. While fluents allow us to capture boolean properties of the behaviour of a reactive system, counting fluents are numerical values, that enumerate event occurrences. The tool supports a superset of FSP (Finite State Processes), that allows one to define LTL properties involving counting fluents, which can be model checked on FSP processes. Detailed information can be found at http://dc.exa.unrc.edu.ar/tools/cltsa.

RERS is an annual verification challenge that focuses on LTL and reachability properties of reactive systems. In 2017, RERS was extended to a one day workshop that in addition to the original challenge program also featured an invited talk about possible future developments. As a satellite of ISSTA and SPIN, the 2017 RERS Challenge itself increased emphasis on the parallel benchmark problems which, like their sequential counterparts, were generated using property-preserving transformations in order to scale their level of difficulty. The first half of the RERS workshop focused on the 2017 benchmark profiles, the evaluation of the received contributions, and short presentations of each participating team. The second half comprised discussions about attractive problem scenarios for future benchmarks, like race detection, the topic of the invited talk, and about systematic ways to leverage a tool's performance based on competition benchmarks and machine learning.

With the growing demand for real-time data originating from myriads of Internet-connected devices, the number of requests hitting today's computing infrastructures goes beyond what is manageable for operations and affordable for management. Coping with these challenges requires a modernization of the application architectures and the underlying infrastructures. The mobile nature inherent to modern communications and interactions requires a radical shift towards new computing paradigms that reflect the fully decentralized perspective of the emerging execution environment.To this end, the trend is to switch thinking from assembling components into systems to dynamically composing autonomous systems into systems-of-systems. Indeed, systems-of-systems possibly emerge dynamically as an opportunistic aggregation of systems available at a given time. Since these systems operate under highly dynamic conditions where both the entities and their interconnections are subject to continuous change, the traditional stability assumptions made on distributed systems' design are no longer valid. Indeed, the dynamic operating conditions introduce uncertainty, which may harm the dependability of the system. In order to guarantee the provision of dependable functionality in such an unknown, ever-changing execution environment, systems should be fluid and able to self-adapt their structure depending on the changing situation.This talk examines a set of principles and techniques facilitating the design and development of fully decentralized systems that leverage on self-adaptivity to mitigate run-time uncertainty. Specifically, the key objective is to efficiently and effectively provide engineers with proper abstractions to develop self-adaptive systems capable of being at the same time fluid, as well as dependable.

Bigraphs and Bigraphical Reactive Systems have been successfully applied in describing software architectures and modeling applications for context-aware systems and System of Systems. Therefore, it is very important to have an implementation of its dynamic to enable simulations and experimentations. In this paper, we present BiGMTE, a tool for bigraph matching and transformation. The implemented solution is based on an investigation of graph rewriting. In fact, we propose to simulate a bigraphical reactive system (i.e., bigraphs with a set of reaction rules which allow their rewriting) with a graph transformation system. Therefore, we propose two algorithms that encode a bigraph into a graph and a reaction rule into a graph rule. Finally, we give an example of modeling a SoS using BiGMTE.

Reactive systems respond to requests from an environment with appropriate timing. Because reactive systems are used widely in infrastructure, it is necessary that they are developed without flaws. Automatic synthesis of reactive systems from particular specifications is an ideal technique for ensuring development without flaws. Several tools for synthesis have been proposed, e.g., Lily, AcaciaPlus and Unbeast. Among them, AcaciaPlus can synthesize systems compositionally, and enables synthesis from large-scale specifications that could not previously be treated. However, the modularization of specifications depends largely on the computation time required for synthesis; this is not a trivial problem. In this paper, we discuss the modularization of specifications to enable efficient synthesis of reactive systems.

Self-adaptation is often loosely defined as the ability of systems to alter at runtime their behavior in response to changes in their environment, capabilities and goals. Yet we have been building self-adaptive systems have been engineered for decades. The shift from functional, input-output software, to reactive systems stems from the need to have software that can sense its environment, whose behavior is uncertain, and react accordingly.In this talk I will argue that this definition is too broad and that it dilutes a very real need for a particular quality of today's software systems. I will postulate that a more refined definition of adaptation should emphasize the need for systems to have the ability to react to changes that were originally unforeseen at design time, and to provide assurances on the correctness of these adaptations.How can systems be designed to account for what is unforeseen? I will argue that a key design decision for achieving self-adaptation is to endow systems with the capability of synthesizing at runtime discrete event controllers. Indeed, reactive systems that are requirements and assumptions aware, if extended with run time controller synthesis capabilities are equipped with a powerful infrastructure towards achieving assured self-adaptation.The vision of runtime discrete event controller synthesis at the heart of self-adaptation requires developing appropriate architectures. I will discuss Morph, a reference architecture that can support not only runtime synthesis but also deal with two other crucial elements: (i) interface, requirements and assumption awareness and (ii) runtime controller deployment and dynamic structural and behavioral reconfiguration.

Domain-specific modelling languages (DSML) enable domain users to model systems in their problem domain, using concepts and notations they are familiar with. The process of domain-specific modelling (DSM) consists of two stages: a language engineering stage where a DSML is created, and a system modelling stage where the DSML is used. Because techniques such as metamodelling and model transformation allow for a efficient creation of DSMLs, and using DSMLs significantly increases productivity, DSM is very suitable for early prototyping. Many systems that are modelled using DSMLs are reactive, meaning that during their execution, they respond to external input. Because of the complexity of input and response behaviour of reactive systems, it is desirable to test models as early as possible. However, while dedicated testing support for specific DSMLs has been provided, no systematic support exists for testing DSML models according to DSM principles. In this paper, we introduce a technique to automatically generate a domain-specific testing framework from an annotated DSML definition. In our approach, the DSML definition consists of a metamodel, a concrete syntax definition and operational semantics described as a schedule of graph rewrite rules, thus covering a large class of DSMLs. Currently, DSMLs with deterministic behaviour are supported, but we provide an outlook to other (nondeterministic, real-time or continuous-time) DSMLs. We illustrate the approach with a DSML for describing an elevator controller. We evaluate the approach and conclude that compared to the state-of-the-art, our testing support is significantly less costly, and similar or better (according to DSM principles) testing support is achieved. Additionally, the generative nature of the approach makes testing support for DSMLs less error-prone while catering the need for early testing.

During the synthesis of reactive systems, if we assume some behavioral property of an environment, any specification must include the environmental constraint in their conditions. In general, the behavior of a synthesized reactive system from such specifications only tends to satisfy the specification for the case where the environmental behavior follows these conditions; however, in a real-world setting it is desirable that the behavior of the reactive system satisfies the specification, even in the case of unexpected environmental behavior. We call tolerance for such a case environmental tolerance. In this paper, we give a simple definition of environmental tolerance, and propose a method for synthesizing a reactive system with environmental tolerance. In our method, the winning region of a safety game is computed using the Safraless synthesis method, and this is converted to a mean-payoff game such that a payoff is earned if the specification is satisfied. The optimal strategy for the game is then computed and the resulting reactive system is synthesized. The method is implemented and applied to specifications as an experiment, and it is confirmed that the obtained reactive systems have environmental tolerance.

© 2016 ACM.In many application domains, continuous operation is a desirable attribute for software-intensive systems. As the environment or system requirements change, so the system should change and adapt without stopping or unduly disturbing its operation. There is, therefore, a need for sound engineering techniques that can cope with dynamic change. In this paper we address the problem of dynamic update of controllers in reactive systems when the specification (environment assumptions, requirements and interface) of the current system changes. We present a general approach to specifying correctness criteria for dynamic update and a technique for automatically computing a controller that handles the transition from the old to the new specification, assuring that the system will reach a state in which such a transition can correctly occur. Indeed, using controller synthesis we show how to automatically build a controller that guarantees both progress towards update and safe update. Seven case studies have been implemented to validate the approach.

Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. Two of the main challenges in bringing reactive synthesis to software engineering practice are its very high worst-case complexity -- for linear temporal logic (LTL) it is double exponential in the length of the formula, and the difficulty of writing declarative specifications using basic LTL operators. To address the first challenge, Piterman et al. have suggested the General Reactivity of Rank 1 (GR(1)) fragment of LTL, which has an efficient polynomial time symbolic synthesis algorithm. To address the second challenge, Dwyer et al. have identified 55 LTL specification patterns, which are common in industrial specifications and make writing specifications easier. In this work we show that almost all of the 55 LTL specification patterns identified by Dwyer et al. can be expressed as assumptions and guarantees in the GR(1) fragment of LTL. Specifically, we present an automated, sound and complete translation of the patterns to the GR(1) form, which effectively results in an efficient reactive synthesis procedure for any specification that is written using the patterns. We have validated the correctness of the catalog of GR(1) templates we have created. The work is implemented in our reactive synthesis environment. It provides positive, promising evidence, for the potential feasibility of using reactive synthesis in practice.

In this paper, we present a solution to this year's DEBS Grand Challenge based on concepts from reactive systems. Reactive systems is a system architecture style with the following properties: Responsive, resilient, elastic, and message driven. When systems are built based on these properties, they tend to be more flexible, loosely-coupled, and scaleable. In this paper, we describe how to combine the operators given in the ReactiveX API to realize the individual challenge queries using asynchronous data-flows and evaluate the performance.

MpicOS is a reactive nano-kernel designed for controlling power- and energy-bound multicore embedded systems. Contrary to the mainstream approach of providing a multithreading framework with context saving, MpicOS is articulated around the reactive trigger-response abstraction with ultra-low power waits and a minimal API based on events and continuations. This change of paradigm keeps low the cost of re-engineering existing software, yet it results in major gains in power and energy usage of the system. Additionally, the reactive approach enables the deployment of novel applications on existing hardware platforms, resulting in new market opportunities and improved user experience.

A previous study claims that i* can be used to specify Teleo-Reactive systems requirements. However, that study also reveals that it shows some weaknesses. In this paper we identify those limitations and present TRiStar, an i* extension for specifying Teleo-Reactive systems requirements that overcomes them.

Behavioral programming (BP) is a decentralized scenario-based paradigm for the programming of reactive software, geared towards incremental and intuitive development. In this work we apply the principles of BP to a large, real-world case-study: a web-server. We discuss the conclusions learned from our attempt and propose several extension idioms to BP, aimed at improving the framework's scalability. Specifically, we propose extending BP with a timeout idiom for handling various time constraints, program-specific execution strategies, dynamic thread creation for efficiently allocating system resources, and support for parameterized events to handle inputs with infinite domains. Our extensions and case-study are implemented in a new framework for behavioral programming in C++.

Refinement calculus is a powerful and expressive tool for reasoning about sequential programs in a compositional manner. In this paper we present an extension of refinement calculus for reactive systems. Refinement calculus is based on monotonic predicate transformers, which transform sets of post-states into sets of pre-states. To model reactive systems, we introduce monotonic property transformers, which transform sets of output traces into sets of input traces. We show how to model in this semantics refinement, sequential composition, demonic choice, and other semantic operations on reactive systems. We use primarily higher order logic to express our results, but we also show how property transformers can be defined using other formalisms more amenable to automation, such as linear temporal logic (suitable for specifications) and symbolic transition systems (suitable for implementations). Finally, we show how this framework generalizes previous work on relational interfaces so as to be able to express systems with infinite behaviors and liveness properties.

Functional Reactive Programming (FRP) provides a method for programming continuous, reactive systems by utilizing signal functions that, abstractly, transform continuous input signals into continuous output signals. These signals may also be streams of events, and indeed, by allowing signal functions themselves to be the values carried by these events (in essence, signals of signal functions), one can conveniently make discrete changes in program behavior by "switching" into and out of these signal functions. This higher-order notion of switching is common among many FRP systems, in particular those based on arrows, such as Yampa. Although convenient, the power of switching is often an overkill and can pose problems for certain types of program optimization (such as causal commutative arrows [14]), as it causes the structure of the program to change dynamically at run-time. Without a notion of just-in-time compilation or related idea, which itself is beset with problems, such optimizations are not possible at compile time. This paper introduces two new ideas that obviate, in a predominance of cases, the need for switching. The first is a non-interference law for arrows with choice that allows an arrowized FRP program to dynamically alter its own structure (within statically limited bounds) as well as abandon unused streams. The other idea is a notion of a settable signal function that allows a signal function to capture its present state and later be restarted from some previous state. With these two features, canonical uses of higher-order switchers can be replaced with a suitable first-order design, thus enabling a broader range of static optimizations.

Given the increasingly sensitive data that web applications deal with, a lot of attention has been put into their security. Dynamic methods for ensuring confidentiality of secret data, such as monitors, are usually preferred due to their permissiveness and ability to adapt to dynamic features of web languages. One dynamic approach to confidentiality is through secure multi-execution, a technique which transforms programs into secure ones. A recent refinement of this technique led to a monitor for reactive systems such as web applications which is precise, in the sense that it raises an alarm exactly when a security condition is violated, and transparent, in the sense that the semantics of secure programs is preserved. A limitation of this and other approaches based on secure multi-execution is that there is a fixed set of channels with a fixed security level. However, most web applications create channels dynamically, even by doing something as trivial as adding a button to a page. Moreover, the security level of such new channel would be chosen dynamically. In this work, we overcome the limitation of assuming a fixed set of channels and introduce a model of reactive systems with dynamic channels and present a precise and transparent monitor for it.

We present a new visual language, SCCharts, designed for specifying safety-critical reactive systems. SCCharts use a statechart notation and provide determinate concurrency based on a synchronous model of computation (MoC), without restrictions common to previous synchronous MoCs. Specifically, we lift earlier limitations on sequential accesses to shared variables, by leveraging the sequentially constructive MoC. The semantics and key features of SCCharts are defined by a very small set of elements, the Core SCCharts, consisting of state machines plus fork/join concurrency. We also present a compilation chain that allows efficient synthesis of software and hardware.

Implementing systems in proof assistants like Coq and proving their correctness in full formal detail has consistently demonstrated promise for making extremely strong guarantees about critical software, ranging from compilers and operating systems to databases and web browsers. Unfortunately, these verifications demand such heroic manual proof effort, even for a single system, that the approach has not been widely adopted. We demonstrate a technique to eliminate the manual proof burden for verifying many properties within an entire class of applications, in our case reactive systems, while only expending effort comparable to the manual verification of a single system. A crucial insight of our approach is simultaneously designing both (1) a domain-specific language (DSL) for expressing reactive systems and their correctness properties and (2) proof automation which exploits the constrained language of both programs and properties to enable fully automatic, pushbutton verification. We apply this insight in a deeply embedded Coq DSL, dubbed Reflex, and illustrate Reflex's expressiveness by implementing and automatically verifying realistic systems including a modern web browser, an SSH server, and a web server. Using Reflex radically reduced the proof burden: in previous, similar versions of our benchmarks written in Coq by experts, proofs accounted for over 80% of the code base; our versions require no manual proofs.

We propose a method that addresses the following dilemma: model checking can formally expose off-nominal behaviors and unintended scenarios in the requirements of concurrent reactive systems. Requirements engineers and non-technical stakeholders who are the system domain experts can greatly benefit from jointly using model checking during the elicitation, analysis, and verification of system requirements. However, model checking is formal verification and many requirements engineers and domain experts typically lack the knowledge and training needed to apply model checking to the formal verification of requirements. To get full advantages of model checking and domain experts’ knowledge in verifying the system, we proposed a front end framework to model checking and evaluated our approach using a real world application.

We consider the synthesis of reactive systems that are robust against intermittent violations of their environment assumptions. Such assumptions are needed to allow many systems that work in a larger context to fulfill their tasks. Yet, due to glitches in hardware or exceptional operating conditions, these assumptions do not always hold in the field. Manually constructed systems often exhibit error-resilience and can continue to work correctly in such cases. With the development cycles of reactive systems becoming shorter, and thus reactive synthesis becoming an increasingly suitable alternative to the manual design of such systems, automatically synthesized systems are also expected to feature such resilience.The framework for achieving this goal that we present in this paper builds on generalized reactivity(1) synthesis, a synthesis approach that is well-known to be scalable enough for many practical applications. We show how, starting from a specification that is supported by this synthesis approach, we can modify it in order to use a standard generalized reactivity(1) synthesis procedure to find error-resilient systems. As an added benefit, this approach allows exploring the possible trade-offs in error resilience that a system designer has to make, and to give the designer a list of all Pareto-optimal implementations.

The functional behaviour of a reactive system can be modelled by an IOLTS (input output labelled transition system). However when the system is observed asynchronously (i.e., remotely through some medium), the apparent (or asynchronous) behaviour is different from its actual functional behaviour. Specifically, each trace of input output events executed by a system can appear distorted in infinite number of ways. Given a finite state IOLTS M describing the actual behaviour of a system, [7] shows how to define a corresponding infinite state IOLTS [M] describing the asynchronous behaviour of the same system. So defined, the resulting [M] is non-deterministic. Since [M] is also infinite state, it is not possible to convert it into its deterministic equivalent [M]D by the standard subset construction method. To this end, our first contribution in this paper is to show how to define an infinite state deterministic IOLTS [M]D from the given M. The states of M and [M]D bear correspondence such that if we distinguish some states of M as accept states, then we can have corresponding accept states in [M]D. Our second contribution is about reachability analysis. In particular, we prove how to determine whether a given state of [M]D leads to some accept state. This result assumes importance because of the infinite size of [M]D. After proving these fundamental results, we shift the discussion to the theory underlying conformance testing. The center of discussion is a test generation tool called TGV. We finally show how these results can be used to build a TGV-like approach for generating test cases for an asynchronously communicating system.

Program analysis plays an important role in a variety of software engineering processes, such as automated code refactoring, compiler optimizations, and program slicing. The internal program representation used by the program analysis algorithm affects the power and efficiency of the analysis. In particular, representations that contain data-flow information alongside control flow are known to be especially useful. While there are many popular internal program representations with data-flow information for traditional languages and platforms, few specifically target mobile applications. In this paper, we propose a new data-flow-enabled representation that addresses the screen-oriented nature of a mobile application and explores its potential. We consider a mobile application to be a reactive system whose states are the screens, and whose events are user actions, incoming communication, or anything else that causes transition from one screen to another. The resulting representation is a finite state machine extended with data-flow information. We suggest that this representation can greatly contribute to optimization, refactoring, and understanding of mobile applications.

Functional Reactive Programming (FRP) is an approach to the development of reactive systems which provides a pure functional interface, but which may be implemented as an abstraction of an imperative event-driven layer. FRP systems typically provide a model of behaviours (total time-indexed values, implemented as pull systems) and event sources (partial time-indexed values, implemented as push systems). In this paper, we investigate a type system for event-driven FRP programs which provide liveness guarantees, that is every input event is guaranteed to generate an output event. We show that FRP can be implemented on top of a model of sets and relations, and that the isomorphism between event sources and behaviours corresponds to the isomorphism between relations and set-valued functions. We then implement sets and relations using a model of continuations using the usual double-negation CPS transform. The implementation of behaviours as pull systems based on futures, and of event sources as push systems based on the observer pattern, thus arises from first principles. We also discuss a Java implementation of the FRP model.

Functional Reactive Programming (FRP) is a model of reactive systems in which signals are time-dependent values, and signal functions are functions between signals. Signal functions are required to be causal, in that output behaviour at time t is only allowed to depend on input behaviour up to time t. In order to enforce causality, many FRP libraries are arrowized, in that they provide combinators for building signal functions, rather than allowing users to write functions directly. In this paper, we provide a definition of deep causality (which coincides with the usual definition on signals of base type, but differs on nested signals). We show that FRP types can be interpreted in System Fomega extended with a kind of time, and show that in this interpretation, a "theorems for free" argument shows that parametric functions are deep causal. Since all System Fomega functions are parametric, this implies that all implementable functions are deep causal. This model is the formal basis of the agda-frp-js FRP library for the dependently typed programming language Agda, which compiles to JavaScript and executes in the browser. Assuming parametricity of Agda, this allows reactive programs to be written as regular functions over signals, without sacrificing causality. All results in this paper have been mechanically verified in Agda.

Priority-based FRP (P-FRP) is a functional programming formalism for reactive systems that guarantees real-time response. Preempted tasks in P-FRP are aborted and have to restart when no higher priority tasks are present in the execution queue. The abort and eventual restart makes the response time of a lower priority task completely dependent on the execution pattern of higher priority tasks. Exact schedulability analysis methods of P-FRP that have been presented so far require the evaluation of all release scenarios of higher priority tasks. Unfortunately, the number of such scenarios scales exponentially with the size of the task set, making exact schedulability analysis of this execution model a computationally expensive proposition. The formal method of Time Petri Net (TPN) has previously been used for schedulability analysis of preemptive and non-preemptive models. TPNs for P-FRP or other transaction like execution models have not been developed yet. In this paper, we develop TPN models for the transactional execution model of P-FRP and show that TPNs offer an efficient alternative for schedulability analysis of this model. We have implemented our TPNs in the model checker ROMEO and have validated the correctness of our models through experimental task sets.

Priority-based Functional Reactive Programming (FRP) is a new declarative approach to modeling and building reactive systems. Preempted tasks in P-FRP are aborted and have to restart when higher priority tasks have completed. Unlike the preemptive model of execution, there is no notion of critical instance in P-FRP. Determination of the actual value of Worst-Case Response Time (WCRT) in P-FRP requires evaluation of an exponential number of release scenarios. Such a 'brute-force' computation is expensive and impractical in several situations. In previous work, researchers have presented a polynomial time algorithm which uses fixed point iteration to compute an approximate upper bound on response time. However, this algorithm fails to converge for several task sets and hence is quite limited in use. In this paper, we present a more robust algorithm that computes response time bounds of P-FRP tasks and guarantees a result for all task sets. Experimental results using synthetic task sets of different sizes have also been presented.

"Timed-Rebeca" is an actor-based modeling language for modeling real-time reactive systems. Its high-level constructs make it more suitable for using it by software practitioners compared to timed-automata based alternatives. Currently, the verification of Timed-Rebeca models is done by converting into timed-automata and using UPPAAL toolset to analyze the model. However, state space explosion and time consumption are the major limitations of using the back-end timed automata model for verification. In this paper, we propose a new approach for direct schedulability checking and deadlock freedom verification of Timed-Rebeca models. The new approach exploits the key feature of Timed-Rebeca, which is encapsulation of concurrent elements. In the proposed method, each state stores the local time of each actor separately, avoiding the need for a global time in the state. This significantly decreases the size of the state space. We prove the bisimilarity of the generated transition system (called floating-time transition system) and the state space generated based on Timed-Rebeca semantics. Also, we provide experimental results showing that the new approach mitigates the state space explosion problem of the former method and allows model-checking of larger problems.

The strength of goal models is their ability to assess candidate solutions against high level criteria for many stakeholders, allowing system-wide trade-offs to be performed. We argue that, in a context-aware system, reasoning based on goal models can complement standard rule-based reasoning engines for decision making without involving explicit interaction with the user. While rule-based systems excel in filtering out unsuitable solutions based on clear criteria, it is difficult to rank suitable solutions based on vague, qualitative criteria of stakeholders with a rule-based approach. The User Requirements Notation (URN) is a goal-based and scenario-based requirements modeling language that has been applied to many different domains, from reactive systems to telecommunication standards to business processes. For context-aware systems, URN's workflow notation can describe the overall behavior of a context-aware system and URN's goal models can further enhance reasoning about contextual situations. While URN already supports some of the interactions between workflow and goal models required for the specification of context-aware systems, it does not yet fully support the modeling, design-time simulation, and run-time execution of a context-aware system based on its URN model. This paper (i) introduces such a modeling, simulation, and execution environment, (ii) discusses three architectural solutions for combined rule-based and goal-oriented reasoning, and (iii) reports on a URN profile that describes a domain-specific language for context-aware reasoning using goal-orientation with the help of an example application from the health care domain.