Reaching the limits for Bounded Model Checking

• Autorzy: Woźna, B.

Warianty tytułu

PL

Osiągnięcie granicy rozszerzalności metody ograniczonej weryfikacji modelowej

• Języki publikacji: EN

Abstrakty

EN

The main contribution of the paper consists in showing that the BMC method is feasible for ACTL* (the universal fragment of CTL*) which subsumes both ACTL and LTL. The extension to ACTL* is obtained by redefining the function returning the sufficient number of executions over which an ACTL* formula is checked, and then by combining two known translations to SAT for ACTL and LTL formulas. The proposed translation of ACTL* formulas is essentially different from the existing translations of both ACTL and LTL formulas. Moreover, ACTL* seems to be the largest set of temporal properties which can be verified by means of BMC. We have implemented our new BMC algorithm for discrete timed automata and we have presented a preliminary experimental results, which prove the efficiency of the method. The formal treatment is the basis for the implementation of the technique in the symbolic model checker VerICS.

PL

Osiągnięcie granicy rozszerzalności metody ograniczonej weryfikacji modelowej. Głównym celem tej pracy jest wykazanie, że metoda ograniczonej weryfikacji modelowej (OWM) jest rozszerzalna do własności wyrażalnych w ACTL* (uniwersalnym fragmencie logiki CTL*), języku który zawiera zarówno ACTL i LTL. Rozszerzenie metody OWM do ACTL* polega na przedefiniowaniu funkcji zwracającej wystarczającą liczbę wykonań systemu, w zbiorze których formuła ACTL* jest sprawdzana, a następnie na zdefiniowaniu translacji będącej kombinacją translacji formuł LTL i ACTL. Zaproponowana translacja formuł ACTL* istotnie różni się od tych istniejących dla LTL i ACTL oraz wydaje się, że język ACTL* jest największym zbiorem własności temporalnych, które mogą być weryfikowane za pomocą metody OWM. Nasz nowy algorytm został zaimplementowany dla elementarnych sieci Petriego oraz dla dyskretnych automatów czasowych, a uzyskane wstępne wyniki eksperymentalne dowodzą efektywności naszej metody. Ponadto, zaproponowana translacja i wykonana implementacja będzie bazą dla nowego modułu w symbolicznym weryfikatorze Öerics.

Słowa kluczowe

PL

ograniczona weryfikacja modelowa; logika TACTL (TECTL); ograniczona semantyka; translacja do SAT; dyskretny automat czasowy; model konkretny; model abstrakcyjny; model zdyskretyzowany; system weryfikacyjny

EN

bounded model checking; logic TACTL (TECTL); bounded semantics; translation to SAT; Discrete Timed Automata; concrete model; discretize model; abstract model; system verification

• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2003
• Tom: Nr 958
• Strony: 1-25
• Opis fizyczny: Bibliogr. 35 poz., rys.

Twórcy

autor

Woźna, B.

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

Bibliografia

• [ACD93] R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(1): 2—34, 1993.
• [ACKS02] 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.
• [BC03] M. Benedetti and Alessandro Cimatti. Bounded model checking for past ltl. In Proc. of TACAS’03, volume 2619 of LNCS, pages -. Springer-Verlag, 2003.
• [BCC+99] 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.
• [BCCZ99] A. Biere, A. Cimatti, E. Claxke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. of TACAS’99, volume 1579 of LNCS, pages 193-207. Springer-Verlag, 1999.
• [Bey02] D. Beyer. Improvements in BDD-based reachability analysis of Timed Automata. In Proc. of Int. Symp. Of Formal Methods Europe (FME’01), volume 2021 of LNCS, pages 318-343. Springer-Verlag, 2002.
• [BJLY98] J. Bengtsson, B. Jonsson, J. Lilius, and W. Yi. Partial order reductions for timed systems. In Proc. of the Int. Conf. on Concurrency Theory (CONCUR’98), volume 1466 of LNCS, pages 485-500. Springer-Verlag, 1998.
• [BMT99] M. Bozga, O. Maler, and S. Tripakis. Efficient verification of Timed Automata using dense and discrete time semantics. In Proc. of the Conf. on Correct Hardware Design and Verification Methods (CHARME’99), 1999.
• [CBRZ01] 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.
• [CGP99] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999.
• [DGG94] 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.
• [DJJ+03] 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.
• [dMRS02] L. de Moura, H. Rueil, and M. Sorea. Lazy theorem proving for bounded model checking over infinite domains. In Proc. of the 18th Int. Conf. on Automated Deduction (CADE’02), volume 2392 of LNCS. Springer-Verlag, 2002. to appear.
• [DT98] C. Daws and S. Tripakis. Model checking of real-time reachability properties using abstractions. In Proc. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), volume 1384 of LNCS, pages 313-329. Springer-Verlag, 1998.
• [EL85] E. A. Emerson and C. L. Lei. Modalities for model checking: Branching time logic strikes back. In Proc. of the 12th ACM Symp. on Principles of Programming Languages, pages 84-96, January 1985.
• [ES95] E. A. Emerson and A. P. Sistla. Symmetry and model checking. Formal Methods in System Design, 9:105-131, 1995.
• [GL91] O. Grumberg and D. E. Long. Model checking and modular verification. In Proc. of the Int. Conf. on Concurrency Theory (CONCUR’91), volume 527 of LNCS, pages 250-265. Springer-Verlag, 1991.
• [HelOl] K. Heljanko. Bounded reachability checking with process semantics. In Proc. of the Int. Conf. on Concurrency Theory (CONCUR’01), volume 2154 of LNCS, pages 218-232. Springer-Verlag, 2001.
• [HN01] 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.
• [JT96] 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.
• [McM93] K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.
• [MMZ+01] 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.
• [MP] O. Maler and A. Pnueli. Timing analysis of asynchronous circuits using timed automata. In Proc. of CHARME’95, volume 987 of LNCS, pages 189-205. Springer-Verlag.
• [NMA+02] P. Niebert, M. Mahfoudh, E. Asarin, M. Bozga, O. Maler, and N. Jain. Verification of Timed Automata via Satisfiability Checking. In Proc. of the 7th Int. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), volume 2469 of LNCS, pages 226-243. Springer-Verlag, 2002.
• [Pag96] 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.
• [Pel96] 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.
• [PP01] 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.
• [PSGK00] W. Penczek, M. Szreter, R. Gerth, and R. Kuiper. Improving partial order reductions for universal branching time properties. Fundamenta Informaticae, 43:245-267, 2000.
• [PWZ02a] 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.
• [PWZ02b] W. Penczek, B. Woźna, and A. Zbrzezny. SAT-Based Bounded Model Checking for the Universal Fragment of TCTL. Technical Report 947, ICS PAS, Ordona 21, 01 - 237 Warsaw, September 2002.
• [PWZ02c] 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.
• [Sor02] Maria Sorea. Bounded model checking for timed automata. In Proc. of the Third Workshop on Models for Time-Critical Systems (MTCS’02); affiliated with CONCUR 2002., volume 68(5) of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2002.
• [TY01] S. Tripakis and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 1S(1):25—68, 2001.
• [WG93] 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.
• [WPZ02] 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’OZ), volume II of Informatik-Berichte Nr 161, pages 380-395. Humboldt University, 2002.