Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

1 2003

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: abstract models

Sortuj według:

Ogranicz wyniki do:

Reachability Analysis for Timed Automata Based on Partitioning

Półrola A., Penczek W., Szreter M.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

2003

Nr 961

1-23

Model checking is an approach commonly applied for automated verification of reachability properties. Given a system $S$ and a property $p$, reachability model checking consists in an exploration of the state space of $S$, checking whether there exists a state where $p$ holds. Since concrete state spaces (models) of timed systems are usually infinite, they cannot be directly applied to model checking. One of the solution to this problem is to exploit finite abstract models, preseving the properties of interest. The paper presents a new method of buildng abstract models for Timed Automata, based on a partitioning algorithm. Our pseudo-bisimulating models are often smaller than forward-reachability graphs , commonly used in reachability analysis. The method enables verification on-the-fly, i.e., generating of the model can be stopped as soon as a state satisfying $p$ is found.

Automatyczne testowanie osiągalności wykonywane jest zazwyczaj za pomocą metod weryfikacji modelowej. Dla danego systemy S i właściwości p polega ono na przejrzeniu przestrzeni stanów S i sprawdzeniu, czy zawiera ona stan w którym p zachodzi. Istotne znaczenie ma zatem rozmiar przeglądanej przestrzeni (modelu), który w wielu przypadkach (np. dla systemów z czasem) może być nawet nieskończony. Jednym z możliwych rozwiązań jest zastosowanie skończonych modeli abstrakcyjnych zachowujących żądane własności. Praca przedstawia nową metodę generowania modeli abstrakcyjnych dla automatów czasowych, bazujących na algorytmie minimalizacji (podziału). Otrzymywane modele pseudobisymulacyjne zachowują osiągalność, a przy tym są często mniejsze niż używane zwykle do jej testowania tzw. grafy forward-reachability. Metoda pozawala też na wykonywanie weryfikacji "w locie", tj. przerywanie budowania modelu gdy wygenerowany zostanie stan spełniający p.