We study schedulability problems of timed systems with non-uniformly recurring computation tasks. Assume a set of real time tasks whose best and worst execution times, and deadlines are known. We use timed automata to...
详细信息
ISBN:
(纸本)354021299X
We study schedulability problems of timed systems with non-uniformly recurring computation tasks. Assume a set of real time tasks whose best and worst execution times, and deadlines are known. We use timed automata to describe the arrival patterns (and release times) of tasks. From the literature, it is known that the schedulability problem for a large class of such systems is decidable and can be checked efficiently. In this paper, we provide a summary on what is decidable and what is undecidable in schedulability analysis using timed automata. Our main technical contribution is that the schedulability problem will be undecidable if these three conditions hold: (1) the execution times of tasks are intervals, (2) a task can announce its completion time, and (3) a task can preempt another task. We show that if one of the above three conditions is dropped, the problem will be decidable. thus our result can be used as an indication in identifying classes of timed systemsthat can be analysed efficiently.
the two predominant program specialization techniques, partial evaluation and staged programming, take opposite approaches to automating binding-time analysis (BTA). Despite their common goal, there are no systems int...
详细信息
ISBN:
(纸本)354021299X
the two predominant program specialization techniques, partial evaluation and staged programming, take opposite approaches to automating binding-time analysis (BTA). Despite their common goal, there are no systems integrating both methods. Programmers must choose between the precision of manually placing staging annotations and the convenience of automating such annotation. We present an automatic BTA algorithm for a subset of MetaML. Such an algorithm provides a basis for a system integrating staged programming and partial evaluation because it allows programmers to switch between automatic and manual staging. Our algorithm is based on typing algorithm coupled with arithmetic-constraint solving. the algorithm decorates each subexpression of both a program and its type with numeric variables representing staging-an notations and then generates simple arithmetic constraints that describe the space of all possible stagings of the original program. Benefits of our approach include expressive BTA specifications in the form of stage-annotated types as well as support for polyvariance.
In this paper, we show how the simple structure of the linear programs encountered during symbolic minimum-cost reachability analysis of priced timed automata can be exploited in order to substantially improve the per...
详细信息
ISBN:
(纸本)354021299X
In this paper, we show how the simple structure of the linear programs encountered during symbolic minimum-cost reachability analysis of priced timed automata can be exploited in order to substantially improve the performance of the current algorithm. the idea is rooted in duality of linear programs and we show that each encountered linear program can be reduced to the dual problem of an instance of the min-cost flow problem. thus, we only need to solve instances of the much simpler min-cost flow problem during minimum-cost reachability analysis. Experimental results using UPPAAL show a 70-80 percent performance gain. As a main application area, we show how to solve energy-optimal task graph scheduling problems using the framework of priced timed automata.
An automated and configurable technique for runtime safety analysis of multithreaded programs is presented, which is able to predict safety violations from successful executions. Based on a user provided safety formal...
详细信息
ISBN:
(纸本)354021299X
An automated and configurable technique for runtime safety analysis of multithreaded programs is presented, which is able to predict safety violations from successful executions. Based on a user provided safety formal specification, the program is automatically instrumented to emit relevant state update events to an observer, which further checks them against the safety specification. the events are stamped with dynamic vector clocks, enabling the observer to infer a causal partial order on the state updates. All event traces that are consistent withthis partial order, including the actual execution trace, are analyzed on-line and in parallel, and a warning is issued whenever there is a trace violating the specification. this technique can be therefore seen as a bridge between testing and model checking. To further increase scalability, a window in the state space can be specified, allowing the observer to infer the most probable runs. If the size of the window is 1 then only the received execution trace is analyzed, like in testing;if the size of the window is infinity then all the execution traces are analyzed, such as in model checking.
We describe a scalable incomplete boundedness test for the communication buffers in UML RT models. UML RT is a variant of the UML modeling language, tailored to describing asynchronous concurrent embedded systems. We ...
详细信息
ISBN:
(纸本)354021299X
We describe a scalable incomplete boundedness test for the communication buffers in UML RT models. UML RT is a variant of the UML modeling language, tailored to describing asynchronous concurrent embedded systems. We reduce UML RT models to systems of communicating finite state machines (CFSMs). We propose a series of further abstractions that leaves us with a system of linear inequalities. those represent the message sending and receiving effect that the control flow cycles of every process have on the overall message buffer. the test tries to establish the existence of a linear combination of the effect vectors so that at least one message can occur an unbounded number of times. We discuss the complexity of this test and present experimental results using the IBOC system that we are implementing. Scalability of the test is in part due to the fact that it is polynomial for the type of sparse control flow graphs that are derived from UML RT models. Also, the analysis is local, i.e., it avoids the combinatorial state space explosion due to concurrency of the models. We also present a method to derive upper bound estimates for the maximal occupancy of each individual message buffer. While we focus on the analysis of UML RT models, the analysis can directly be applied to any type of CFSM models.
In the deterministic safety analysis codes are required in order to provide evaluations of potential nuclear plant accidents. In the fields of the core transient behaviour, the computer codes have achieved a high degr...
详细信息
In the deterministic safety analysis codes are required in order to provide evaluations of potential nuclear plant accidents. In the fields of the core transient behaviour, the computer codes have achieved a high degree of realistic modelling. Nevertheless, some further tools for the investigations of the wide range of physical phenomena in the whole plant transient, such as modeling the ex-core detector signals and the malfunctioning of the emergency control system are unavoidable, too. the programs and methods used in KFKI-AEKI for safety analysis of VVER-440 NPP are presented. the accident analysis methodology for a boron dilution scenario, in which an inactive coolant loop is started, is shown.
the simplicity of the sequential injection (SIA) manifold and its low need for maintenance makes it an ideal tool in speciation. As miniaturization and reduction of reagent consumption are also ultimate goals in chemi...
详细信息
the simplicity of the sequential injection (SIA) manifold and its low need for maintenance makes it an ideal tool in speciation. As miniaturization and reduction of reagent consumption are also ultimate goals in chemical sensing, it is useful to review the use of combined injection and programmed flow as a central issue in designing SIA systems with chemical sensors and structurally simplified chemical analysers. this overview gives an insight into the current state, analytical scope and performance characteristics of sequential injection systems as analytical tools for speciation. the suitability of SIA for speciation analysis is illustrated by the methods used in the conduits of sequential injection systems for the chemical conversion of different chemical forms into detectable chemical species. Configurations of the basic sequential injection speciation analysissystems were designed around a multi-syringe-time-based-injection system with one detector, direct and indirect speciation of different forms using a single detector including diode array detection and direct speciation of different forms using multiple detection. Examples showing the use of SIA for the simultaneous determination or speciation of metal ions, inorganic anions and organic compounds are given with some recent results from our research groups. (C) 2004 Elsevier B.V. All rights reserved.
Growing acceptance of model-based test generation in the industry has created a need for a tester-friendly model construction process and associated tools. In this paper, we present an automated approach for checking ...
详细信息
On-Line Analytical Processing (OLAP) systems based on multidimensional databases are essential elements of decision support. However, most existing data is stored in "ordinary" relational OLTP databases, i.e...
详细信息
tools for managing systems requirements help keeping specifications consistent, up-to-date and accessible. Since the requirements for complex systems are themselves complex information structures that must be handled ...
详细信息
tools for managing systems requirements help keeping specifications consistent, up-to-date and accessible. Since the requirements for complex systems are themselves complex information structures that must be handled in complex process scenarios, there are many strong requirements concerning a tool for managing them. this work presents a requirements catalog for requirements management toolsthat is based on substantial project experience (including tool evaluation experiences) in the area of automotive as well as aircraft and defense systems. the purpose of this catalog is to help users compare and select requirements management tools as well as helping tool providers to direct future tool developments.
暂无评论