SAT-based Unbounded Model Checking of Timed Automata

• Autorzy: Penczek W. , Szreter M.
• Języki publikacji: EN

Abstrakty

EN

We present an improvement to the SAT-based Unbounded Model Checking (UMC, for short) algorithm [13]. Our idea consists in building blocking clauses of literals corresponding not only to propositional variables encoding states, but also to more general subformulas over these variables encoding sets of states. This way our approach alleviates an exponential blow-up in the number of blocking clauses. A hybrid algorithm for verifying Timed Automata is proposed, where the timed part of blocking clauses is computed using Difference Bound Matrices. The optimization results in a considerable reduction in the size and the number of generated blocking clauses, thus improving the overall performance. This is shown on the standard benchmark of Fischer's Mutual Exclusion protocol.

Słowa kluczowe

EN

Timed Automata; model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 425--440
• Opis fizyczny: bibliogr. 22 poz.

Twórcy

autor

Penczek W.

autor

Szreter M.

• Institute of Computer Science, Polish Academy of Science, Ordona 21, 01-237 Warsaw, Poland,

Bibliografia

• [1] P. A. Abdulla, P. Bjesse, and N. Eén. Symbolic reachability analysis based on SAT-solvers. In Proc. of the 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, pages 411-425. Springer-Verlag, 2000.
• [2] R. Alur and D. Dill. Automata-theoretic verification of real-time systems. In Formal Methods for Real-Time Computing, Trends in Software Series, pages 55-82. John Wiley & Sons, 1996.
• [3] G. Behrmann, K. G. Larsen, J. Pearson, C.Weise, andW. Yi. Efficient timed reachability analysis using Clock Difference Diagrams. In Proc. of the 11th Int. Conf. on Computer Aided Verification (CAV'99), volume 1633 of LNCS, pages 341-353. Springer-Verlag, 1999.
• [4] D. Beyer. Rabbit: Verification of real-time systems. In Proc. of the Workshop on Real-Time Tools (RTTOOLS'01), pages 13-21, 2001.
• [5] E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [6] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, and A. Zbrzezny. VerICS: A tool for verifying timed automata and Estelle specifications. 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 278-283. Springer-Verlag, 2003.
• [7] E. A. Emerson and E. Clarke. Characterizing correctness properties of parallel programs using fixpoints. In Proc. of the 7th Int. Colloquium on Automata, Languages and Programming (ICALP'80), volume 85 of LNCS, pages 169-181. Springer-Verlag, 1980.
• [8] M. Ganai, A. Gupta, and P. Ashar. Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In Proc. of the Int. Conf. on Computer-Aided Design (ICCAD'04), pages 510-517, 2004.
• [9] M. Kacprzak, A. Lomuscio, and W. Penczek. From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae, 63(2-3):221-240, 2004.
• [10] Magdalena Kacprzak, Alessio Lomuscio, Artur Niewiadomski, Wojciech Penczek, Franco Raimondi, and Maciej Szreter. Comparing bdd and sat based techniques for model checking chaum's dining cryptographers protocol. Fundam. Inform., 72(1-3):215-234, 2006.
• [11] W. Nabiałek M. Kacprzak, A. Niewiadomski, W. Penczek, M. Szreter A. Półrola, and B. Woźna. VerICS 2006: A model checker for real time and multi-agent systems. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), pages 345-356.Warsaw University, 2007.
• [12] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• [13] K. L. McMillan. Applying SAT methods in unbounded symbolic model checking. In Proc. of the 14th Int. Conf. on Computer Aided Verification (CAV'02), volume 2404 of LNCS, pages 250-264. Springer-Verlag, 2002.
• [14] J. Møller, J. Lichtenberg, H. Andersen, and H. Hulgaard. Difference Decision Diagrams. In Proc. of the 13th Int. Workshop Computer Science Logic (CSL'99), volume 1683 of LNCS, pages 111-125. Springer-Verlag, 1999.
• [15] W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, and M. Szreter. VerICS 2004: A model checker for real time and multi-agent systems. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'04), volume 170(1) of Informatik-Berichte, pages 88-99. Humboldt University, 2004.
• [16] 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.
• [17] P. Pettersson and K. G. Larsen. UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70:40-44, February 2000.
• [18] Mukul R. Prasad, Armin Biere, and Aarti Gupta. A survey of recent advances in sat-based formal verification. STTT, 7(2):156-173, 2005.
• [19] S. Seshia and R. Bryant. Unbounded, fully symbolic model checking of timed automata using boolean methods. In Proc. of the 15th Int. Conf. on Computer Aided Verification (CAV'03), volume 2725 of LNCS, pages 154-166. Springer-Verlag, 2003.
• [20] Maciej Szreter. SAT-based model checking of distributed systems. PhD thesis, Instytut Podstaw Informatyki PAN, 2006.
• [21] F. Wang. RED: Model checker for timed automata with clock-restriction diagram. In Proc. of the Int.Workshop on Real-Time Tools (RT-TOOLS'01), 2001.
• [22] B. Woźna. Ograniczona weryfikacja modelowa dla logik czasu rozgałęzionego: Szybka metoda falsyfikacji. PhD thesis, IPI PAN, June 2003. In Polish.