On hierarchically developing reactive systems

The hierarchical development method is one of the most practical and effective methods for designing large reactive systems by allowing a design at different levels of abstraction. Combining hierarchical specification with hierarchical implementation plays a key role in decreasing the complexity of the verification of these systems. But, up to now, little work has been done related to the topic. In this paper, we investigate this issue.     

TRAMMAS: A tracing model for multiagent systems

Agent's flexibility and autonomy, as well as their capacity to coordinate and cooperate, are some of the features which make multiagent systems useful to work in dynamic and distributed environments. These key features are directly related to the way in which agents communicate and perceive each other, as well as their environment and surrounding conditions. Traditionally, this has been accomplished by means of message exchange or by using blackboard systems. These traditional methods have the advantages of being easy to implement and well supported by multiagent platforms; however, their main disadvantage is that the amount of social knowledge in the system directly depends on every agent actively informing of what it is doing, thinking, perceiving, etc. There are domains, for example those where social knowledge depends on highly distributed pieces of data provided by many different agents, in which such traditional methods can produce a great deal of overhead, hence reducing the scalability, efficiency and flexibility of the multiagent system. This work proposes the use of event tracing in multiagent systems, as an indirect interaction and coordination mechanism to improve the amount and quality of the information that agents can perceive from both their physical and social environment, in order to fulfill their goals more efficiently. In order to do so, this work presents an abstract model of a tracing system and an architectural design of such model, which can be incorporated to a typical multiagent platform.     

Superposition refinement of reactive systems

Superposition refinement enhances an algorithm by superposing one computation mechanism onto another mechanism, in a way that preserves the behavior of the original mechanism. Superposition seems to be particularly well suited to the development of parallel and distributed programs: an originally simple sequential algorithm can be extended with mechanisms that distribute control and state information to many processes, thus permitting efficient parallel execution of the algorithm. We will show in this paper how superposition of reactive systems is expressed in the refinement calculus. We illustrate the power of this method by a case study, showing how a distributed broadcasting system is derived through a sequence of superposition refinements.     

Testing interruptions in reactive systems

Modelling and testing of reactive systems with interruptions are discussed. These systems are commonly found in portable devices, where interruptions to a running application can be demanded at any time, due to concurrent execution of processes sharing a single resource, such as screen, as well as arrival of calls from network distributed services. Since the possible number of combinations of allowed interruptions is large, proper test case selection activities need to be performed. But, in order to systematically investigate and select test cases, it is fundamental to explicitly model interruption behaviour in a compositional way, avoiding the need for explicit enumeration. This work presents a strategy for testing interruptions in reactive systems that covers modelling for testing of systems with interruptions, generation and selection of sound test cases. The strategy is supported by the LTS-BT tool. Moreover, a formal model of an environment devoted to execution of test cases with interruptions is presented. Finally, a case study illustrates its applicability in the mobile phone application domain.     

Scheduling for reactive real-time systems

In designing Chinook, a hardware-software cosynthesis system for reactive real-time controllers, the impact of timing constraints on software scheduling has been a central concern. By dividing constraints into two levels, corresponding to low-level interactions with device interfaces and high-level real-time response and rate requirements, we have developed solutions tailored to each aspect. These scheduling techniques enable Chinook to map a high-level specification onto a specified collection of processors and peripheral devices while respecting performance requirements     

Rigorous examination of reactive systems

The goal of the RERS challenge is to evaluate the effectiveness of various verification and validation approaches on reactive systems, a class of systems that is highly relevant for industrial critical applications. The RERS challenge brings together researchers from different areas of software verification and validation, including static analysis, model checking, theorem proving, symbolic execution, and testing. The challenge provides a forum for experimental comparison of different techniques on specifically designed verification tasks. These benchmarks are automatically synthesized to exhibit chosen properties, and then enhanced to include dedicated dimensions of difficulty, such as conceptual complexity of the properties (e.g., reachability, safety, liveness), size of the reactive systems (a few hundred lines to millions of lines), and complexity of language features (arrays and pointer arithmetic). The STTT special section on RERS describes the results of the evaluations and the different analysis techniques that were used in the RERS challenges 2012 and 2013.     

Modeling data-intensive reactive systems with relational transition systems

In this paper, the formalism of Relational Transition Systems (RTSes) is used to model data-intensive reactive systems, and four RTS models of reactive systems based on temporal logic programming, production systems, recurrence equations, and Petri nets are presented. The paper also describes different methods of comparison of the expressive powers of various RTSes in terms of the trajectories they can generate and carries out this comparison for the four RTS formalisms. It is shown that these formalisms have the same expressive power in the deterministic case. The paper also compares expressive powers of non-deterministic production systems and non-deterministic temporal logic programming systems. It is shown that, although the two formalisms are incomparable in the general case, their restricted versions are isomorphic to each other. Received December 7, 1993 / January 26, 1995     

Dynamic subtree tracing and its application in pay-TV systems

A traitor tracing algorithm can be used to identify content decoders that are used in the process of committing piracy. Fiat and Tassa introduced the concept of dynamic traitor tracing. A dynamic traitor tracing algorithm is based on examining content, either rendered illegally by a decoder or re-broadcast by the pirate. In addition, real-time feedback from the pirate’s network is used to adapt the state of the algorithm. This results in very efficient schemes, measured by the number of iterations required to identify all traitors. Drawbacks of currently available dynamic traitor tracing algorithms are that the best-known, real-time computational cost and bandwidth usage depend linearly on the number of content decoders. In particular, for large populations of content decoders, for example, common in pay-TV applications, these schemes can become impractical as system requirements can no longer be fulfilled. This paper presents a new dynamic traitor tracing algorithm, referred to as dynamic subtree tracing. The new algorithm inherits the advantages of the previously presented dynamic schemes and eliminates their disadvantages. In particular, it is shown that the number of iterations, the computational cost, the bandwidth usage, and the amount of storage in a decoder are all logarithmic in the number of content decoders. This makes the new scheme attractive for application in pay-TV systems, as illustrated with numerical examples.     

Communication in reactive multiagent robotic systems

Multiple cooperating robots are able to complete many tasks more quickly and reliably than one robot alone. Communication between the robots can multiply their capabilities and effectiveness, but to what extent? In this research, the importance of communication in robotic societies is investigated through experiments on both simulated and real robots. Performance was measured for three different types of communication for three different tasks. The levels of communication are progressively more complex and potentially more expensive to implement. For some tasks, communication can significantly improve performance, but for others inter-agent communication is apparently unnecessary. In cases where communication helps, the lowest level of communication is almost as effective as the more complex type. The bulk of these results are derived from thousands of simulations run with randomly generated initial conditions. The simulation results help determine appropriate parameters for the reactive control system which was ported for tests on Denning mobile robots.     

Optimal reactive compensation in power systems

This article describes a method for planning the type, location and minimum amount of installed reactive capacity necessary for maintaining an acceptable voltage profile in a power system during credible contingencies. The problem is formulated as the minimisation of the cost function representing the total cost of the reactive compensation provided. A mixed integer linear programming technique is used subject to constraints of network reactive power flow and allowable limits on busbar voltages and tap change transformers. A dynamic sensitivity measure is used to adjust the cost coefficients to obtain the best location of the compensating elements. The method is quite flexible in that both inductive and capacitative compensators are included and that the magnitude of the compensation can be treated as discrete and/or continuous variables. Test results, together with comparison with earlier methods, are also presented.     

Verification of external specifications of reactive systems

External specification is currently approached by specification languages for describing and analyzing system requirements. The external specification can be defined during the early stages of the system development and can be very useful for: checking the class/system/subsystem requirements; checking the system composition; evaluating costs of reuse; defining validated reference requirements, histories, and traces for the final validation. The paper presents a collection of criteria in order to formally verify the external specification of reactive systems/subsystems. The verification criteria are grounded on the Tempo Reale object-oriented language (TROL) specification model for real-time systems. In TROL, the external specification is expressed in terms of ports and clauses with temporal constraints. The goal of the verification criteria presented is to check the completeness and consistency of the external specification with special attention to temporal constraints. These criteria can be applied to other real-time specification models and have been enforced in the tool object oriented machine state (TOOMS) tool. A practical example illustrates the verification process that embodies these criteria     

Generating test case chains for reactive systems

Testing of reactive systems is challenging because long input sequences are often needed to drive them into a state to test a desired feature. This is particularly problematic in on-target testing, where a system is tested in its real-life application environment and the amount of time required for resetting is high. This article presents an approach to discovering a test case chain—a single software execution that covers a group of test goals and minimizes overall test execution time. Our technique targets the scenario in which test goals for the requirements are given as safety properties. We give conditions for the existence and minimality of a single test case chain and minimize the number of test case chains if a single test case chain is infeasible. We report experimental results with our ChainCover tool for C code generated from Simulink models and compare it to state-of-the-art test suite generators.     

A denotational theory of synchronous reactive systems

In this paper, systems which interact permanently with their environments are considered. Such systems are encountered, for instance, in real-time control or signal processing systems, C³-systems, and man-machine interfaces, to mention just a few cases. The design and implementation of such systems require a concurrent programming language which can be used to verify and synthesize the synchronization mechanisms, and to perform transformations of the concurrent source code to match a particular target architecture. Synchronous languages are convenient tools for such a purpose: they rely on the assumptions that: (1) internal actions of synchronous systems are instantaneous, and (2) communication with the environment is performed via instantaneous flashes involving some external stimuli. In this paper, we present a mathematical model of synchronous languages and illustrate its use on the language. This model is denotational, and encompasses both relational and functional styles of specification. It allows us to answer fundamental questions related to synchronous languages, such as “what are the basic constructions which should be provided by such languages?”     

On a traitor tracing scheme from ACISP 2003

At ACISP 2003 conference, Narayanan, Rangan and Kim proposed a secret-key traitor tracing scheme used for pay TV system. In this note, we point out a flaw in their scheme.     

Modelling timed reactive systems from natural-language requirements

At the very beginning of system development, typically only natural-language requirements are documented. As an informal source of information, however, natural-language specifications may be ambiguous and incomplete; this can be hard to detect by means of manual inspection. In this work, we present a formal model, named data-flow reactive system (DFRS), which can be automatically obtained from natural-language requirements that describe functional, reactive and temporal properties. A DFRS can also be used to assess whether the requirements are consistent and complete. We define two variations of DFRS: a symbolic and an expanded version. A symbolic DFRS (s-DFRS) is a concise representation that inherently avoids an explicit representation of (possibly infinite) sets of states and, thus, the state space-explosion problem. We use s-DFRS as part of a technique for test-case generation from natural-language requirements. In our approach, an expanded DFRS (e-DFRS) is built dynamically from a symbolic one, possibly limited to some bound; in this way, bounded analysis (e.g., reachability, determinism, completeness) can be performed. We adopt the s-DFRS as an intermediary representation from which models, for instance, SCR and CSP, are obtained for the purpose of test generation. An e-DFRS can also be viewed as the semantics of the s-DFRS from which it is generated. In order to connect such a semantic representation to established ones in the literature, we show that an e-DFRS can be encoded as a TIOTS: an alternative timed model based on the widely used IOLTS and ioco. To validate our overall approach, we consider two toy examples and two examples from the aerospace and automotive industry. Test cases are independently created and we verify that they are all compatible with the corresponding e-DFRS models generated from symbolic ones. This verification is performed mechanically with the aid of the NAT2TEST tool, which supports the manipulation of such models.     

基于变迁系统的反应型控制系统建模与分析

文中通过对基本变迁系统进行相应的扩充，分别给并发、实时及混成等3个不同轴象层次反应型控制系统的计算模型，并分析它们各自不同的特点。     

Spectra: a specification language for reactive systems

We introduce Spectra, a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Spectra comes with the Spectra Tools, a set of analyses, including a synthesizer to obtain a correct-by-construction implementation, several means for executing the resulting controller, and additional analyses aimed at helping engineers write higher-quality specifications. We present the language in detail and give an overview of its tool set. Together with the language and its tool set, we present four collections of many, non-trivial, large specifications, written by undergraduate computer science students for the development of autonomous Lego robots and additional example reactive systems. The collected specifications can serve as benchmarks for future studies on reactive synthesis. We present the specifications, with observations and lessons learned about the potential use of reactive synthesis by software engineers.