| Identifikační kód |
RIV/00216224:14330/09:00029324 |
| Název v anglickém jazyce |
Efficient Large-Scale Model Checking |
| Druh |
D - Stať ve sborníku |
| Jazyk |
eng - angličtina |
| Obor - skupina |
I - Informatika |
| Obor |
IN - Informatika |
| Rok uplatnění |
2009 |
| Kód důvěrnosti údajů |
S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku |
3 |
| Počet tvůrců celkem |
4 |
| Počet domácích tvůrců |
2 |
| Výčet všech uvedených jednotlivých tvůrců |
Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792)
Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773)
Henri E. Bal (státní příslušnost: NL - Nizozemsko)
Kees Verstoep (státní příslušnost: NL - Nizozemsko) |
| Popis výsledku v anglickém jazyce |
Model checking is a popular technique to systematically and automatically verify system properties. Unfortunately, the well-known state explosion problem often limits the extent to which it can be applied to realistic specifications, due to the huge resulting memory requirements. Distributed-memory model checkers exist, but have thus far only been evaluated on small-scale clusters, with mixed results. We examine one well-known distributed model checker, DiVinE, in detail, and show how a number of additional optimizations in its runtime system enable it to efficiently check very demanding problem instances on a large-scale, multi-core compute cluster. We analyze the impact of the distributed algorithms employed, the problem instance characteristics andnetwork overhead. Finally, we show that the model checker can even obtain good performance in a high-bandwidth computational grid environment. |
| Klíčová slova oddělená středníkem |
model checking; distributed; parallel; large-scale |
| Stránka www, na které se nachází výsledek |
- |
| Odkaz na údaje z výzkumu |
- |