Abstract
In our previous work, we formally validated the correctness of a translation from a subset of Accellera’s Property Specification Language (PSL) to linear temporal logic (LTL) using the HOL theorem prover. We also built an interface from HOL to the SMV model checker based on a formal translation of LTL to ω-automata. In the present paper, we describe how this work has been extended and combined to produce a model checking infrastructure for a significant subset of PSL that works by translating model checking problems to equivalent checks for the existence of fair paths through a Kripke structure specified in higher order logic. This translation is done by theorem proving in HOL, so it is proven to be correct. The existence check is carried out using the interface from HOL to SMV. Moreover, we have applied our infrastructure to implement a tool for validating the soundness of a separate PSL model checker.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Accellera. Property specification language reference manual, version 1.1 (June 2004), http://www.eda.org
Armoni, R., et al.: Resets vs. aborts in linear temporal logic. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 65–80. Springer, Heidelberg (2003)
Beer, I., et al.: The temporal logic Sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363–367. Springer, Heidelberg (2001)
Beer, I., et al.: RuleBase: Model checking at IBM. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 480–483. Springer, Heidelberg (1997)
Burch, J., et al.: Symbolic model checking: 1020 states and beyond. In: Symposium on Logic in Computer Science (LICS), Washington, D.C., June 1990, pp. 1–33. IEEE Computer Society Press, Los Alamitos (1990)
Bustan, D., Fisman, D., Havlicek, J.: Automata construction for PSL. Technical Report MCS05- 04, The Weizmann Institute of Science, Israel (2005)
Büchi, J.: On a decision method in restricted second order arithmetic. In: Nagel, E. (ed.) International Congress on Logic, Methodology and Philosophy of Science, pp. 1–12. Stanford University Press, Stanford (1960)
Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)
Daniele, M., Giunchiglia, F., Vardi, M.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)
DeepChip survey on assertions (June 2004), http://www.deepchip.com/items/dvcon04-06.html
Emerson, E., Clarke, E.: Using branching-time temporal logic to synthesize synchronization skeletons. Science of Computer Programming 2(3), 241–266 (1982)
Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Gerth, R., et al.: Simple on-the-fly automatic verification of linear temporal logic. In: Symposium on Protocol Specification, Testing, and Verification (PSTV), Warsaw, June 1995, North-Holland, Amsterdam (1995)
Gordon, M.: HOL: A machine oriented formulation of higher order logic. Tech. Rep. 68, Computer Laboratory, University of Cambridge (May 1985)
Gordon, M.: PSL semantics in higher order logic. In: Workshop on Designing Correct Circuits (DCC), Barcelona, Spain (2004)
Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)
Havlicek, J., Fisman, D., Eisner, C.: Basic results on the semantics of Accellera PSL 1.1 foundation language. Technical Report 2004.02, Accellera (2004)
Kleene, S.: Representation of events in nerve nets and finite automata. In: Shannon, C., McCarthy, J. (eds.) Automata Studies, pp. 3–41. Princeton University Press, Princeton (1956)
McMillan, K.: Symbolic Model Checking. Kluwer, Norwell (1993)
Pnueli, A.: The temporal logic of programs. In: Symposium on Foundations of Computer Science (FOCS), vol. 18, New York, vol. 18, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)
Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006)
Schneider, K.: Improving automata generation for linear temporal logic by considering the automata hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 39–54. Springer, Heidelberg (2001)
Schneider, K.: Verification of Reactive Systems – Formal Methods and Algorithms. In: Texts in Theoretical Computer Science. EATCS Series, Springer, Heidelberg (2003)
Schneider, K., Hoffmann, D.: A HOL conversion for translating linear time temporal logic to omega-automata. In: Bertot, Y., et al. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 255–272. Springer, Heidelberg (1999)
Tuerk, T.: A hierarchy for Accellera’s property specification language. Master’s thesis, University of Kaiserslautern, Department of Computer Science (2005)
Tuerk, T., Schneider, K.: From PSL to LTL: A formal validation in HOL. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 342–357. Springer, Heidelberg (2005)
Vardi, M.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)
Wolper, P.: Temporal logic can be more expressive. In: Symposium on Foundations of Computer Science (FOCS), New York, pp. 340–348. IEEE Computer Society Press, Los Alamitos (1981)
Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1-2), 72–99 (1983)
Wolper, P., Vardi, M., Sistla, A.: Reasoning about infinite computations paths. In: Symposium on Foundations of Computer Science (FOCS), New York, pp. 185–194. IEEE Computer Society Press, Los Alamitos (1983)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Tuerk, T., Schneider, K., Gordon, M. (2007). Model Checking PSL Using HOL and SMV. In: Bin, E., Ziv, A., Ur, S. (eds) Hardware and Software, Verification and Testing. HVC 2006. Lecture Notes in Computer Science, vol 4383. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70889-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-70889-6_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70888-9
Online ISBN: 978-3-540-70889-6
eBook Packages: Computer ScienceComputer Science (R0)