Jak zapewnić poprawności działania programów komputerowych?

• Autorzy: Greniewski M. J.

Warianty tytułu

EN

How to ensure the proper operation of computer programs?

• Języki publikacji: PL

Abstrakty

PL

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).

Słowa kluczowe

PL

jakość oprogramowania; walidacja; liniowa logika temporalna; diagram stanów; model kontroli

EN

software quality; validation; linear temporal logic; state diagram; model checking

• Wydawca: Oficyna Wydawnicza Europejskiej Uczelni
• Czasopismo: Studia i Materiały / Europejska Uczelnia Informatyczno-Ekonomiczna w Warszawie
• Rocznik: 2015
• Tom: Nr 2(10)
• Strony: 1--15
• Opis fizyczny: Bibliogr. 11 poz., rys.

Twórcy

autor

Greniewski M. J.

• Europejska Uczelnia Informatyczno-Ekonomiczna w Warszawie, ul. Białostocka 22, 03-741 Warszawa

Bibliografia

• [1] Ben-Ari Mordechai, Mathematical Logic for Computer Science – Third Edition, Springer Verlag, London, Heidenberg, New York, Dordrecht 2012.
• [2] Chellas Brian F., Modal Logic – an Introduction, Cambridge 1980.
• [3] Clarke Edmund M., Emerson E. Allen, Sifakis Joseph, Model Checking: Algorithmic Verification and Debugging, “Communications of the ACM”, Vol. 52, No. 11, November 2009, pages 74-84.
• [4] Hoare Charles Antony Richard, Communicating Sequential Processes, “Communications of the ACM”, Vol. 21, No. 8, 1978, pages 666-677.
• [5] Holzmann Gerard J., Basic SPIN Manual, http://www.spinroot.com.
• [6] Holzmann Gerard J., The SPIN Model Checker – Primer and Reference Manual, Addison-Wesley, Boston, San Francisco, New York, Toronto, Montreal, London, Munich, Paris, Madrid, Cape Town, Sydney, Tokyo, Singapore, Mexico City 2004.
• [7] Kozanecka Anna, O rodzajach logik temporalnych, „Roczniki Filozoficzne”, tom IV, nr 1, 2007.
• [8] Pnueli Amir, The temporal logic of programs, SFCS '77 Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46-57, IEEE Computer Society Washington, DC, USA 1977.
• [9] Prior Arthur Norman, Time and Modality (based on his 1956 John Locke lectures), Oxford University Press, 1957.
• [10] Tarski Alfred, A Lattice-Theoretical Fixpoint Theorem and Its Applications, Pacific J. Math. 5, 1955, pp. 285-309.
• [11] Trzesicki Kazimierz, Temporal Logic Model Checkers as Applied In Computer Science, “Studies In Logic, Grammar and Rhetoric” 17 (30) 2009.