The proceedings contains 40 papers. Topics discussed include multimedia communication, multicast routing, asynchronous transfer mode switching control system, main memory database systems, formal specifications and ve...
详细信息
The proceedings contains 40 papers. Topics discussed include multimedia communication, multicast routing, asynchronous transfer mode switching control system, main memory database systems, formal specifications and verification, fault tolerance, timing analysis, realtimesystems, scheduling algorithms.
real-timesystems are distributed and require reliability. The formal verification and specification are important for real-timesystems. In this paper, in order to obtain reliability, we think the notion of dense-tim...
详细信息
real-timesystems are distributed and require reliability. The formal verification and specification are important for real-timesystems. In this paper, in order to obtain reliability, we think the notion of dense-time and probabilities are necessary. We propose the following methods in order to specify and verify performance properties in dense time model. (1) Probabilistic and dense time statecharts and temporal logic (2) An automatic verification method by probabilistic and dense time model checking.
This paper presents a scheduling technique for guaranteeing end-to-end timing constraints. applications are structured as a set of tasks which are the sequence of actions to produce an output. Task is decomposed into ...
详细信息
This paper presents a scheduling technique for guaranteeing end-to-end timing constraints. applications are structured as a set of tasks which are the sequence of actions to produce an output. Task is decomposed into subtasks and shares subtasks with other tasks. According to the proposed scheduling technique, for each instance of a task, the sequence of subtasks is determined off-line and then called by the task sequentially at runtime. This technique avoids unnecessary execution of shared tasks and satisfies precedence constraints between subtasks even in overload situations.
In this paper, we analyze the diagnosability and diagnosis problems of a multiprocessor systems using the test results generated by other processors in the system. We also propose some rules which find the faulty proc...
详细信息
In this paper, we analyze the diagnosability and diagnosis problems of a multiprocessor systems using the test results generated by other processors in the system. We also propose some rules which find the faulty processors in the system using the comparison approach. A polynomial time algorithm identify the faulty units of such a system can be implemented in realtime on the basis of the comparison results when the system is known to be diagnosable.
A main concern in the initial phases of the development of a system to be built is capturing the system requirements and expressing them as an adequate model, either formal or informal. In subsequent phases of the dev...
详细信息
A main concern in the initial phases of the development of a system to be built is capturing the system requirements and expressing them as an adequate model, either formal or informal. In subsequent phases of the development of the system this model is used as reference for transformation steps. In this paper we describe a reasonably successful experimental strategy for the implementation of real-timesystems, starting from a formal specification, resulting in an Ada 95 implementation of the system and we evaluate the approach based upon practical experiences.
A compositional CTL mode-checking algorithm for real-time concurrent systems with a discrete global clock is presented based on a new high-level description model. We implement the algorithm in a system called VERIFAS...
详细信息
ISBN:
(纸本)0818676264
A compositional CTL mode-checking algorithm for real-time concurrent systems with a discrete global clock is presented based on a new high-level description model. We implement the algorithm in a system called VERIFAST-2 which has passed the extended General Session Setup Control protocols with concurrency from 5 to 51 threads all in one minute and demonstrated truly scalable performance with respect to the size of concurrency. In this respect, it outperforms HyTech version 1.02b and VERIFAST-1. Then we discuss how to incorporate R.J. Parikh's classic work on semilinear expressions to verify software recursions.
There is a clear and urgent need for mechanisms that are able to integrate the real-time and the reliability requirements. So, it would be possible to address the real-time and fault-tolerance requirements together du...
详细信息
There is a clear and urgent need for mechanisms that are able to integrate the real-time and the reliability requirements. So, it would be possible to address the real-time and fault-tolerance requirements together during the design of the system. This would make the development of reliable real-timesystems simple and efficient. This paper presents the development of a fault-tolerant mechanism, one which is able to take into account the real-time constraints of the tasks. This mechanism is a real-time Recoverable Action which can provide both forward and backward error recovery. The atomic action is used as a natural way of achieving fault-tolerance in a distributed or parallel system. An adaptable scheduler is used to schedule the real-time Recoverable Action, guaranteeing the hardreal-time tasks.
In this paper, the end-to-end communication latency in HARTS(Hexagonal Architecture for real-timesystems) is evaluated, which is depends on the intra-node delay as well as the inter-node delay. While the inter-node d...
详细信息
In this paper, the end-to-end communication latency in HARTS(Hexagonal Architecture for real-timesystems) is evaluated, which is depends on the intra-node delay as well as the inter-node delay. While the inter-node delay is bounded due to the point-to-point real-time channel, the intra-node delay is variable according to the message traffic and the internal structure of a HARTS node. The intra-node delay is evaluated analytically and by computer simulation for the various implementational models, and an arbitration algorithm is proposed to provide real-time scheduling for VMEbus-based HARTS node.
In this paper, we discuss the problem of jointly scheduling both hard deadline of periodic and aperiodic tasks in dynamic priority systems. The proposed scheduling scheme has extended the APS (Alternative Priority Sch...
详细信息
ISBN:
(纸本)0818676264
In this paper, we discuss the problem of jointly scheduling both hard deadline of periodic and aperiodic tasks in dynamic priority systems. The proposed scheduling scheme has extended the APS (Alternative Priority Scheduling) algorithm which is developed by the authors. The APS algorithm has a simple slack calculation method which in consequence makes it be practical. The paper develops an efficient acceptance test method for hard-aperiodic requests. The on-line acceptance test performs to determine whether the timing requirements of the arriving hard aperiodic tasks can be met while guaranteeing all the deadlines of periodic tasks and any already accepted but not yet completed aperiodic tasks.
暂无评论