On tracing reactive systems

We present a rich and highly dynamic technique for analyzing, visualizing, and exploring the execution traces of reactive systems. The two inputs are a designer’s inter-object scenario-based behavioral model, visually described using a UML2-compliant dialect of live sequence charts (LSC), and an execution trace of the system. Our method allows one to visualize, navigate through, and explore, the activation and progress of the scenarios as they “come to life” during execution. Thus, a concrete system’s runtime is recorded and viewed through abstractions provided by behavioral models used for its design, tying the visualization and exploration of system execution traces to model-driven engineering. We support both event-based and real-time-based tracing, and use details-on-demand mechanisms, multi-scaling grids, and gradient coloring methods. Novel model exploration techniques include semantics-based navigation, filtering, and trace comparison. The ideas are implemented and tested in a prototype tool called the Tracer.     

On models of developing systems and their applications

We consider integral models based on the mathematical model proposed by V.M. Glushkov. We describe a two-sector version of the Glushkov model and consider the identification problem for model parameters. We propose a numerical identification method and present results of test computations. We consider the problem of power grid field described with a one-sector version of the Glushkov model. We give computational results based on real data.     

On one integral Volterra model of developing dynamical systems

We develop an approach for constructing continuous solutions of integral Volterra equations of the first kind that arise in modeling developing dynamical systems. We give existence theorems for the solutions and study their asymptotic behavior. Theoretical results are illustrated with numerical computations on test examples.     

An empirical approach to evaluating dependency locality in hierarchically structured software systems

In software development, especially component-based software development, dependency locality states that relevant software components should be at shorter distances than irrelevant components. This principle is used together with modularity and hierarchy to guide the design of large-scale complex software systems. In previous work, dependency locality and its correlation with design quality were studied by statically measuring the interactions between software components. This paper presents an empirical approach to evaluating the hierarchical structure of software systems through mining their revision history. Two metrics, spatial distance and temporal distance, are adapted to measure the dependencies between software components. The correlation of spatial distance and temporal distance between software components represents a factor that influences system design quality. More specially, a well designed system hierarchy should have a significant positive correlation while a non-significant positive correlation or a negative correlation would signify design flaws. In an application of this approach, we use Mantel test to study the dependency locality of six software systems from Apache projects.     

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.     

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     

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.     

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     

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.     

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.     

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?”     

A two-sector model of developing systems

A two-sector model of developing systems of V.M. Glushkov is studied; it is described by a system of nonclassical equations of the Volterra type that includes equations with variable lower limits of both first and second kinds. Numerical methods for solving systems of nonclassical Volterra equations are constructed.     

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.     

Equilibria in models of hierarchically organized dynamical control systems with regard to sustainable development conditions

We study dynamic game theoretic models for two- and three-level control systems taking into account sustainable development conditions. We consider methods of compulsion and impulsion as hierarchical control methods. We give definitions of equilibria and show algorithms for constructing them in various cases.     

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个不同轴象层次反应型控制系统的计算模型，并分析它们各自不同的特点。     

Information systems as social systems: Implications for developing countries

Abstract

Computer‐based information systems should be conceptualised as social systems in which technology is only one of the dimensions. This broader perspective on information systems offers opportunities for a deeper understanding of their development and use. The social systems approach is illustrated in the paper by two research projects in the UK on the evaluation of information systems and information systems strategy formulation. The relevance of the UK research to a developing country context is discussed and it is argued that methodologies which aim to provide an understanding of the organisational, social and political context are highly suitable for organisations in developing countries. Some implications are drawn for research, education and practice related to information systems in developing countries.