Efficient Bounded Model Checking for LTL

Rui Wang; Xian Jin  Fu

doi:10.4028/www.scientific.net/AMM.380-384.1239

Paper Titles

Several Strategies to Compute the Minimum Stochastic Dominating Sets in Graphs
p.1221

Computer Simulation of the Subwavelength Design for Different Characteristic Equations
p.1226

Research on Clustering Algorithm for Wireless Sensor Networks
p.1231

An Algorithm Based on SIFT Matching Combined SR Saliency Detection with Frequency Segmentation for Remote Sensing Images
p.1235

Efficient Bounded Model Checking for LTL
p.1239

Simulation of VAV System Control Based on Improved Bacterial Foraging Optimization Algorithm
p.1243

Analysis on Children Custody Decision Making Model
p.1247

Relationship between Short Term Traffic Flow Chaos Fractal Properties and the Necessary Data for Prediction
p.1256

The New Criterion for Determining Nonsigularity of Matrices
p.1262

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 380-384Efficient Bounded Model Checking for LTL

Efficient Bounded Model Checking for LTL

Abstract:

Bounded Model Checking is an efficient method of finding bugs in system designs. LTL is one of the most frequently used specification languages in model checking. In this paper, We present an linearization encoding for LTL bounded model checking. We use the incremental SAT technology to solve the BMC problem. We implement the new encoding in NuSMV model checker.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 380-384)

Pages:

1239-1242

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.380-384.1239

Citation:

Cite this paper

Online since:

August 2013

Authors:

Rui Wang, Xian Jin Fu

Keywords:

Bounded Model Checking, Linearization Encoding, LTL, NuSMV

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic model checking without bdds. In Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1579 of Lecture Notes in Computer Science, pp.193-207. Springer-Verlag, (1999).

DOI: 10.1007/3-540-49059-0_14

Google Scholar

[2] K. Heljanko, T. Junttila, and T. Latvala. Incremental and complete bounded model checking for full pltl. In Computer Aided Veri_cation, pages 517–527. Springer, (2005).

DOI: 10.1007/11513988_10

Google Scholar

[3] E. Clarke, D. Kroening, J. Ouaknine, and O. Strichman. Completeness and complexity of bounded model checking. In B. Steffen and G. Levi, editors, VMCAI'04, volume 2937 of Lecutre Notes in Computer Science, pages 85–96. Springer-Verlag, (2004).

DOI: 10.1007/978-3-540-24622-0_9

Google Scholar

[4] R. Cavada, A. Cimatti, C. A. Jochim, G. Keighren, E. Olivetti, M. Pistore, M. Roveri, and A. Tchaltsev. Nusmv 2. 5 user manual. http: /nusmv. fbk. eu/NuSMV/userman/v25/nusmv. pdf, Apr. (2010).

DOI: 10.1007/3-540-45657-0_29

Google Scholar

[5] E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In CAV'94, volume 818 of Lecture Notes in Computer Science, pages 415–427. Springer-Verlag, (1994).

DOI: 10.1007/3-540-58179-0_72

Google Scholar

[6] Cimatti, A., Pistore, M., Roveri, M., Sebastiani, R.: Improving the encoding of LTL model checking into SAT. In: Verification, Model Checking, and Abstract Interpretation (VMCAI'2002). Volume 2294 of LNCS., Springer (2002) 196–207.

DOI: 10.1007/3-540-47813-2_14

Google Scholar

[7] Frisch, A., Sheridan, D., Walsh, T.: A fixpoint encoding for bounded model checking. In: FormalMethods in Computer-Aided Design (FMCAD'2002). Volume 2517 of LNCS., Springer (2002) 238–255.

DOI: 10.1007/3-540-36126-x_15

Google Scholar

[8] T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is better: Efficient bounded model checking for past LTL. In VMCAI'05, volume 3385 of LNCS, pages 380–395. Springer, jan (2005).

DOI: 10.1007/978-3-540-30579-8_25

Google Scholar

[9] M.W. Moskewicz, C.F. Madigan, Y. Zhao, and S. Malik. Chaff: Engineering an efficent sat solver. In Proceedings of the 38th Design Automation Conference (DAC2001), volume 208, pages 530–535. Springer-Verlag, (2001).

DOI: 10.1145/378239.379017

Google Scholar

[10] H. Tauriainen and K. Heljanko. Testing ltl formula translation into buchi automata. STTT-International Journal on Software Tools for Technology Transfer, (4): 57-70, (2002).

DOI: 10.1007/s100090200070

Google Scholar