- Tytuł:
-
Logic in formal verification of computer systems. Some remarks
Logika i formalna weryfikacja systemów komputerowych. Kilka uwag - Autorzy:
- Trzęsicki, K.
- Powiązania:
- https://bibliotekanauki.pl/articles/341099.pdf
- Data publikacji:
- 2009
- Wydawca:
- Politechnika Białostocka. Oficyna Wydawnicza Politechniki Białostockiej
- Tematy:
-
logika
weryfikacja
metoda teorio-dowodowa
sprawdzanie za pomocą modelu
logic
verification
proof-theoretical method
model checking - Opis:
-
Various logics are applied to specification and verification of both hardware and software systems. The problem with finding of proof is the most important disadvantage of proof-theoretical method. The proof-theoretical method presupposes the axiomatization of the logic. Proprieties of a system can also be checked using a model of the system. A model is constructed with the specification language and checked using automatic model checkers. The model checking application presupposes the decidability of the task.
Do specyfikacji i weryfikacji zarówno sprzętu jak i programów stosowane są różne logiki. Główną wadą metody teorio-dowodowej weryfikacji jest problem znalezienia dowodu. Zastosowanie tej metody zakłada aksjomatyzację logiki. Własności systemu mogą być sprawdzane za pomocą jego modelu. Model jest zbudowany w języku specyfikacji i sprawdzany automatycznie. Zastosowanie sprawdzania za pomocą modelu zakłada rozstrzygalność zadania. Istnieje wielka różnorodność programów (model checker) do sprawdzania własności za pomocą modeli. - Źródło:
-
Zeszyty Naukowe Politechniki Białostockiej. Informatyka; 2009, 4; 151-175
1644-0331 - Pojawia się w:
- Zeszyty Naukowe Politechniki Białostockiej. Informatyka
- Dostawca treści:
- Biblioteka Nauki
Artykuł