Logic in formal verification of computer systems. Some remarks

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.