Systematyczna analiza poprawności w wytwarzaniu bezpiecznego oprogramowania

• Autorzy: Szmuc T. , Rogus G.

Warianty tytułu

EN

Systematic correctness analysis in development of safety software

• Języki publikacji: PL

Abstrakty

PL

W artykule opisano zastosowanie języka formalnej specyfikacji LOTOS do wspomagania systematycznej analizy poprawności. Scharakteryzowano możliwości tego języka (tzw. style projektowe), jak również opisano koncepcję analizy poprawności. Przedstawiono również ramowe algorytmy analizy poprawności z wykorzystaniem pakietu CADP.

EN

An application of LOTOS formal specification language for systematic correctness verification support is described in the paper. Basic possibilities (the so-called design frameworks) of this language are described, as well as the correctness concept is discussed. General algorithms for the correctness analysis using CADP package are also described.

Słowa kluczowe

PL

poprawność oprogramowania; metody formalne; język LOTOS

EN

correctness of software; formal methods; LOTOS language

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2005
• Tom: R. 51, nr 9 bis
• Strony: 288--290
• Opis fizyczny: Bibliogr. 10 poz., rys., tab.

Twórcy

autor

Szmuc T.

• Akademia Górniczo-Hutnicza, Katedra Automatyki

autor

Rogus G.

• Akademia Górniczo-Hutnicza, Katedra Automatyki

Bibliografia

• [1] Braek R., Haugen O., Engineering Real Times Systems, Prentice Hall, 1993.
• [2] CADP, CAESAR/ALDEBARAN Development Package, http://www.inrialpcs.fr/vasy/vadp. html
• [3] Douglass B. P. Real Time UML Third Edition. Advances in the UMlL for Real-Time Systems. Addison-Wesley, 2004.
• [4] Fernandez J., Gavarel H., Kerbat A., CADP (CAESAR/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. Proceedings of The 8th Conference on Computer-Aided Verification, New Jersey USA 1996.
• [5] Gomaa H., Designing Concurrent, Distributed, and Real-Time Applications with UML, Addison-Wesley 2000.
• [6] Hoare C. A. R., Communicating Sequential Processes, Prentice Hall 1985.
• [7] ISO 8807 International Standard: Information Processing Systems - Open Systems Interconnection - LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behuvior-International Organization for Standarisation Geneve (E. Brinksma, cd.), 1989.
• [8] Milner R., Commtmication and Concurrency. Prectice Hall, 1989.
• [9] Rogus G., Zastosowanie jeżyka LOTOS do wspomagania wytwarzania poprawnego oprogramowania systemów reaktywnych. (Praca doktorska wykonana pod kierunkiem T. Szmuca),. Akademia Górniczo-Hutnicza 2005.
• [11] Szmuc T., Oskwarek S., Projektowanie poprawnego oprogramowania wspomagane formalizmem algebry procesów. Materiały V Krajowej Konferencji Naukowo-Technicznej Diagnostyka Procesów Przemysłowych, Łagów Lubuski 2001, 319-322.

Uwagi

Praca była wykonana w ramach grantu KBN .4T11C03524.: Zastosowanie metod formalnych do wspomagania wytwarzania poprawnego oprogramowania systemów czasu rzeczywistego