Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2013 | Buch

Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs Kapitel lesen Erstes Kapitel lesen

Formal Modeling and Analysis of Timed Systems

11th International Conference, FORMATS 2013, Buenos Aires, Argentina, August 29-31, 2013. Proceedings

herausgegeben von: Víctor Braberman, Laurent Fribourg

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013, held in Buenos Aires, Argentina, in August 2013.

The 18 revised full papers presented were carefully reviewed and selected from 41 submissions. The book covers topics of foundations and semantics (theoretical foundations of timed systems and languages; comparison between different models, such as timed automata, timed Petri nets, hybrid automata, timed process algebra, max-plus algebra, probabilistic models); methods and Tools (techniques, algorithms, data structures, and software tools for analyzing timed systems and resolving temporal constraints, e.g., scheduling, worst-case execution time analysis, optimization, model checking, testing, constraint solving, etc.); applications (adaptation and specialization of timing technology in application domains in which timing plays an important role, e.g., real-time software, hardware circuits, and problems of scheduling in manufacturing and telecommunications).

Inhaltsverzeichnis

Frontmatter
Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs
Abstract
Quantifying the robustness of a real-time system consists in measuring the maximum extension of the timing delays such that the system still satisfies its specification. In this work, we introduce a more precise notion of robustness, measuring the allowed variability of the timing delays in their neighbourhood. We consider here the formalism of time Petri nets extended with inhibitor arcs. We use the inverse method, initially defined for timed automata. Its output, in the form of a parametric linear constraint relating all timing delays, allows the designer to identify the delays allowing the least variability. We also exhibit a condition and a construction for rendering robust a non-robust system.
Étienne André, Giuseppe Pellegrino, Laure Petrucci
Spectral Gap in Timed Automata
Abstract
Various problems about probabilistic and non-probabilistic timed automata (computing probability density, language volume or entropy) can be naturally phrased as iteration of linear operators in Banach spaces. Convergence of such iterations is guaranteed whenever the operator’s spectrum has a gap. In this article, for operators used in entropy computation, we use the theory of positive operators to establish the existence of such a gap. This allows to devise simple numeric algorithms for computing the entropy and prove their exponential convergence.
Eugene Asarin, Nicolas Basset, Aldric Degorre
Robust Weighted Timed Automata and Games
Abstract
Weighted timed automata extend timed automata with cost variables that can be used to model the evolution of various quantities. Although cost-optimal reachability is decidable (in polynomial space) on this model, it becomes undecidable on weighted timed games. This paper studies cost-optimal reachability problems on weighted timed automata and games under robust semantics. More precisely, we consider two perturbation game semantics that introduce imprecisions in the standard semantics, and bring robustness properties w.r.t. timing imprecisions to controllers. We give a polynomial-space algorithm for weighted timed automata, and prove the undecidability of cost-optimal reachability on weighted timed games, showing that the problem is robustly undecidable.
Patricia Bouyer, Nicolas Markey, Ocan Sankur
On MITL and Alternating Timed Automata
Abstract
One clock alternating timed automata (OCATA) have been recently introduced as natural extension of (one clock) timed automata to express the semantics of MTL [12]. We consider the application of OCATA to problem of model-checking MITL formulas (a syntactic fragment of MTL) against timed automata. We introduce a new semantics for OCATA where, intuitively, clock valuations are intervals instead of single values in ℝ. Thanks to this new semantics, we show that we can bound the number of clock copies that are necessary to allow an OCATA to recognise the models of an MITL formula. Equipped with this technique, we propose a new algorithm to translate an MITL formula into a timed automaton, and we sketch several ideas to define new model checking algorithms for MITL.
Thomas Brihaye, Morgane Estiévenart, Gilles Geeraerts
Predictability of Event Occurrences in Timed Systems
Abstract
We address the problem of predicting events’ occurrences in partially observable timed systems modelled by timed automata. Our contribution is many-fold: 1) we give a definition of bounded predictability, namely k-predictability, that takes into account the minimum delay between the prediction and the actual event’s occurrence; 2) we show that 0-predictability is equivalent to the original notion of predictability of S. Genc and S. Lafortune; 3) we provide a necessary and sufficient condition for k-predictability (which is very similar to k-diagnosability) and give a simple algorithm to check k-predictability; 4) we address the problem of predictability of events’ occurrences in timed automata and show that the problem is PSPACE-complete.
Franck Cassez, Alban Grastien
Transience Bounds for Distributed Algorithms
Abstract
A large variety of distributed systems, like some classical synchronizers, routers, or schedulers, have been shown to have a periodic behavior after an initial transient phase (Malka and Rajsbaum, WDAG 1991). In fact, each of these systems satisfies recurrence relations that turn out to be linear as soon as we consider max-plus or min-plus algebra. In this paper, we give a new proof that such systems are eventually periodic and a new upper bound on the length of the initial transient phase. Interestingly, this is the first asymptotically tight bound that is linear in the system size for various classes of systems. Another significant benefit of our approach lies in the straightforwardness of arguments: The proof is based on an easy convolution lemma borrowed from Nachtigall (Math. Method. Oper. Res. 46) instead of purely graph-theoretic arguments and involved path reductions found in all previous proofs.
Bernadette Charron-Bost, Matthias Függer, Thomas Nowak
Back in Time Petri Nets
Abstract
The time progress assumption is at the core of the semantics of real-time formalisms. It is also the major obstacle to the development of partial-order techniques for real-time distributed systems since the events are ordered both by causality and by their occurrence in time. Anyway, extended free choice safe time Petri nets (TPNs) were already identified as a class where partial order semantics behaves well. We show that, for this class, the time progress assumption can even be dropped (time may go back in case of concurrency), which establishes a nice relation between partial-order semantics and time progress assumption.
Thomas Chatain, Claude Jard
A Mechanized Semantic Framework for Real-Time Systems
Abstract
Concurrent systems consist of many components which may execute in parallel and are complex to design, to analyze, to verify, and to implement. The complexity increases if the systems have real-time constraints, which are very useful in avionic, spatial and other kind of embedded applications. In this paper we present a logical framework for defining and validating real-time formalisms as well as reasoning methods over them. For this purpose, we have implemented in the Coq proof assistant well known semantic domains for real-time systems based on labelled transitions systems and timed runs. We experiment our framework by considering the real-time CSP-based language fiacre, which has been defined as a pivot formalism for modeling languages (aadl, sdl, ...) used in the TOPCASED project. Thus, we define an extension to the formal semantic models mentioned above that facilitates the modeling of fine-grained time constraints of fiacre. Finally, we implement this extension in our framework and provide a proof method environment to deal with real-time system in order to achieve their formal certification.
Manuel Garnacho, Jean-Paul Bodeveix, Mamoun Filali-Amine
Quantitative Analysis of AODV and Its Variants on Dynamic Topologies Using Statistical Model Checking
Abstract
Wireless Mesh Networks (WMNs) are self-organising ad-hoc networks that support broadband communication. Due to changes in the topology, route discovery and maintenance play a crucial role in the reliability and the performance of such networks. Formal analysis of WMNs using exhaustive model checking techniques is often not feasible: network size (up to hundreds of nodes) and topology changes yield state-space explosion. Statistical Model Checking, however, can overcome this problem and allows a quantitative analysis.
In this paper we illustrate this by a careful analysis of the Ad hoc On-demand Distance Vector (AODV) protocol. We show that some optional features of AODV are not useful, and that AODV shows unexpected behaviour—yielding a high probability of route discovery failure.
Peter Höfner, Maryam Kamali
More or Less True DCTL for Continuous-Time MDPs
Abstract
Discounted Computation Tree Logic is a logic that measures utility (as a real value in the interval [0,1]) instead of discrete truth (only 0 or 1). It is able to express properties that give more weight to the near future than to the far future. This article extends earlier work on DCTL with time, to continuous-time Markov chains and continuous-time Markov decision processes. It presents model checking algorithms for the two possible semantics of DCTL.
A long version of this article containing full proofs is available as [4].
David N. Jansen
Incremental Language Inclusion Checking for Networks of Timed Automata
Abstract
Checking the language inclusion between two models is a fundamental problem arising in application areas such as formal verification or refinement in top-down design. We propose an incremental procedure for checking the language inclusion between two real-time specifications, modeled as networks of deterministic timed automata, where the two specifications are equivalent up to one component. For such classes of systems we aim to improve the efficiency of the language inclusion check by exploiting the compositional nature of the problem and avoiding the explicit parallel composition of the timed automata in the network. We first develop a generic procedure that gives freedom to specific implementation choices. We then propose an instantiation of the procedure that is based on bounded model checking techniques. We illustrate the application of our approach in a case study and discuss promising experimental results.
Willibald Krenn, Dejan Ničković, Loredana Tec
Nested Timed Automata
Abstract
This paper proposes a new timed model named nested timed automata (NeTAs). A NeTA is a pushdown system whose stack symbols are timed automata (TAs). It either behaves as the top TA in the stack, or switches from one TA to another by pushing, popping, or changing the top TA of the stack. Different from existing component-based context-switch models such as recursive timed automata and timed recursive state machines, when time passage happens, all clocks of TAs in the stack elapse uniformly. We show that the safety property of NeTAs is decidable by encoding NeTAs to the dense timed pushdown automata. NeTAs provide a natural way to analyze the recursive behaviors of component-based timed systems with structure retained. We illustrate this advantage by the deadline analysis of nested interrupts.
Guoqiang Li, Xiaojuan Cai, Mizuhito Ogawa, Shoji Yuen
On Fixed Points of Strictly Causal Functions
Abstract
We ask whether strictly causal components form well defined systems when arranged in feedback configurations. The standard interpretation for such configurations induces a fixed-point constraint on the function modelling the component involved. We define strictly causal functions formally, and show that the corresponding fixed-point problem does not always have a well defined solution. We examine the relationship between these functions and the functions that are strictly contracting with respect to a generalized distance function on signals, and argue that these strictly contracting functions are actually the functions that one ought to be interested in. We prove a constructive fixed-point theorem for these functions, and introduce a corresponding induction principle.
Eleftherios Matsikoudis, Edward A. Lee
Detecting Quasi-equal Clocks in Timed Automata
Abstract
A recent optimizations technique for timed model checking starts with a given specification of quasi-equal clocks. In principle, the zone graph can used to detect which clocks are quasi-equal; the construction of the zone graph would, however, defeat its very purpose (which is the optimization of this construction). In this paper, we present an abstraction that is effective for the goal of the optimization based on quasi-equal clocks: it is coarse enough to yield a drastic reduction of the size of the zone graph. Still, it is precise enough to identify a large class of quasi-equal clocks. The abstraction is motivated by an intuition about the way quasi-equalities can be tracked. We have implemented the corresponding reasoning method in the Jahob framework using an SMT solver. Our experiments indicate that our intuition may lead to a useful abstraction.
Marco Muñiz, Bernd Westphal, Andreas Podelski
On the Verification of Timed Discrete-Event Models
Abstract
Timed discrete-event (DE) is an actor-oriented formalism for modeling timed systems. A DE model is a network of actors consuming/producing timed events from/to a set of input/output channels. In this paper we study a basic DE model, called deterministic DE (DDE), where actors are simple constant-delay components, and two extensions of DDE: NDE, where actors are non-deterministic delays, and DETA, where actors are either deterministic delays or timed automata. We investigate verification questions on DE models and examine expressiveness relationships between the DE models and timed automata.
Christos Stergiou, Stavros Tripakis, Eleftherios Matsikoudis, Edward A. Lee
Symmetry Breaking for Multi-criteria Mapping and Scheduling on Multicores
Abstract
Multiprocessor mapping and scheduling is a long-old difficult problem. In this work we propose a new methodology to perform mapping and scheduling along with buffer memory optimization using an SMT solver. We target split-join graphs, a formalism inspired by synchronous data-flow (SDF) which provides a compact symbolic representation of data-parallelism. Unlike the traditional design flow for SDF which involves splitting of a big problem into smaller heuristic sub-problems, we deal with this problem as a whole and try to compute exact Pareto-optimal solutions for it. We introduce symmetry breaking constraints in order to reduce the run-times of the solver. We have tested our work on a number of SDF graphs and demonstrated the practicality of our method. We validate our models by running an image decoding application on the Tilera multicore platform.
Pranav Tendulkar, Peter Poplavko, Oded Maler
Confluence Reduction for Markov Automata
Abstract
Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. Recently, the process algebra MAPA was introduced to efficiently model such systems. As always, the state space explosion threatens the analysability of the models generated by such specifications. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep these models small. We define the notion of confluence directly on Markov automata, and discuss how to syntactically detect confluence on the MAPA language as well. That way, Markov automata generated by MAPA specifications can be reduced on-the-fly while preserving divergence-sensitive branching bisimulation. Three case studies demonstrate the significance of our approach, with reductions in analysis time up to an order of magnitude.
Mark Timmer, Jaco van de Pol, Mariëlle I. A. Stoelinga
Optimal Control for Linear-Rate Multi-mode Systems
Abstract
Linear-Rate Multi-Mode Systems is a model that can be seen both as a subclass of switched linear systems with imposed global safety constraints and as hybrid automata with no guards on transitions. We study the existence and design of a controller for this model that keeps at all times the state of the system within a given safe set. A sufficient and necessary condition is given for such a controller to exist as well as an algorithm that finds one in polynomial time. We further generalise the model by adding costs on modes and present an algorithm that constructs a safe controller which minimises the peak cost, the average-cost or any cost expressed as a weighted sum of these two. Finally, we present numerical simulation results based on our implementation of these algorithms.
Dominik Wojtczak
Backmatter
Metadaten
Titel
Formal Modeling and Analysis of Timed Systems
herausgegeben von
Víctor Braberman
Laurent Fribourg
Copyright-Jahr
2013
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-40229-6
Print ISBN
978-3-642-40228-9
DOI
https://doi.org/10.1007/978-3-642-40229-6

Premium Partner

    Bildnachweise