nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Bounded Correctness Checking for Extended CTL Properties with Past Operators

verfasst von : Fei Pu

Erschienen in: Geo-Spatial Knowledge and Intelligence

Verlag: Springer Singapore

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Bounded semantics of a certain temporal logic is a basis to develop bounded model checking algorithms for finding errors in system designs. Traditional temporal logics are used in formal verification to predicate about the future evolutions of dynamic systems, both with a linear time model or a branching time model. This paper we further study bounded semantics of extended CTL formulas with past operators (PeCTL) which not only allows some sort of fairness but also could reason about the past behaviors of the systems being verified. Since QBF (quantified boolean formula) is exponentially more succinct in expressing specifications, we thus develop a QBF encoding of PeCTL from the proposed bounded semantics. Finally, we present a bounded correctness checking algorithm for PeCTL formulas and apply the bounded semantics of PeCTL to derive a QBF-based characterization of PeCTL properties.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Research on a New Density Clustering Algorithm Based on MapReduce

Nächstes Kapitel A Cloud Based Three Layer Key Management Scheme for VANET

Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 408–414. Springer, Heidelberg (2005). https://doi.org/10.1007/11499107_32CrossRef

Biere, A., Cimmatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58, 117–148 (2003)CrossRef

Heljanko, K., Junttila, T., Latvala, T.: Incremental and Complete Bounded Model Checking for Full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98–111. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_10CrossRef

Penczek, W., Wozna, B., Zbrzezny, A.: Bounded model checking for the universal fragment of CTL. Fundam. Inform. 51, 135–156 (2002)MathSciNetMATH

Oshman, R., Grumberg, O.: A new approach to bounded model checking for branching time logics. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 410–424. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75596-8_29CrossRefMATH

Laroussinie, F., Schnoebelen, P.: Specification in CTL past for verification in CTL. Inf. Comput. 156, 236–263 (2000)MathSciNetCrossRef

Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 585–602. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_39CrossRef

Benedetti, M., Cimatti, A.: Bounded Model checking for past LTL. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 18–33. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_3CrossRefMATH

10.

Armando, A., Carbone, R., Compagna, L.: SATMC: A SAT-based model checker for security-critical systems. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 31–45. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_3CrossRef

11.

Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_26CrossRef

12.

McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher, Dordrecht (1993)CrossRef

13.

Bryant, R.E.: Binary decision diagrams and beyond: enabling technologies for formal verification. In: ICCAD, pp. 236–243 (1995)

14.

Jussila, T., Biere, A.: Compressing BMC encodings with QBF. Electron. Notes Theor. Comput. Sci. 174, 45–56 (2006)CrossRef

15.

Allen, E.: Sometimes and Not Never revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986)MathSciNetCrossRef

16.

Zhang, W.: QBF encoding of temporal properties and QBF-based verification. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 224–239. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_16CrossRef

17.

Zhang, W., Smentics, B.: Theor. Comput. Sci. 564, 1–29 (2015)CrossRef

18.

Zhaowei, X., Zhang, W.: Linear templates of ACTL formulas with an application to SAT-based verification. Inf. Process. Lett. 127, 6–16 (2017)MathSciNetCrossRef

19.

Zhang, W.: Bounded semantics of CTL and SAT-based verification. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 286–305. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10373-5_15CrossRef

20.

Clarke, E., Kroening, D., Ouaknine, J., Strichman, O.: Computational challenges in bounded model checking. Int. J. Softw. Tools Technol. Transfer 7, 174–183 (2005)CrossRef

21.

Ganai, M.K., Gupta, A.: Accelerating high-level bounded model checking. In: ICCAD, pp. 794–801 (2006)

22.

Wozna, B.: ATCL* properties and bounded model checking. Fundam. Inform. 63, 65–87 (2004)MathSciNetMATH

23.

Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past LTL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 245–259. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30494-4_18CrossRef

24.

Ji, K.: CTL model checking in deduction modulo. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 295–310. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_20CrossRef

25.

Kemper, S.: SAT-based verification for timed component connectors. Sci. Comput. Program. 77(7–8), 779–798 (2012)CrossRef

26.

Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time markov chains using bounded model checking. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 366–380. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-93900-9_29CrossRefMATH

27.

Gomes, C., Selman, B., Kautz, H.: SAT encodings of state-space reachability problems in numeric domains. In: IJCAI, pp. 1918–1923 (2007)

28.

Navarro-Pérez, J.A., Voronkov, A.: Encodings of bounded LTL model checking in effectively propositional logic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 346–361. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73595-3_24CrossRef

Titel: Bounded Correctness Checking for Extended CTL Properties with Past Operators
verfasst von: Fei Pu
Verlag: Springer Singapore
Buch: Geo-Spatial Knowledge and Intelligence
Print ISBN: 978-981-13-0895-6

Electronic ISBN: 978-981-13-0896-3

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-981-13-0896-3_56

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"