Narasta problem skutków błędów w oprogramowaniu. Konieczna stała się zmiana podejścia – zapewnienie poprawności działania programów komputerowych. Dotyczy to głównie programów współbienych – reaktywnych. Metody formalne pozwalają na zastąpienie metody testowania programów (o wątpliwej skuteczności) metodami walidacji, czyli dowodzenia poprawności działania przez sprawdzanie stanów osiagąnych przez model sterowania programu. Podstawą jest pomysł użycia logiki temporalnej do opisu działania programów współbiernych Amira Pnueli z 1977 roku, który został rozwinięty na początku lat osiemdziesiątych ubiegłego wieku w teorie przez Clarke’a, Emersona oraz Sifakisa (uhonorowani w 2007 r. ACM A.M. Turing Award). Wzmiankowana teorie zastosowano w języku modelowania Promela oraz procesorze Spin (Simple Promela Interpreter) autorstwa zespołu Gerarda J. Holzmanna (uhonorowanego w 2002 r. ACM Software System Award).
EN
There is a growing tendency of the effects of bugs in the software. It becomes necessary to change the approach – to ensure proper operation of computer programs. This applies mainly to concurrent programs – reactive ones. Formal methods allow substitution of the method of testing programs (of dubious efficacy) by validation methods, which is proving the correctness of the action – by checking the status achieved by the control model program. The basis is the idea of using temporal logic to describe the actions of concurrent programs by Amir Pnueli from 1977, further developed in the early eighties of the last century into the theory of Clarke, Emerson and Sifakis (honored in 2007 ACM A.M. Turing Award). The theory mentioned above, was used in modeling language Promela and Spin processor (Simple Promela Interpreter) by Gerard J. Holzmann team (which won the 2002 ACM Software System Award).
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.