Wytwarzanie oprogramowania czasu rzeczywistego wspomagane metodą formalną: SDL - kolorowane sieci Petriego

• Autorzy: Szmuc W.

Warianty tytułu

EN

Development of real-time software supported by formal method: SDL - colored Petri nets

• Języki publikacji: PL

Abstrakty

PL

Referat pokazuje zasady przekształcania diagramów języka SDL na kolorowane sieci Petriego. Przedstawiono algorytm konwersji umożliwiający tłumaczenie konstrukcji obiektowych. Zachowuje on hierarchię diagramów SDL, co powoduje dużą (na ile to możliwe) czytelność sieci wynikowych. Zastosowanie takiej konwersji umożliwia wspomaganie wytwarzania poprawnego oprogramowania, przez formalną weryfikację poprawności produktu w poszczególnych fazach. Metoda konwersji diagramów SDL na sieci Petriego została opracowana na podstawie przekształcenia przykładowego systemu zdalnej rejestracji przejazdów autostradą. W artykule przedstawiono jedynie przykłady konwersji pewnych charakterystycznych konstrukcji, zastosowanych w wyżej wspomnianym systemie (nie przedstawiono samego systemu). Sam algorytm jest rozwinięciem opracowanej wcześniej metody konwersji diagramów SDL na sieci Petriego. Polega ono na dodaniu mechanizmów hierarchizacji sieci, co z kolei umożliwia łatwe przekształcanie konstrukcji obiektowych. Algorytm nie umożliwia jednak pełnego tłumaczenia diagramów SDL ze względu na brak możliwości konwersji struktur danych oraz algorytmów przetwarzania danych (dotyczy jedynie dynamiki systemu). W artykule wspomniano również o niektórych metodach sprawdzania własności oprogramowania wykorzystujących sieci Petriego oraz narzędziach wspomagających wykonanie tych operacji.

EN

Growing complexity of software forces improvement of design tools. Real-time systems usually are developed in SDL. Unfortunately this tool cannot prove some system features that have to be met in family of real-time systems. The article proposes solution that can be used to at least minimize this kind of disadvantages. The paper describes an algorithm for conversion of SDL diagrams into Petri nets. Application of hierarchical nets enables translation of objects constructions and keeps clarity (as it is possible). This solution helps in design of proper software by formal verification of product correctness in individual phases. The algorithm is result of experience gained in transformation of example system of remote registration of motorway users. The article presents only examples of some characteristic constructions conversion used in the system (not described). The algorithm is expansion of earlier proposed conversion method of SDL diagram into Petri nets. The improvement lies in application of hierarchy constructs, which makes translation of object constructs easier. The algorithm is focused on behavioral view of system, doesn't deals with translation of data structures and constructions associated with them. The paper mentions also some methods for checking of software properties using Petri nets. Tools supporting the checking are shortly described too.

Słowa kluczowe

PL

oprogramowanie; czas rzeczywisty; SDL; sieci Petriego

EN

software; real-time; SDL; Petri nets

• Wydawca: Wydawnictwa AGH
• Czasopismo: Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie
• Rocznik: 2003
• Tom: T. 7, z. 1-2
• Strony: 267--273
• Opis fizyczny: Bibliogr. 8 poz.

Twórcy

autor

Szmuc W.

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

Bibliografia

• [1] Ellsberger J., Hogrefe D., Sarma A.: SDL Formal Object-Oriented Language for Communicating Systems. Prentice Hall Europe 1997
• [2] Jensen K..: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Springer Verlag 1996 (tom I i II), 1997 (tom III)
• [3] Meta Softwere Corporation: Design/CPN Reference Manual for X-Windows
• [4] Starke P.H., Roch S.: INA - Integrated Net Analyzer Version 2.2 - Manual. Berlin, 1!
• [5] Suraj Z., Komarek B.: GRAPH-system graficznej konstrukcji i analizy sieci Petriego Akademicka Oficyna Wydawnicza PLJ 1994
• [6] Szmuc T.: Zaawansowane metody tworzenia oprogramowania systemów czasu rzeczywistego. Wydawnictwo CCATIE, 15, 1998
• [7] Szmuc W.: Zastosowanie kolorowanych sieci Petriego do modelowania i analizy diagramów stanów w języku SDL. Kraków, 2001 (praca magisterska pod kier. dr. inż. R. Klimka)
• [8] Telelogic AB: SDL Suite 4.1 Methodology Guidelines. Telelogic AB, 2000