Formal Analysis of Discrete-Event Systems with Hard Real-Time Bounds
Systémy řízené diskrétními událostmi (DES) jsou široce používané jako modelovací formalismus v pravděpodobnostní verifikaci a analýze výkonnosti. Chování těchto modelů je určeno diskrétními událostmi, které nastávají náhodně ve spojitém čase. Zabýváme se dopadem pevných časových hranic v těchto syst...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2014
|
| Témata: | |
| On-line přístup: | http://is.muni.cz/th/139854/fi_d/ |
| Shrnutí: | Systémy řízené diskrétními událostmi (DES) jsou široce používané jako modelovací formalismus v pravděpodobnostní verifikaci a analýze výkonnosti. Chování těchto modelů je určeno diskrétními událostmi, které nastávají náhodně ve spojitém čase. Zabýváme se dopadem pevných časových hranic v těchto systémech, jako např. hranice čekání v rámci modelu nebo časová hranice v jeho požadovaném chování. Dříve neexistoval žádný základní rigorózní text o takových pevných hranicích v DES přes jejich přítomnost v mnohých prakticky orientovaných článcích. Ukážeme, že DES vykazují nestabilní chování a obecně nemají limitní distribuci. Tento výsledek je obzvláště překvapivý, protože je v rozporu s několika předchozími výsledky. Kromě toho poskytujeme dostačující podmínky pro stabilitu DES. Dále se zabýváme tím, jak se změní situace, pokud nejsou pevné hranice součástí modelu a místo toho jsou součástí specifikace jeho požadovaného chování. Ukážeme, že takové systémy netrpí nestabilitou jako v předchozím Discrete-event systems (DES) are widely used as a modelling formalism in probabilistic verification and performance evaluation. The behaviour of these models is driven by discrete events that occur randomly in continuous time. We study the impact of hard real-time bounds within DES such as time-outs changing the state of the model or deadlines in the specification of the desired behaviour of the model. Previously, there was no rigorous foundational material on such hard real-time bounds despite their presence in numerous practically oriented papers. We show that DES with hard real-time bounds can exhibit an unstable behaviour and in general do not have a long-run average distribution. This is rather surprising as it contradicts several previous results. We also provide sufficient conditions upon which DES with hard real-time bounds are guaranteed to be stable. Furthermore, we study what changes if the hard real-time bounds are not part of the DES but a part of the specification of its |
|---|---|
| Popis jednotky: | Vedoucí práce: Antonín Kučera |
| Fyzický popis: | ix, 118 s. |