Bounded Parametric Verification for Distributed Time Petri Nets with Discrete-Time Semantics

• Autorzy: Knapik M. , Penczek W. , Szreter M. , Półrola A.
• Języki publikacji: EN

Abstrakty

EN

Bounded Model Checking (BMC) is an efficient technique applicable to verification of temporal properties of (timed) distributed systems. In this paper we show for the first time how to apply BMC to parametric verification of time Petri nets with discrete-time semantics. The properties are expressed by formulas of the logic PRTECTL - a parametric extension of the existential fragment of Computation Tree Logic (CTL).

Słowa kluczowe

EN

Computation Tree Logic (CTL); bounded model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 101, nr 1/2
• Strony: 9--27
• Opis fizyczny: Bibliogr. 31 poz., tab.

Twórcy

autor

Knapik M.

autor

Penczek W.

autor

Szreter M.

autor

Półrola A.

• Polish Academy of Sciences, ICS Ordona 21, 01-237 Warsaw, Poland,

Bibliografia

• [1] R. Alur, T. Henzinger, and M. Vardi. Parametric real-time reasoning. In Proc. of the 25th Ann. Symp. On Theory of Computing (STOC'93), pages 592-601. ACM, 1993.
• [2] G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani. Bounded model checking for timed systems. In Proc. of the 22nd Int. Conf. on Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of LNCS, pages 243-259. Springer-Verlag, 2002.
• [3] M. Benedetti and A. Cimatti. Bounded model checking for Past LTL. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 18-33. Springer-Verlag, 2003.
• [4] A. Biere, A. Cimatti, E. Clarke, M.Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. of the ACM/IEEE Design Automation Conference (DAC'99), pages 317-320, 1999.
• [5] V. Bruyére, E. Dall'Olio, and J-F. Raskin. Durations and parametric model-checking in timed automata. ACM Transactions on Computational Logic, 9(2), 2008.
• [6] G. Bucci, A. Fedeli, L. Sassoli, and E. Vicaro. Modeling flexible real time systems with preemptive time Petri nets. In Proc. of the 15th Euromicro Conference on Real-Time Systems (ECRTS'03), pages 279-286. IEEE Computer Society, 2003.
• [7] G. Bucci and E. Vicaro. Compositional validation of time-critical systems using communicating time Petri nets. IEEE Trans. on Software Eng., 21(12):969-992, 1995.
• [8] E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7-34, 2001.
• [9] E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [10] E. A. Emerson and E. Clarke. Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241-266, 1982.
• [11] E. A. Emerson and R. Trefler. Parametric quantitative temporal reasoning. In Proc. of the 14th Symp. On Logic in Computer Science (LICS'99), pages 336-343. IEEE Computer Society, July 1999.
• [12] K. Heljanko. Bounded reachability checking with process semantics. In Proc. of the 12th Int. Conf. On Concurrency Theory (CONCUR'01), volume 2154 of LNCS, pages 218-232. Springer-Verlag, 2001.
• [13] T. Hune, J. Romijn,M. Stoelinga, and F. Vaandrager. Linear parametricmodel checking of timed automata. In Proc. of the 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), volume 2031 of LNCS, pages 189-203. Springer-Verlag, 2001.
• [14] R. Janicki. Nets, sequential components and concurrency relations. Theoretical Computer Science, 29:87-121, 1984.
• [15] M. Knapik, W. Penczek, and M. Szreter. Bounded parametric model checking for elementary net systems. In Proc. of Int. Workshop on Petri Nets and Software Engineering (PNSE'09), pages 97-117. University of Hamburg, 2009.
• [16] R. Mascarenhas, D. Karumuri, U. Buy, and R. Kenyon. Modeling and analysis of a virtual reality system with time Petri nets. In Proc. of the 20th Int. Conf. on Software Engineering (ICSE'98), pages 33-42. IEEE Computer Society, 1998.
• [17] P. Merlin and D. J. Farber. Recoverability of communication protocols - implication of a theoretical study. IEEE Trans. on Communications, 24(9):1036-1043, 1976.
• [18] D. Peled. All from one, one for all: On model checking using representatives. In Proc. of the 5th Int. Conf. on Computer Aided Verification (CAV'93), volume 697 of LNCS, pages 409-423. Springer-Verlag, 1993.
• [19] W. Penczek and A. Półrola. Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach, volume 20 of Studies in Computational Intelligence. Springer-Verlag, 2006.
• [20] W. Penczek, A. Półrola, and A. Zbrzezny. SAT-based (parametric) reachability for distributed time Petri nets. In Proc. of the Int. Workshop on Petri Nets and Software Engineering (PNSE'09), pages 133-154. University of Hamburg, 2009.
• [21] W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, 2002.
• [22] W. Penczek, B. Woźna, and A. Zbrzezny. Towards bounded model checking for the universal fragment of TCTL. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of LNCS, pages 265-288. Springer-Verlag, 2002.
• [23] A. Półrola and W. Penczek. Minimization algorithms for time Petri nets. Fundamenta Informaticae, 60(1-4):307-331, 2004.
• [24] L. Popova. On time Petri nets. Elektronische Informationsverarbeitung und Kybernetik, 27(4):227-244,1991.
• [25] L. Popova-Zeugmann. Time Petri nets state space reduction using dynamic programming. Journal of Control and Cybernetics, 35(3):721-748, 2006.
• [26] J-F. Raskin and V. Bruyère. Real-time model checking: Parameters everywhere. In Proc. of the 23rd Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'03), volume 2914 of LNCS, pages 100-111. Springer-Verlag, 2003.
• [27] O. Strichman. Tuning SAT checkers for boundedmodel checking. In Proc. of the 12th Int. Conf. on Computer Aided Verification (CAV'00), volume 1855 of LNCS, pages 480-494. Springer-Verlag, 2000.
• [28] B. Woźna. ACTL_ properties and bounded model checking. Fundamenta Informaticae, 63(1):65-87, 2004.
• [29] B. Woźna, A. Zbrzezny, and W. Penczek. Checking reachability properties for timed automata via SAT. Fundamenta Informaticae, 55(2):223-241, 2003.
• [30] A. Zbrzezny. Improvements in SAT-based reachability analysis for timed automata. Fundamenta Informaticae, 60(1-4):417-434, 2004.
• [31] A. Zbrzezny. Improving the translation from ECTL to SAT. Fundamenta Informaticae, 85(1-4):513-531, 2008.