| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
R-automata
- 2008
-
Ingår i: CONCUR 2008 - Concurrency Theory. - Berlin : Springer-Verlag. - 9783540853602 ; , s. 67-81
-
Konferensbidrag (refereegranskat)abstract
- We introduce R-automata - finite state machines which operate on a finite number of unbounded counters. The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. R-automata can be, for example, used to model systems with resources (modeled by the counters) which are consumed in small parts but which can be replenished at once. We define the language accepted by an R-automaton relative to a natural number D as the set of words allowing a run along which no counter value exceeds D. As the main result, we show decidability of the universality problem, i.e., the problem whether there is a number D such that the corresponding language is universal. We present a proof based on finite monoids and the factorization forest theorem. This theorem was applied for distance automata in [12] - a special case of R-automata with one counter which is never reset. As a second technical contribution, we extend the decidability result to R-automata with Buchi acceptance conditions.
|
|
| 2. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Sampled universality of timed automata
- 2007
-
Ingår i: Foundations of Software Science and Computational Structures, Proceedings. - Berlin, Heidelberg : Springer Berlin Heidelberg. - 9783540713883 ; , s. 2-16
-
Konferensbidrag (refereegranskat)abstract
- Timed automata can be studied in not only a dense-time setting but also a discrete-time setting. The most common example of discrete-time semantics is the so called sampled semantics (i.e., discrete semantics with a fixed time granularity epsilon). In the real-time setting, the universality problem is known to be undecidable for timed automata. In this work, we study the universality question for the languages accepted by timed automata with sampled semantics. On the negative side, we show that deciding whether for all sampling periods epsilon a timed automaton accepts all timed words in epsilon-sampled semantics is as hard as in the real-time case, i.e., undecidable. On the positive side, we show that checking whether there is a sampling period such that a timed automaton accepts all untimed words in epsilon-sampled semantics is decidable. Our proof uses clock difference relations, developed to characterize the reachability relation for timed automata in connection with sampled semantics.
|
|
| 3. |
|
|
| 4. |
|
|
| 5. |
- Abdullah, Jakaria, et al.
(författare)
-
Towards a Tool : TIMES-Pro for Modeling, Analysis, Simulation and Implementation of Cyber-Physical Systems
- 2017
-
Ingår i: MODELS, ALGORITHMS, LOGICS AND TOOLS. - Cham : SPRINGER INTERNATIONAL PUBLISHING AG. - 9783319631219 - 9783319631202 ; , s. 623-639
-
Konferensbidrag (refereegranskat)abstract
- We consider a Cyber-Physical System (CPS) as a network of components that are either physical plants with continuous behaviors or discrete controllers. To build CPS's in a systematic manner, the TIMES-Pro tool is designed to support modeling, analysis and code generation for real-time simulation and final deployment. In this paper, we present our decisions in designing the modeling language, the tool architecture and features of TIMES-Pro, and also a case study to demonstrate its applicability.
|
|
| 6. |
- Abdullah, Jakaria, et al.
(författare)
-
Worst-Case Cause-Effect Reaction Latency in Systems with Non-Blocking Communication
- 2019
-
Ingår i: Design, Automation & Test in Europe Conference & Exhibition. - : IEEE. - 9783981926323 ; , s. 1625-1630
-
Konferensbidrag (refereegranskat)abstract
- In real-time embedded systems, a system functionality is often implemented using a data-flow chain over a set of communicating tasks. A critical non-functional requirement in such systems is to restrict the amount of time, i.e. cause-effect latency, for an input to impact its corresponding output. The problem of estimating the worst-case cause-effect latency is well-studied in the context of blocking inter-task communication. Recent research results show that non-blocking communication preserving functional semantics is critical for the model-based design of dynamically updatable systems. In this paper, we study the worst-case cause-effect reaction latency estimation problem in the context of non-blocking inter-task communication. We present a computationally efficient algorithm that tightly over-approximates the exact worst-case reaction latency in cause-effect data-flow chains.
|
|
| 7. |
|
|
| 8. |
|
|
| 9. |
|
|
| 10. |
- Amnell, Tobias, et al.
(författare)
-
TIMES: a Tool for Schedulability Analysis and Code Generation of Real-Time Systems
- 2003
-
Ingår i: Proceedings of the International Conference of Formal Modeling and Analysis of Timed Systems. - 9783540216711
-
Konferensbidrag (refereegranskat)abstract
- TIMES is a tool suite designed mainly for symbolic schedulability analysis and synthesis of executable code with predictable behaviours for real-time systems. Given a system design model consisting of(1) a set of application tasks whose executions may be required to meet mixed timing, precedence, and resource constraints,(2) a network of timed automata describing the task arrival patterns and(3) a preemptive or non-preemptive scheduling policy,TIMES will generate a scheduler, and calculate the worst case response times for the tasks. The design model may be further validated using a model checker e.g. UPPAAL and then compiled to executable C-code using the TIMES compiler. In this paper, we present the design and main features of TIMES including a summary of theoretical results behind the tool. TIMES can be downloaded at www.timestool.com.
|
|
