SMT-based reachability analysis for simply-timed systems

• Autorzy: Zbrzezny A. M. , Zbrzezny A.

Identyfikatory

DOI

dx.doi.org/10.16926/m.2015.20.09

• Języki publikacji: EN

Abstrakty

EN

In the paper we present Satisfiability Modulo Theory based (SMT-based) reachability analysis algorithm for Simply-Timed Systems (i.e., Kripke structures where each transition holds a duration, which is an arbitrary natural number) generated by simply-timed automata. The algorithm is based on a SMT-based encoding for Simply-Timed Systems. We have tested the algorithm in question by using the generic simply timed pipeline paradigm model as the benchmark. The performance evaluation of the algorithm is given by means of the running time and the memory used.

Słowa kluczowe

EN

reachability analysis; SMT; time systems

PL

analiza osiągalności; SMT; systemy czasowe

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2015
• Tom: Vol. 20
• Strony: 83--92
• Opis fizyczny: Bibliogr. 26 poz., rys.

Twórcy

autor

Zbrzezny A. M.

• Jan Długosz University in Czestochowa Institute of Mathematics and Computer Science al. Armii Krajowej 13/15, 42-200 Czestochowa, Poland

autor

Zbrzezny A.

• Jan Długosz University in Czestochowa Institute of Mathematics and Computer Science al. Armii Krajowej 13/15, 42-200 Czestochowa, Poland

Bibliografia

• [1] R. Alur. Timed Automata. In Proceedings of the 11th International Conference on Computer Aided Verification (CAV’99), volume 1633 of LNCS, pages 8-22. Springer-Verlag, 1999.
• [2] R. Alur, C. Courcoubetis, and D. Dill. Model checking for real-time systems. In Proceedings of the 5th Symp. on Logic in Computer Science (LICS’90), pages 414-425. IEEE Computer Society, 1990.
• [3] R. Alur, C. Courcoubetis, and D. Dill. Model checking in dense real-time. Information and Computation, 104(1):2-34, 1993.
• [4] 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.
• [5] Alessandro Armando, Claudio Castellini, and Enrico Giunchiglia. SAT-based procedures for temporal reasoning. In ECP, pages 97-108, 1999.
• [6] Alessandro Armando and Enrico Giunchiglia. Embedding complex decision procedures inside an interactive theorem prover. Ann. Math. Artif. Intell., 8(3-4):475-502, 1993.
• [7] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
• [8] Randal E. Bryant, Steven M. German, and Miroslav N. Velev. Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Log., 2(1):93-134, 2001.
• [9] S. Campos and E. Clarke. Analysis and verification of real-time systems using quantitative symbolic algorithms. International Journal on Software Tools for Technology Transfer, 2(3):260-269, 1999.
• [10] Edmund M. Clarke. The birth of model checking. In 25 Years of Model Checking - History, Achievements, Perspectives, volume 5000 of Lecture Notes in Computer Science, pages 1-26. Springer, 2008.
• [11] Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 1983, pages 117-126. ACM Press, 1983.
• [12] Edmund M. Clarke and Jeannette M. Wing. Formal methods: State of the art and future directions. ACM Comput. Surv., 28(4):626-643, 1996.
• [13] Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337-340, 2008.
• [14] E. A. Emerson and R. Trefler. Parametric quantitative temporal reasoning. In Proceedings of the 14th Symp. on Logic in Computer Science (LICS’99), pages 336-343. IEEE Computer Society, July 1999.
• [15] Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning About Knowledge. MIT Press, 1995.
• [16] C. A. Furia and P. Spoletini. Tomorrow and all our yesterdays: MTL satisfiability over the integers. In Proceedings of the Theoretical Aspects of Computing (ICTAC’ 2008), volume 5160 of LNCS, pages 253-264. Springer-Verlag, 2008.
• [17] Fausto Giunchiglia and Roberto Sebastiani. Building decision procedures for modal logics from propositional decision procedure - the case study of modal K. In CADE, pages 583-597, 1996.
• [18] N. Markey and Ph. Schnoebelen. Symbolic model checking of simply-timed systems. In Proceedings of the Joint Conferences Formal Modelling and Analysis of Timed Systems (FORMATS’04) and Formal Techniques in RealTime and Fault-Tolerant Systems (FTRTFT’04), volume 3253 of LNCS, pages 102-117. Springer, 2004.
• [19] P. Merlin and D. J. Farber. Recoverability of communication protocols - implication of a theoretical study. IEEE Transaction on Communications, 24(9):1036-1043, 1976.
• [20] Amir Pnueli, Yoav Rodeh, Ofer Strichman, and Michael Siegel. Deciding equality formulas by small domains instantiations. In CAV, pages 455-469, 1999.
• [21] M. Pradella, A. Morzenti, and P. San Pietro. A metric encoding for bounded model checking. In Proceedings of the 2nd World Congress on Formal Methods (FM 2009), volume 5850 of LNCS, pages 741-756. Springer-Verlag, 2009.
• [22] J. P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symp. on Programming, volume 131 of LNCS, pages 337-351. Springer-Verlag, 1981.
• [23] Wiebe van der Hoek and Michael Wooldridge. Model checking knowledge and time. In Model Checking of Software, 9th International SPIN Workshop, Grenoble, France, April 11-13, 2002, Proceedings, volume 2318 of Lecture Notes in Computer Science, pages 95-111. Springer, 2002.
• [24] B. Woźna-Szcześniak, A. M. Zbrzezny, and A. Zbrzezny. The BMC method for the existential part of RTCTLK and interleaved interpreted systems. In Proceedings of the 15th Portuguese Conference on Artificial Intelligence (EPIA’2011), volume 7026 of LNAI, pages 551-565. Springer-Verlag, 2011.
• [25] Bożena Woźna-Szcześniak, Agnieszka Zbrzezny, and Andrzej Zbrzezny. SAT-based bounded model checking for RTECTL and simply-timed systems. In EPEW, pages 337-349, 2013.
• [26] A. Zbrzezny. A new translation from ECTL* to SAT. Fundamenta Informaticae, 120(3-4):377-397, 2012.