Zastosowanie algebry procesów do wspomagania projektowania poprawnego oprogramowania systemów reaktywnych

• Autorzy: Szmuc T. , Oskwarek S.

Warianty tytułu

EN

Process algebra supporting design of correct software for reactive systems

• Języki publikacji: PL

Abstrakty

PL

W pracy pokazano możliwość wspomagania analizy poprawności oprogramowania systemów reaktywnych. Pokazano translację między specyfikacją systemu w języku SDL (FSM) a algebrą procesów CCS oraz opisano koncepcję dowodzenia poprawności (bisymulacji). Rozważania prowadzone są na znanym w literaturze przykładzie systemu obronnego krążownika rakietowego.

EN

An application of process algebra (CCS) supporting design of correct software for reactive systems is presented in the paper. A translation between SDL (FSM) diagrams and process algebra is shown and a concept of correctness (bisimulation) proving is given. All the considerations are carried out using well-known Naval Vessel problem.

Słowa kluczowe

PL

oprogramowanie systemów reaktywnych; bisymulacja; SDL; CCS

EN

software for reactive systems; bisimulation; SDL; CCS

• Wydawca: Wydawnictwa AGH
• Czasopismo: Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
• Rocznik: 2001
• Tom: T. 5, z. 1/2
• Strony: 523--533
• Opis fizyczny: Bibliogr. 16 poz., rys.

Twórcy

autor

Szmuc T.

autor

Oskwarek S.

• Katedra Automatyki, Akademia Górniczo-Hutnicza w Krakowie

Bibliografia

• [1] Anders E.: Automatic Debugging of Communicating System Using SDT Validator. Telelogic AB
• [2] Bergstra J. A.: A Process Creation Mechanism in Process Algebra. Programming Research Group, University of Amsterdam 1995
• [3] Bradley S., Henderson W, Kendall D., Robson A.: Application-oriented real-time algebra. Software Engineering Journal, 9, 1994, 201-212
• [4] Braek R., Haugen O.: Engineering Real Time Systems. An object-oriented methodology using SDL. Prentice Hall 1993
• [5] Encyklopedia Techniki Wojskowej. Wydawnictwo Ministerstwa Obrony Narodowej 1987
• [6] Gordon S., Billington J.: Applying Coloured Petri Nets and Design/CPN to an Air-to-Air Missile Simulator. School of Physics and Electronic System Engineering, University of South Australia, Adelaide, SA5095
• [7] Jensen K.: Coloured Petri Nets - Basic Concepts. Analysis Methods and Practical Use-Volume 3. Springer Verlag 1997
• [8] Milner R.: Communication and Concurrency. Prectice Hall 1989
• [9] Moller F., Stevens P.: The Edinburgh Concurrency Workbench user manual (Version 7.1). Laboratory for Foundations of Computer Science, University of Edinburg 1999
• [10] Oskwarek S.: Rozwijanie poprawnego oprogramowania współbieżnego z zastosowaniem Języka SDL i algebry procesów. Kraków, AGH 1999 (praca magisterska)
• [11] Stamvik R.: Integrating SDT generated code with target platforms. Telelogic AB
• [12] Stirling C.: Bisimulation, Model Checking and Other Games. Department of Computer Science University of Edinburgh, Edinburgh EH9 3JZ, UK
• [13] SzmucT., SzwedP.: Towards Automatic Correctness Verification of Real-Time Programs. Applied Mathematics and Computer Science, 4,4,1994,643-660
• [14] Szmuc T.: Zaawansowane metody tworzenia oprogramowania czasu rzeczywistego. Kraków, Wydawnictwo CCATIE 1998
• [15] Szmuc T., Oskwarek S.: Projektowanie poprawnego oprogramowania czasu rzeczywistego wspomaganeformalizmem algebry procesów. Materiały VII Konferencji Systemy Czasu Rzeczywistego (red. T. Szmuc, R. Klimek), Kraków, 25-28 września 2000, 109-123
• [16] Telelogic AB: TelelogicSuite 4.1. Telelogic AB 2000