Detail výsledku

Abstract Regular Model Checking

BOUAJJANI, A.; HABERMEHL, P.; VOJNAR, T. Abstract Regular Model Checking. Lecture Notes in Computer Science, 2004, vol. 2004, no. 3114, p. 372-386. ISSN: 0302-9743.
Typ
článek v časopise
Jazyk
anglicky
Autoři
Bouajjani Ahmed
Habermehl Peter
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

We propose abstract regular model checking as a new generic techniquefor verification of parametric and infinite-state systems. Thetechnique combines the two approaches of regular model checking andverification by abstraction. We propose a general framework of themethod as well as several concrete ways of abstracting automata ortransducers, which we use for modelling systems and encoding sets oftheir configurations as usual in regular model checking. Theabstraction is based on collapsing states of automata (or transducers)and its precision is being incrementally adjusted by analysing spuriouscounterexamples. We illustrate the technique on verification of a widerange of systems including a novel application of automata-basedtechniques to an example of systems with dynamic linked data structures.

Klíčová slova

formal verification, infinite-state and parameterized systems, regular model checking, abstraction

URL
Rok
2004
Strany
372–386
Časopis
Lecture Notes in Computer Science, roč. 2004, č. 3114, ISSN 0302-9743
Kniha
Computer Aided Verification
Vydavatel
Springer Verlag
Místo
Berlin
DOI
10.1007/978-3-540-27813-9_29
EID Scopus
2-s2.0-35048901593
BibTeX 
@article{BUT45718,
  author="Ahmed {Bouajjani} and Peter {Habermehl} and Tomáš {Vojnar}",
  title="Abstract Regular Model Checking",
  journal="Lecture Notes in Computer Science",
  year="2004",
  volume="2004",
  number="3114",
  pages="372--386",
  doi="10.1007/978-3-540-27813-9\{_}29",
  issn="0302-9743",
  url="http://www.fit.vutbr.cz/~vojnar/Publications/bhv-armc-04.ps.gz"
}
Projekty
Automatizované metody a nástroje pro vývoj spolehlivých paralelních a distribuovaných systémů, GAČR, Standardní projekty, GA102/04/0780, zahájení: 2004-01-01, ukončení: 2006-12-31, ukončen
Pokročilé metody automatické verifikace parametrických a nekonečně stavových systémů, GAČR, Postdoktorandské granty, GP102/03/D211, zahájení: 2003-09-01, ukončení: 2006-09-01, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru