Verification of real-time systems with preemption: negative and positive results

The aim of this article is to explore the problem of verification of preemptible real-time systems, i.e. systems composed of tasks which can be suspended and resumed by an on-line scheduler. The first contribution of the article is to show that this problem is unfortunately undecidable. To overcome this negative result, we restrict the real-time tasks to be periodic and the implementation to be functionally deterministic, meaning that the preemptions do not affect the functional behaviour and preserve some temporal properties satisfied by the specification. We prove that the verification problem of functional determinism is decidable. This outlines a verification strategy: (1) prove that the scheduled real-time system is deterministic, (2) consider a deterministic non preemptible behaviour which is functionally equivalent to the executions and (3) verify the properties on this behaviour.     

Minimum and maximum delay problems in real-time systems

We consider a finite-state system with a finite number of clocks, where the transitions may depend on the values of the clocks, and may reset some of the clocks. We address the complexity and provide algorithms for the following problems. Suppose that the system starts from a given current state with a given assignment of values to the clocks. Can a given target state ever appear in the history of the system? What is the earliest time it can appear? What is the latest time it can appear?     

Dual ceiling protocol for real-time synchronization under preemption threshold scheduling

The application of object-oriented design methods to real-time embedded systems is seriously hindered by the lack of existing real-time scheduling techniques that can be seamlessly integrated into these methods. Preemption threshold scheduling (PTS) enables a scalable real-time system design and thus has been suggested as a solution to this problem. However, direct adoption of PTS may lead to long priority inversion since object-oriented real-time systems require synchronization considerations in order to maintain consistent object states. In this paper, we propose the dual ceiling protocol (DCP) in order to solve this problem. While DCP exploits both priority ceilings and preemption threshold ceilings, this is not a straightforward integration of existing real-time synchronization protocols for PTS. We present the rationale for the locking conditions of DCP and show that it leads to the least blocking and response times by comparison with other real-time synchronization protocols. We also present its blocking properties and schedulability analyses. We implemented PTS and DCP in a real-time object-oriented CASE tool and present the associated experimental results, which show that the proposed protocol is a viable solution that is superior to other real-time synchronization protocols for PTS.     

低复杂度的阈值优化实时调度算法

嵌入式实时系统在其CPU及内存资源相对稀缺时,必须采用复杂度低,系统开销小的调度算法.基于阈值的调度算法可以提高任务的调度性,减少任务间的切换,以此减少内存需求和系统开销.提出了基于抢占差值的阈值分配优化算法.算法在最小阈值分配法基础上,从高优先级向低优先级方向设置任务的阈值,为任务集找出一组满足最大抢占差值的阈值分配方案.经过理论分析及实例验证,算法可以显著降低任务的切换次数,并且算法的复杂度优于传统的优化算法.     

sensitivity minimization for delay systems

This paper announces results on the problem of feedback compensator design for ^∞ norm weighted sensitivity minimization when the plant contains a delay in the input. A complete solution is presented for the case of one pole/zero weighting function and a single-input/single-output plant for stable minimum-phase rational part. Generalizations and proofs will be published elsewhere.     

Finite-dimensional observers for delay systems

A finite-dimensional observer theory is formulated for a class of point delayed systems. The observer is characterized by the fact that it directly generates a finite-dimensional feedback controller for this class of systems. The theory is based on a preliminary approximation theory which allows the delay system to be exponentially approximated by a system of ordinary differential equations.     

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     

Network invariants for real-time systems

We extend the approach of model checking parameterized networks of processes by means of network invariants to the setting of real-time systems. We introduce timed transition structures (which are similar in spirit to timed automata) and define a notion of abstraction that is safe with respect to linear temporal properties. We strengthen the notion of abstraction to allow a finite system, then called network invariant, to be an abstraction of networks of real-time systems. In general the problem of checking abstraction of real-time systems is undecidable. Hence, we provide sufficient criteria, which can be checked automatically, to conclude that one system is an abstraction of a concrete one. Our method is based on timed superposition and discretization of timed systems. We exemplify our approach by proving mutual exclusion of a simple protocol inspired by Fischer’s protocol, using the model checker TLV. Part of this work was done during O. Grinchtein’s stay at Weizmann Institute. This author was supported by the European Research Training Network “Games”.     

Scheduling for embedded real-time systems

The authors review several approaches to control-oriented and dataflow-oriented software scheduling to determine whether a given technique can satisfy deadlines, throughput, and other constraints for embedded real-time systems     

Concurrent engineering for real-time systems

The Incremental Prototyping Technology for Embedded Real-Time Systems (Iptes) project, which is part of ESPRIT II, is described. The goal of the project is to develop methodologies and tools for the distributed prototyping of real-time systems. The work concentrates on two areas of support for concurrent engineering: adapting graphical-animation techniques to real-time-system development and creating a mechanism for propagating changes within and between tasks     

Requirements-based monitors for real-time systems

Before designing safety- or mission-critical real-time systems, a specification of the required behavior of the system should be produced and reviewed by domain experts. After the system has been implemented, it should be thoroughly tested to ensure that it behaves correctly. This is best done using a monitor, a system that observes the behavior of a target system and reports if that behavior is consistent with the requirements. Such a monitor can be used both as an oracle during testing and as a supervisor during operation. Monitors should be based on the documented requirements of the system. If the target system is required to monitor or control real-valued quantities, then the requirements, which are expressed in terms of the monitored and controlled quantities, will allow a range of behaviors to account for errors and imprecision in observation and control of these quantities. Even if the controlled variables are discrete valued, the requirements must specify the timing tolerance. Because of the limitations of the devices used by the monitor to observe the environmental quantities, there is unavoidable potential for false reports, both negative and positive, This paper discusses design of monitors for real-time systems, and examines the conditions under which a monitor will produce false reports. We describe the conclusions that can be drawn when using a monitor to observe system behavior     

Conformance testing for real-time systems

We propose a new framework for black-box conformance testing of real-time systems. The framework is based on the model of partially-observable, non-deterministic timed automata. We argue that partial observability and non-determinism are essential features for ease of modeling, expressiveness and implementability. The framework allows the user to define, through appropriate modeling, assumptions on the environment of the system under test (SUT) as well as on the interface between the tester and the SUT. We consider two types of tests: analog-clock tests and digital-clock tests. Our algorithm for generating analog-clock tests is based on an on-the-fly determinization of the specification automaton during the execution of the test, which in turn relies on reachability computations. The latter can sometimes be costly, thus problematic, since the tester must quickly react to the actions of the system under test. Therefore, we provide techniques which allow analog-clock testers to be represented as deterministic timed automata, thus minimizing the reaction time to a simple state jump. We also provide algorithms for static or on-the-fly generation of digital-clock tests. These tests measure time only with finite-precision digital clocks, another essential condition for implementability. We also propose a technique for location, edge and state coverage of the specification, by reducing the problem to covering a symbolic reachability graph. This avoids having to generate too many tests. We report on a prototype tool called and two case studies: a lighting device and the Bounded Retransmission Protocol. Experimental results obtained by applying on the Bounded Retransmission Protocol show that only a few tests suffice to cover thousands of reachable symbolic states in the specification.     

Worst-case response time analysis of real-time tasks under fixed-priority scheduling with deferred preemption

Fixed-priority scheduling with deferred preemption (FPDS) has been proposed in the literature as a viable alternative to fixed-priority pre-emptive scheduling (FPPS), that obviates the need for non-trivial resource access protocols and reduces the cost of arbitrary preemptions. This paper shows that existing worst-case response time analysis of hard real-time tasks under FPDS, arbitrary phasing and relative deadlines at most equal to periods is pessimistic and/or optimistic. The same problem also arises for fixed-priority non-pre-emptive scheduling (FPNS), being a special case of FPDS. This paper provides a revised analysis, resolving the problems with the existing approaches. The analysis is based on known concepts of critical instant and busy period for FPPS. To accommodate for our scheduling model for FPDS, we need to slightly modify existing definitions of these concepts. The analysis assumes a continuous scheduling model, which is based on a partitioning of the timeline in a set of non-empty, right semi-open intervals. It is shown that the critical instant, longest busy period, and worst-case response time for a task are suprema rather than maxima for all tasks, except for the lowest priority task. Hence, that instant, period, and response time cannot be assumed for any task, except for the lowest priority task. Moreover, it is shown that the analysis is not uniform for all tasks, i.e. the analysis for the lowest priority task differs from the analysis of the other tasks. These anomalies for the lowest priority task are an immediate consequence of the fact that only the lowest priority task cannot be blocked. To build on earlier work, the worst-case response time analysis for FPDS is expressed in terms of known worst-case analysis results for FPPS. The paper includes pessimistic variants of the analysis, which are uniform for all tasks, illustrates the revised analysis for an advanced model for FPDS, where tasks are structured as flow graphs of subjobs rather than sequences, and shows that our analysis is sustainable.     

A constraint programming model for the scheduling of JIT cross-docking systems with preemption

In this paper, a scheduling problem of minimizing the total of the earliness, tardiness and the number of preemption for the outbound trucks on a cross-dock system is considered. This problem, which is known to be NP-hard, is compatible with the concepts of just-in-time (JIT) production and supply chain management. A new multi-criteria model, with non-linear terms and integer variables, which cannot be solved efficiently for large sized problems, is proposed. This paper also shows how to map a JIT cross-dock model to a constraint satisfaction problem (CSP) and integer programming (IP). To solve the model for real size applications, a genetic algorithm (GA) is applied. Finally, a computational experiment is carried out to analyze the performances of CSP, GA and IP models with respect to modeling capability, solution quality and time.     

Bounding set calculation for neural network-based output feedback adaptive control systems

Evaluating the bounding set of dynamic systems subject to direct neural-adaptive control is a critical issue in applications where the control system must undergo a rigorous verification process in order to comply with certification standards. In this paper, the boundedness problem is addressed for a comprehensive class of uncertain dynamic systems. Several common but unnecessary approximations that are typically performed to simplify the Lyapunov analysis have been avoided in this effort. This leads to a more accurate and general formulation of the bounding set for the overall closed loop system. The conditions under which boundedness can be guaranteed are carefully analyzed; additionally, the interactions between the control design parameters, the ‘Strictly Positive Realness’ condition, and the shape and dimensions of the bounding set are discussed. Finally, an example is presented in which the bounding set is calculated for the neuro-adaptive control of an F/A-18 aircraft, along with a numerical study to evaluate the effect of several design parameters.     

Stability conditions for integral delay systems

In this paper we consider a special class of integral delay systems arising in several stability problems of time‐delay systems. For these integral systems we derive stability and robust stability conditions in terms of Lyapunov–Krasovskii functionals. More explicitly, after providing the stability conditions we compute quadratic functionals and apply them to derive exponential estimates for solutions, and robust stability conditions for perturbed integral delay systems. Copyright © 2008 John Wiley & Sons, Ltd.     

Delayless observers for systems with delay

The design of minimal-order observers for linear systems having a time-delay in the state variables is considered. Necessary and sufficient conditons are established for the existence of delayless observers for these systems.     

Linear estimation for random delay systems

This paper is concerned with the linear estimation problems for discrete-time systems with random delayed observations. When the random delay is known online, i.e., time-stamped, the random delayed system is reconstructed as an equivalent delay-free one by using measurement reorganization technique, and then an optimal linear filter is presented based on the Kalman filtering technique. However, the optimal filter is time-varying, stochastic, and does not converge to a steady state in general. Then an alternative suboptimal filter with deterministic gains is developed under a new criteria. The estimator performance in terms of their error covariances is provided, and its mean square stability is established. Finally, a numerical example is presented to illustrate the efficiency of proposed estimators.