Abstract
During the last two decades, model checking has emerged as an effective system analysis technique complementary to simulation and testing. Many model checking algorithms and state space reduction techniques have been proposed. Although it is desirable to have dedicated model checkers for every language (or application domain), implementing one with effective reduction techniques is rather challenging. In this work, we present a generic and extensible framework PAT, which facilitates users to build customized model checkers. PAT provides a library of state-of-art model checking algorithms as well as support for customizing language syntax, semantics, state space reduction techniques, graphic user interfaces, and even domain specific abstraction techniques. Based on this design, model checkers for concurrent systems, real-time systems, probabilistic systems and Web Services are developed inside the PAT framework, which demonstrates the practicality and scalability of our approach.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
PAT: Process Analysis Toolkit, http://pat.comp.nus.edu.sg/
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Dwyer, M.B., Hatcliff, J., Hoosier, M., Robby: Building Your Own Software Model Checker Using the Bogor Extensible Model Checking Framework. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 148–152. Springer, Heidelberg (2005)
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Wiley, Chichester (2003)
Liu, Y., Chen, W., Liu, Y.A., Sun, J.: Model Checking Lineariability via Refinement. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 321–337. Springer, Heidelberg (2009)
Liu, Y., Pang, J., Sun, J., Zhao, J.: Efficient Verification of Population Ring Protocols in PAT. In: TASE 2009, pp. 81–89 (2009)
Liu, Y., Sun, J., Dong, J.S.: Scalable Multi-Core Model Checking Fairness Enhanced Systems. In: ICFEM 2009, pp. 426–445 (December 2009)
Magee, J., Kramer, J.: Concurrency: State Models & Java Programs. Wiley, Chichester (1999)
Roscoe, A.W.: Model-checking CSP. In: A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 353–378 (1994)
Sun, J., Liu, Y., Dong, J.S.: Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. In: ISoLA 2008, pp. 307–322. Springer, Heidelberg (2008)
Sun, J., Liu, Y., Dong, J.S., Chen, C.Q.: Integrating Specification and Programs for System Modeling and Verification. In: TASE 2009, pp. 127–135. IEEE Computer Society, Los Alamitos (2009)
Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 702–708. Springer, Heidelberg (2009)
Sun, J., Liu, Y., Dong, J.S., Sun, J.: Bounded Model Checking of Compositional Processes. In: TASE 2008, pp. 23–30. IEEE Computer Society, Los Alamitos (2008)
Sun, J., Liu, Y., Dong, J.S., Wang, H.H.: Verifying Stateful Timed CSP using Implicit Clocks and Zone Abstraction. In: ICFEM 2009, pp. 581–600 (December 2009)
Sun, J., Liu, Y., Roychoudhury, A., Liu, S., Dong, J.S.: Fair Model Checking of Parameterized Systems. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 123–139. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, Y., Sun, J., Dong, J.S. (2010). Developing Model Checkers Using PAT. In: Bouajjani, A., Chin, WN. (eds) Automated Technology for Verification and Analysis. ATVA 2010. Lecture Notes in Computer Science, vol 6252. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15643-4_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-15643-4_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15642-7
Online ISBN: 978-3-642-15643-4
eBook Packages: Computer ScienceComputer Science (R0)