Modelowanie i weryfikacja protokołu SCTP z wykorzystaniem automatów czasowych ze zmiennymi

• Autorzy: Męski A. , Półrola A.

Warianty tytułu

EN

Modelling and verification of the SCTP protocol using timed automata with discrete data

• Języki publikacji: PL

Abstrakty

PL

W pracy konstruujemy model protokołu SCTP (Stream Transmission Control Protocol) - protokołu transportowego zawierającego szereg mechanizmów mających zapewnić niezawodne dostarczanie. Do modelowania protokołu używamy automatów czasowych ze zmiennymi całkowitymi. Otrzymany model wykorzystywany jest następnie do automatycznej weryfikacji protokołu, podczas której testujemy własności wyrażone za pomocą formuł logiki temporalnej CTL (ang. Computation Tree Logic).

EN

In the paper we construct a model for SCTP (Stream Control Transmission Protocol) - a transport layer protocol which provides mechanisms of reliable delivery. The protocol is modelled by a set of timed automata augmented with integer variables. The resulting model is then used to test the protocol w.r.t. certain properties expressed by the formulas of the temporal logic CTL (Computation Tree Logic).

Słowa kluczowe

PL

model protokołu SCTP; weryfikacja protokołu; logika temporalna CTL; system tranzycyjny; automat czasowy ze zmiennymi całkowitymi; sieci ACZC

EN

Computational Tree Logic; Stream Transmission Control Protocol

• Wydawca: Wyższa Szkoła Informatyki i Umiejętności
• Czasopismo: Zeszyty Naukowe Wyższej Szkoły Informatyki
• Rocznik: 2008
• Tom: Vol. 7, Nr 1
• Strony: 49--67
• Opis fizyczny: Bibliogr. 5 poz., rys.

Twórcy

autor

Męski A.

autor

Półrola A.

• Wyższa Szkoła Informatyki w Łodzi

Bibliografia

• [1] Behrmann G., David A., Larsen K. G.: A Tutorial on Uppaal, 2004.
• [2] Clarke E. M., Emerson E. A., Sistla A. P.: Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, April 1986, pages 244-263.
• [3] Penczek W., Półrola A.: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. Springer-Verlag, 2006.
• [4] Stewart R., Xie Q., Morneault K., Sharp C., Schwarzbauer H.,.Taylor T, Rytina I., Kalla M., Zhang L., Paxson V.: Stream Control Transmission Protocol (RFC 2960), 2000.
• [5] Zbrzezny A., Półrola A.: SAT-Based Reachability Checking for Timed Automata with Discrete Data. Fundamenta Informaticae 79(3-4), str. 579-593, IOS Press, 2007