Detail publikace

Towards Smaller Invariants for Proving Coverability

HOLÍK, L.; HOLÍKOVÁ, L. Towards Smaller Invariants for Proving Coverability. In Computer Aided Systems Theory - EUROCAST 2017. Berlin Heidelberg: Springer Verlag, 2018. p. 109-116. ISBN: 978-3-319-74727-9.
Název česky
Směrem k menším invariantům pro dokázání spolehlivosti
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Holíková Lenka, Ing., Ph.D. (UITS)
Klíčová slova

parallel system, verification, petri nets, WSTS, CEGAR

Abstrakt

V tomto článku zkoumáme možnost vylepšení stávajících metod ověřování paralelních systémů. Zvláště se soustředíme na vlastnost bezpečnosti dobře strukturovaných přechodových systémů. Naše práce je relevantní především pro nedávné metody, které jsou založeny na hledání induktivních invariantů pomocí sekvence zjemňování získaných z protipříkladů. Naším cílem je zlepšit celkovou efektivitu tohoto přístupu tím, že se soustředíme na nalezení takových zjemnění, které povedou k stručnějším invariantům. Za tímto účelem navrhujeme analyzovat tzv. minimální protipříklady. Tyto protipříklady jsou dostatečně krátké, aby umožnily podrobnější analýzu. Experimentovali jsme s jednoduchým zpřesňovacím algoritmem založeným na analýze minimálních běhů a uspěli jsme ve vygenerování výrazně stručnějších invariantů než těch, které jsou generovány v nejmodernějších metodách.

Rok
2018
Strany
109–116
Sborník
Computer Aided Systems Theory - EUROCAST 2017
ISBN
978-3-319-74727-9
Vydavatel
Springer Verlag
Místo
Berlin Heidelberg
DOI
10.1007/978-3-319-74727-9_13
UT WoS
000531202800013
EID Scopus
2-s2.0-85041711934
BibTeX 
@inproceedings{BUT155053,
  author="Lukáš {Holík} and Lenka {Holíková}",
  title="Towards Smaller Invariants for Proving Coverability",
  booktitle="Computer Aided Systems Theory - EUROCAST 2017",
  year="2018",
  pages="109--116",
  publisher="Springer Verlag",
  address="Berlin Heidelberg",
  doi="10.1007/978-3-319-74727-9\{_}13",
  isbn="978-3-319-74727-9",
  url="https://www.fit.vut.cz/research/publication/11735/"
}
Nahoru