On Combining Partial Order Reduction with Fairness Assumptions
BRIM, Luboš, Ivana ČERNÁ, Pavel MORAVEC a Jiří ŠIMŠA. On Combining Partial Order Reduction with Fairness Assumptions. In Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006). Bonn, Germany: University Bonn, 2006, s. 1-16. ISBN 978-3-540-70951-0. |
Další formáty:
BibTeX
LaTeX
RIS
|
Základní údaje | |
---|---|
Originální název | On Combining Partial Order Reduction with Fairness Assumptions |
Název česky | Kombinace redukce pomocí reprezentantů s fairness předpoklady |
Autoři | BRIM, Luboš (203 Česká republika, garant), Ivana ČERNÁ (203 Česká republika), Pavel MORAVEC (203 Česká republika) a Jiří ŠIMŠA (203 Česká republika). |
Vydání | Bonn, Germany, Proceedings of the 11th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2006), s. 1-16, 2006. |
Nakladatel | University Bonn |
Další údaje | |
---|---|
Originální jazyk | angličtina |
Typ výsledku | Stať ve sborníku |
Obor | 10201 Computer sciences, information science, bioinformatics |
Stát vydavatele | Německo |
Utajení | není předmětem státního či obchodního tajemství |
Kód RIV | RIV/00216224:14330/06:00015442 |
Organizační jednotka | Fakulta informatiky |
ISBN | 978-3-540-70951-0 |
UT WoS | 000245773800006 |
Klíčová slova anglicky | partial order reduction; fairness; LTL model checking |
Štítky | Fairness, LTL model checking, partial order reduction |
Příznaky | Mezinárodní význam, Recenzováno |
Změnil | Změnila: prof. RNDr. Ivana Černá, CSc., učo 1419. Změněno: 31. 3. 2010 15:40. |
Anotace |
---|
We present a new approach to combine partial order reduction with fairness in the context of LTL model checking. For this purpose, we define several behaviour classes representing typical fairness assumptions and examine how various reduction techniques affect these classes. In particular, we consider both reductions preserving all behaviours and reductions preserving only some behaviours. |
Anotace česky |
---|
Je prezentován nový přístup kombinace redukce pomocí reprezentantů a fairness podmínek v kontextu ověřování LTL vlastností modelu. Je zadefinováno několik tříd chování popisující typické fairness přepoklady a dokázáno, jak jednotlivé redukční techniky zachovávají tyto třídy. Zejména je uvažován případ, kdy redukce zachovávají všechna chování a redukce zachovávající jen některá z nich. |
Návaznosti | |
---|---|
GA201/06/1338, projekt VaV | Název: Automatizovaná verifikace softwaru |
Investor: Grantová agentura ČR, Automatizovaná verifikace softwaru | |
GD102/05/H050, projekt VaV | Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů |
Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů | |
MSM0021622419, záměr | Název: Vysoce paralelní a distribuované výpočetní systémy |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy | |
1ET408050503, projekt VaV | Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů | |
1M0545, projekt VaV | Název: Institut Teoretické Informatiky |
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky |
VytisknoutZobrazeno: 19. 9. 2024 09:02