BENEŠ, Nikola, Luboš BRIM, Ivana ČERNÁ, Jiří SOCHOR, Pavlína VAŘEKOVÁ a Barbora ZIMMEROVÁ. Partial Order Reduction for State/Event LTL. Brno, Czech Republic: Faculty of Informatics, Masaryk University. 21 s. Technical report FIMU-RS-2008-07. 2008.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Partial Order Reduction for State/Event LTL
Název česky Metoda partial order redukce pro State/Event LTL
Autoři BENEŠ, Nikola (203 Česká republika, domácí), Luboš BRIM (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí), Jiří SOCHOR (203 Česká republika, domácí), Pavlína VAŘEKOVÁ (203 Česká republika, domácí) a Barbora ZIMMEROVÁ (203 Česká republika, garant, domácí).
Vydání Brno, Czech Republic, 21 s. Technical report FIMU-RS-2008-07, 2008.
Nakladatel Faculty of Informatics, Masaryk University
Další údaje
Originální jazyk angličtina
Typ výsledku Výzkumná zpráva
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Česká republika
Utajení není předmětem státního či obchodního tajemství
WWW FIMU Technical Reports URL
Kód RIV RIV/00216224:14330/08:00024265
Organizační jednotka Fakulta informatiky
Klíčová slova anglicky Partial order reduction; state/event LTL; formal verification
Štítky formal verification, partial order reduction, state/event LTL
Příznaky Mezinárodní význam
Změnil Změnil: prof. Ing. Jiří Sochor, CSc., učo 2446. Změněno: 18. 9. 2015 12:32.
Anotace
The paper introduces a partial order reduction technique for verification of state/event LTL properties. The core of the partial order reduction is a novel notion of stuttering equivalence which we call state/event stuttering equivalence. The positive attribute of the equivalence is that it can be resolved with existing methods for partial order reduction. State/event LTL properties are, in general, not preserved under state/event stuttering equivalence. To this end we define a new logic, called weak state/event LTL, which is invariant under the new equivalence.
Anotace česky
Článek představuje novou metodu partial order reduction pro verifikaci vlastností logiky state/event LTL. Jádrem metody je nová definice stuttering ekvivalence, kterou nazýváme state/event stuttering ekvivalence.
Návaznosti
MSM0021622419, záměrNá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
1ET400300504, projekt VaVNázev: Realistická aplikace formálních metod v komponentových systémech
Investor: Akademie věd ČR, Realistická aplikace formálních metod v komponentových systémech
1ET408050503, projekt VaVNá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ů
VytisknoutZobrazeno: 19. 4. 2024 16:54