| 1. |
- Fersman, Elena, et al.
(författare)
-
Task Automata : Schedulability, Decidability and Undecidability
- 2007
-
Ingår i: Information and Computation. - : Elsevier. - 0890-5401 .- 1090-2651. ; 205:8, s. 1149-1172
-
Tidskriftsartikel (refereegranskat)abstract
- We present a model, task automata, for real time systems with non-uniformly recurring computation tasks. It is an extended version of timed automata with asynchronous processes that are computation tasks generated (or triggered) by timed events. Compared with classical task models for real time systems, task automata may be used to describe tasks (1) that are generated non-deterministically according to timing constraints in timed automata, (2) that may have interval execution times representing the best case and the worst case execution times, and (3) whose completion times may influence the releases of task instances. We generalize the classical notion of schedulability to task automata. A task automaton is schedulable if there exists a scheduling strategy such that all possible sequences of events generated by the automaton are schedulable in the sense that all associated tasks can be computed within their deadlines. Our first technical result is that the schedulability for a given scheduling strategy can be checked algorithmically for the class of task automata when the best case and the worst case execution times of tasks are equal. The proof is based on a decidable class of suspension automata: timed automata with bounded subtraction in which clocks may be updated by subtractions within a bounded zone. We shall also study the borderline between decidable and undecidable cases. Our second technical result shows that the schedulability checking problem will be undecidable if the following three conditions hold: (1) the execution times of tasks are intervals, (2) the precise finishing time of a task instance may influence new task releases, and (3) a task is allowed to preempt another running task.
|
|
| 2. |
- Galusin, Sergey, 1985-, et al.
(författare)
-
An approach to joint application of integrated deterministic-probabilistic safety analysis and PSA Level 2 to severe accident issues in Nordic BWRs
- 2016
-
Ingår i: PSAM 2016 - 13th International Conference on Probabilistic Safety Assessment and Management2017. - : International Association for Probabilistic Safety Assessment and Management (IAPSAM).
-
Konferensbidrag (refereegranskat)abstract
- In this paper we outline a conceptual approach for combined use of Probabilistic Safety Assessment (PSA) and Integrated Deterministic-Probabilistic Safety Assessment (IDPSA), considering Nordic Boiling Water Reactor (BWR) severe accident issues (specifically ex-vessel steam explosion and debris bed coolability) for illustration.We describe a conceptual approach based on post processing of the results generated by IDPSA to update the “static” Boolean structures in the standard PSA representation. The challenge in the evaluation is to retain the failure combinations from the PSA to allow for component importance evaluation, to be able to perform the calculations in a reasonable time frame and to use all relevant information from the IDPSA results.We discuss the approaches for determination of the event space (for IDPSA analysis) which is consistent with PSA damage states from PSA-L1 and L2. We also discuss application of post processing approach for analysis of huge amount of data generated in the process of uncertainty space exploration, which is difficult to use directly in decision making process including incorporation of such data into PSA framework, to update structures of “static” Boolean structures in standard PSA. Using data post processing approach we can significantly reduce amount of information which represents results from IDPSA analysis.
|
|
| 3. |
- Krcal, Jan, et al.
(författare)
-
Scalable Analysis of Fault Trees with Dynamic Features
- 2015
-
Ingår i: 2015 45Th Annual IEEE/IFIP International Conference On Dependable Systems And Networks. - 9781479986293 ; , s. 89-100
-
Konferensbidrag (refereegranskat)abstract
- Fault trees constitute one of the essential formalisms for static safety analysis of various industrial systems. Dynamic fault trees (DFT) enrich the formalism by time-dependent behavior, e.g., repairs or functional dependencies. Analysis of DFT is so far limited to substantially smaller models than those required for, e.g., nuclear power plants. We propose a fault tree formalism that combines both static and dynamic features, called SD fault trees. It gives the user the freedom to express each equipment failure either statically, without modeling temporal information, or dynamically, allowing repairs and other timed interdependencies. We introduce an analysis algorithm for an important subclass of SD fault trees. The algorithm (1) scales similarly to static algorithms and (2) allows for a more realistic analysis compared to static algorithms as it takes into account temporal interdependencies. Finally, we demonstrate the applicability of the method by an experimental evaluation on fault trees of nuclear power plants.
|
|
| 4. |
- 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.
|
|
| 5. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
R-automata
- 2008
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- We introduce \emphR-automata – a model for analysis of systems with resources which are consumed in small parts but which can be replenished at once. An R-automaton is a finite state machine which operates on a finite number of unbounded counters (modeling the resources). The values of the counters can be incremented, reset to zero, or left unchanged along the transitions. 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. The decidability proof is based on a reformulation of the problem in the language of finite monoids and solving it using the factorization forest theorem. This approach extends the way in which the factorization forest theorem was used to solve the limitedness problem for distance automata in Simon, 1994. We also show decidability of the non-emptiness problem and the limitedness problem, i.e., whether there is a natural number D such that the corresponding language is non-empty resp.\ all the accepted words can also be accepted with counter values smaller than D. Finally, we extend the decidability results to R-automata with Büchi acceptance conditions.
|
|
| 6. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Sampled semantics of timed automata
- 2010
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 6:3, s. 14:1-37
-
Tidskriftsartikel (refereegranskat)
|
|
| 7. |
- 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.
|
|
| 8. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Universality of R-automata with value copying
- 2009
-
Ingår i: Electronic Notes in Theoretical Computer Science. - : Elsevier BV. - 1571-0661. ; 239, s. 131-141
-
Tidskriftsartikel (refereegranskat)
|
|
| 9. |
|
|
| 10. |
- Krcal, Pavel, et al.
(författare)
-
Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
- 2006
-
Ingår i: Computer Aided Verification (CAV 2006). ; , s. 14-
-
Konferensbidrag (refereegranskat)abstract
- We study channel systems whose behaviour (sending and receiving messagesvia unbounded FIFO channels) must follow given timing constraintsspecifying the execution speeds of the local components. We proposeCommunicating Timed Automata (CTA) to model such systems. The goal is tostudy the borderline between decidable and undecidable classes of channelsystems in the timed setting. Our technical results include: (1) CTA withone channel without shared states in the form $(A_1,A_2, c_{1,2})$ isequivalent to one-counter machine, implying that verification problemssuch as checking state reachability and channel boundedness are decidable,and (2) CTA with two channels without sharing states in the form$(A_1,A_2,A_3, c_{1,2},c_{2,3})$ has the power of Turing machines. Notethat in the untimed setting, these systems are no more expressive thanfinite state machines. This shows that the capability of synchronizing ontime makes it substantially more difficult to verify channel systems.
|
|
