Analysis of Parallel Discrete Systems: Persistent Sets vs. Concurrent Simulation

• Autorzy: Karatkevich A.
• Języki publikacji: EN

Abstrakty

EN

Formal verification is one of the necessary steps of the process of digital system design. Full exploration of state space presents a complete picture of system behaviour, but it is not practically possible for the large systems because of the so-called state explosion problem. That is the reason, why algorithms of partial state space exploration are important in practice. In this paper two basic methods of such exploration are described and compared: persistent set approach and concurrent simulation approach.

PL

Niezbędnym elementem procesu projektowania systemów cyfrowych jest formalna weryfikacja projektów. Ale pełna eksploracja przestrzeni stanów, dająca pełny obraz zachowania systemu, nie jest możliwa dla dużych współbieżnych systemów z powodu problemu eksplozji stanów. Dlatego ważne są algorytmy częściowej eksploracji przestrzeni stanów. Tematem artykułu jest opis i porównanie dwóch podstawowych metod takiej eksploracji: podejścia zbiorów uporczywych i współbieżnej symulacji.

Słowa kluczowe

EN

formal model; Petri nets

PL

systemy dyskretne; sieci Petriego

• Wydawca: Wydawnictwo SIGMA-NOT
• Czasopismo: Przegląd Elektrotechniczny
• Rocznik: 2009
• Tom: R. 85, nr 7
• Strony: 182--184
• Opis fizyczny: Bibliogr. 14 poz., rys., tab., schem.

Twórcy

autor

Karatkevich A.

• University of Zielona Góra, Institute of Komputer Engineering and Electronics, ul. Podgórna 50, 65-246 Zielona Góra,

Bibliografia

• [1] Adamski M., Węgrzyn M., Wolański P., A VHDL based approach to logic controllers design, Proc. of Int. Conference PDS, (1998), 9-16.
• [2] Godefroid P., Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, LNCS, 1032 (1996)
• [3] Valmari A., Stubborn Sets for Reduced State Space Generation, LNCS, 483 (1991), 491-515
• [4] Valmari A., State of the Art Report: Stubborn Sets, Petri Net Newsletter, 46 (1994), 6-14.
• [5] Valmari A., The State Explosion Problem, LNCS, 1491 (1998), 429-528
• [6] Karatkevich A., Properties and Analysis of ?-nets, Informatyka teoretyczna i stosowana, 5 (2003), 53-64
• [7] Karatkevich A., Dynamic Analysis of Petri Net-Based Discrete Systems, LNCIS, 356 (2007)
• [8] Karatkevich A., Adamski M., Węgrzyn M., Rapid Correctness Analysis for Sequential Function Chart, 45. Internationales Wissenschaftliches Kolloquium IWK, (2000), 679-684.
• [9] Karatkevich A., To Behavior Analysis of a Class of Petri Nets, 27th IFAC/IFIP/IEEE Workshop on Real-Time Programming WRTP, (2003), 33-38
• [10] Janicki R., Lauer P.E., Koutny M., Devillers R., Concurrent and Maximally Concurrent Evolution of Non-Sequential Systems, Theoretical Computer Science, 43 (1986), 213-238
• [11] Janicki R., Koutny M., Using Optimal Simulations to Reduce Reachability Graphs, Proceedings of the 2nd International Conference CAV’90, (1991) 166-175
• [12] Karatkevich A., Analysis of Parallel Discrete Systems: Persistent Sets and Concurrent Simulation, PAK, 6bis (2006), 20-22
• [13] Wasielewski P., System analizy sieci Petriego z wykorzystaniem symulacji współbieżnej, Praca dyplomowa, Uniwersytet Zielonogórski (2008)
• [14] Murata T., Petri Nets: Properties, Analysis and Applications, Proceedings of the IEEE, Vol.77, ? 4 (April 1989), 541-580