External Memory LTL Model Checking

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F09%3A00047049" target="_blank" >RIV/00216224:14330/09:00047049 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

External Memory LTL Model Checking

Popis výsledku v původním jazyce

Model checking is an increasingly popular method for formal verification of safety-critical systems. This thesis is focused on fighting state explosion (the well-known problem in model checking) by employing external memory, which can have by orders of magnitude larger capacity than internal memory. For computations, probably the most proper external memory device is hard disk. It has a sufficient speed and capacity for a low price. As a drawback, hard disks suffer from long access times, which means than data must be read by blocks in order to preserve a sufficient transfer rate. Therefore, model checking algorithms must be re-designed to behave efficiently w.r.t. the number of performed I/O operations when a substantial part of a state space is stored on disk. The thesis offers I/O-efficient solutions to the two well-known model checking problems --- reachability analysis and LTL model checking. All newly designed algorithms have been implemented, thoroughly experimentally evaluated

Název v anglickém jazyce

External Memory LTL Model Checking

Popis výsledku anglicky

Model checking is an increasingly popular method for formal verification of safety-critical systems. This thesis is focused on fighting state explosion (the well-known problem in model checking) by employing external memory, which can have by orders of magnitude larger capacity than internal memory. For computations, probably the most proper external memory device is hard disk. It has a sufficient speed and capacity for a low price. As a drawback, hard disks suffer from long access times, which means than data must be read by blocks in order to preserve a sufficient transfer rate. Therefore, model checking algorithms must be re-designed to behave efficiently w.r.t. the number of performed I/O operations when a substantial part of a state space is stored on disk. The thesis offers I/O-efficient solutions to the two well-known model checking problems --- reachability analysis and LTL model checking. All newly designed algorithms have been implemented, thoroughly experimentally evaluated

Druh

O - Ostatní výsledky

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2009

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů