SAT-Based Bounded Model Checking for the Universal Fragment of TCTL

• Autorzy: Penczek W. , Woźna B. , Zbrzezny A.
• Języki publikacji: EN

Abstrakty

EN

Bounded Model Checking (BMC) based on SAT methods consists in searching for a counterexample of a particular length and to generate a propositional formula that is satisfiable iff such a counterexample exists. Our paper shows how the concept of bounded model checking can be extended to deal with \TACTL\ (the universal fragment of \TCTL ) properties of a network of concurrent Timed Automata.

PL

Ograniczona Weryfikacja Modelowa, bzaująca na metodach SAT, polega na poszukiwaniu kontrprzykładów o długości ograniczonej przez pewną liczbę całkowitą k > 0 oraz generowanie formuły zdaniowej, która jest spełniana wtedy i tylko wtedy, gdy taki kontrprzykład istnieje. Celem tej pracy jest przedstawienie koncepcji ograniczonej weryfikacji modelowej dla automatów czasowych reprezentowanych przez siec współbieżnych i wzajemnie komunikujących się komponentów oraz własności wyrażanych w języku logiki TACTL (uniwersalnego fragmentu TCTL).

Słowa kluczowe

EN

bounded model checking; logic TACTL (TECTL); bounded semantics; translation to SAT; Timed Automata; Region Graphs; discretization; system verification

PL

ograniczona weryfikacja modelowa; logika TACTL (TECTL); ograniczona semantyka; translacja do SAT; automat czasowy; graf regionów; dyskretyzacja; system weryfikacyjny

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2002
• Tom: Nr 947
• Strony: 1--26
• Opis fizyczny: Bibliogr. 38 poz.

Twórcy

autor

Penczek W.

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

autor

Woźna B.

• Institute of Mathematics and Computer Science, PU Armii Krajowej 13/15, 42-200 Częstochowa, Poland

autor

Zbrzezny A.

• Institute of Mathematics and Computer Science, PU Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• E. Asaxin, M. Bozga, A. Kerbrat, 0. Maler, A. Pnueli, and A. Rasse. Data-structures for the verification of Timed Automata. In Proc. of Int. Workshop on Hybrid and Real-Time Systems (HART’97), volume 1201 of LNCS, pages 346-360. Springer-Verlag, 1997.
• R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. An implementation of three algo¬rithms for timing verification based on automata emptiness. In Proc. of the 13th IEEE Real-Time Systems Symposium (RTSS’92), pages 157-166. IEEE Comp. Soc. Press, 1992.
• R. Alur, C. Courcoubetis, D. Dill, N. Halbwachs, and H. Wong-Toi. Minimization of timed transition systems. In Proc. of CONCUR’92, volume 630 of LNCS, pages 340-354. Springer-Verlag, 1992.
• R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(l).-2-34, 1993.
• R. Alur and D. Dill. A theory of Timed Automata. Theoretical Computer Science, 126(2):183 - 235, 1994. R. Alur, T. Feder, and T. Henzinger. The benefits of relaxing punctuality. Journal of the ACM, 43(1):116—146, 1996.
• A. Biere, A. Cimatti, E. Clarke, M.Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. of ACM/IEEE Design Automation Conference (DAC’99), pages 317-320, 1999.
• A. Biere, A. Cimatti, E. Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS’99, volume 1579 of LNCS, pages 193-207. Springer-Verlag, 1999.
• J. Bengtsson, B. Jonsson, J. Lilius, and W. Yi. Partial order reductions for timed systems. In Proc. of CONCUR’98, volume 1466 of LNCS, pages 485-500. Springer-Verlag, 1998.
• R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers, 35(8):677—691, 1986.
• A. Bouajjani, S. Tripakis, and S. Yovine. On-the-fly symbolic model checking for real-time systems. In Proc. of the 18th IEEE Real-Time Systems Symposium (RTSS’97), pages 232 - 243. IEEE Comp. Soc. Press, 1997. E. Clarke, A. Biere, R. Raimi, and Y. Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(l):7-34, 2001.
• E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*. In Proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET’94)- Elsevier Science Publishers, 1994.
• D. Dams, R. Gerth, B. Knaack, and R. Kuiper. Partial-order reduction techniques for real-time model checking. In Proc. of the 3rd Int. Workshop on Formal Methods for Industrial Critical Systems, pages 157 - 169, 1998.
• C.Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. of TACAS’98, volume 1384 of LNCS, pages 313-329. Springer-Verlag, 1998.
• E.A. Emerson and E. M. Clarke. Using branching-time temporal logic to synthesize synchronization skele¬tons. Science of Computer Programming, 2(3):241-266, 1982.
• R. H. Eckhouse. Minicomputer Systems. Organization and Programming. Prentice-Hall, 1975.
• E. A. Emerson. Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter Temporal and Modal Logic, pages 995-1067. Elsevier, 1990.
• E.A. Emerson and A. P. Sistla. Symmetry and model checking. Formal Methods in System Design, 9:105-131, 1995.
• O. Grumberg and D. E. Long. Model checking and modular verification. In Proc. of CONCUR’91, volume 527 of LNCS, pages 250-265. Springer-Verlag, 1991.
• K. Heljanko and I. Niemela. Bounded LTL model checking with stable models. In Proc. of the 6th Int. Conf. on Logic Programming and Nonmonotonic Reasoning (LPNMR’2001), volume 2173 of LNCS, pages 200-212. Springer-Verlag, 2001.
• D.S. Johnson and M. A. Trick, editors. Cliques, Coloring and Satisfiability: The Second DIMACS Implementation Challenge, volume 26 of ACM/AMS DIMACS Series. Amer. Math. Soc., 1996.
• O. Kupferman, T. A. Henzinger, and M. Y. Vardi. A space-efficient on-the-fly algorithm for real-time model checking. In Proc. of CONCJJR’96, volume 1119 of LNCS, pages 514-529. Springer-Verlag, 1996.
• I. Kang and I. Lee. An efficient state space generation for the analysis of real-time systems. In Proc. of Int. Symposium on Software Testing and Analysis, 1996.
• J. Lilius. Efficient state space search for Time Petri Nets. In Proc. of MFCS Workshop on Concurrency, Brno’98, volume 18 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 1999. [McM93] K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.
• M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference (DAC01), pages 530-535, June 2001.
• F. Pagani. Partial orders and verification of real-time systems. In Proc. of the 4th Int. Symp. on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT’96), volume 1135 of LNCS, pages 327-346. Springer-Verlag, 1996.
• D. Peled. Partial order reduction: Linear and branching temporal logics and process algebras. In Proc. of Partial Order Methods in Verification (POMIV’96), volume 29 of ACM/AMS DIMACS Series, pages 79-88. Amer. Math. Soc., 1996.
• W. Penczek and A. Półrola. Abstractions and partial order reductions for checking branching properties of Time Petri Nets. In Proc. of the Int. Conf. on Applications and Theory of Petri Nets (ICATPN’01), volume 2075 of LNCS, pages 323-342. Springer-Verlag, 2001.
• W. Penczek, M. Szreter, Ft. Gerth, and R. Kuiper. Improving partial order reductions for universal branching time properties. Fundamenta Informaticae, 43:245-267, 2000.
• W. Penczek and B. Woźna. Towards bounded model checking for Timed Automata. In Proc. of the Int. Workshop on Concurrency Specification and Programming (CS&P’Ol), pages 195-209, 2001.
• W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, June 2002.
• W. Penczek, B. Woźna, and A. Zbrzezny. Branching time bounded model checking for elementary net systems. Technical Report 940, ICS PAS, Ordona 21, 01 - 237 Warsaw, January 2002.
• 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.
• S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(l):25-68, 2001.
• P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In Proc. of CONCUR’93, volume 715 of LNCS, pages 233-246. Springer-Verlag, 1993.
• B. Woźna, W. Penczek, and A. Zbrzezny. Reachability for timed systems based on SAT-solvers. In Proc. of the Int. Workshop on Concurrency Specification and Programming (CS&P'02), Informatik-Berichte. Humboldt University, 2002. to appear.
• T. Yoneda and B.H. Schlingloff. Efficient verification of parallel real-time systems. Formal Methods in System Design, 11(2):197-215, 1997.
• L. Zhang. ZchaiT. http://www.ee.princeton.edu/~chaff/zchaff.php, 2001.
• L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In Proc. of Int. Conf. on Computer-Aided Design (ICCAD’01), pages 279-285, 2001.