BENEŠ, Nikola, Jan KŘETÍNSKÝ, Kim G. LARSEN a Jiří SRBA. On Determinism in Modal Transition Systems. Theoretical Computer Science. Elsevier, 2009, roč. 410/2009, č. 41, s. 4026-4043. ISSN 0304-3975.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název On Determinism in Modal Transition Systems
Název česky O determinismu v modálních přechodových systémech
Autoři BENEŠ, Nikola (203 Česká republika, domácí), Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí), Kim G. LARSEN (208 Dánsko) a Jiří SRBA (203 Česká republika, domácí).
Vydání Theoretical Computer Science, Elsevier, 2009, 0304-3975.
Další údaje
Originální jazyk angličtina
Typ výsledku Článek v odborném periodiku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Nizozemské království
Utajení není předmětem státního či obchodního tajemství
Impakt faktor Impact factor: 0.943
Kód RIV RIV/00216224:14330/09:00029307
Organizační jednotka Fakulta informatiky
UT WoS 000269865800003
Klíčová slova anglicky compositional verification; modal transition systems; determinism; refinement; consistency
Štítky compositional verification, consistency, determinism, modal transition systems, REFINEMENT
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: RNDr. Nikola Beneš, Ph.D., učo 72525. Změněno: 24. 10. 2013 16:20.
Anotace
Modal transition systems (MTS) is a formalism which extends the classical notion of labelled transition systems by introducing transitions of two types: must transitions that have to be present in any implementation of the MTS and may transitions that are allowed but not required. The MTS framework has proved to be useful as a specification formalism of component-based systems as it supports compositional verification and stepwise refinement. Nevertheless, there are some limitations of the theory, namely that the naturally defined notions of modal refinement and modal composition are incomplete with respect to the semantic view based on the sets of the implementations of a given MTS specification. Recent work indicates that some of these limitations might be overcome by considering deterministic systems, which seem to be more manageable but still interesting for several application areas. In the present article, we provide a comprehensive account of the MTS framework in the deterministic setting. We study a number of problems previously considered on MTS and point out to what extent we can expect better results under the restriction of determinism.
Anotace česky
Modální přechodové systémy (MTS) jsou formalismus rozšiřující klasické označkované přechodové systémy zavedením přechodů dvou typů: must přechody, které musí být přítomny v každé implementaci a may přechody, které jsou povolené, ale nikoli vyžadované. Rámec MTS se prokázal být užitečným formalismem pro specifikaci komponentových systémů, protože podporuje kompozicionální verifikaci a postupné zjemňování. Nicméně tato teorie má i své limity: přirozeně definované pojmy modálního zjemnění a modální kompozice jsou neúplné vzhledem k sémantice založené na množinách implementací dané MTS specifikace. Nedávné výsledky však naznačují, že tyto potíže mohou být překonány uvážením deterministických systémů, které se zdají více zvladatelné, ale stále zajímavé pro řadu praktických oblastí. V tomto článku podáváme ucelenou studii MTS v deterministickém rámci. Studujeme řadu problémů dříve uvažovaných na MTS a ukazujeme, do jaké míry můžeme očekávat lepší výsledky při restrikci na determinismus.
Návaznosti
GA201/09/1389, projekt VaVNázev: Verifikace a analýza velmi velkých počítačových systémů
Investor: Grantová agentura ČR, Verifikace a analýza velmi velkých počítačových systémů
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
1M0545, projekt VaVNázev: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky
VytisknoutZobrazeno: 1. 9. 2024 01:09