Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
10-2008
Abstract
FDR, initially introduced decades ago, is the de facto analyzer for Communicating Sequential Processes (CSP). Model checking techniques have been evolved rapidly since then. This paper describes PAT, i.e., a process analysis toolkit which complements FDR in several aspects. PAT is designed to analyze event-based compositional system models specified using CSP as well as shared variables and asynchronous message passing. It supports automated refinement checking, model checking of LTL extended with events, etc. In this paper, we highlight how partial order reduction is applied to improve refinement checking in PAT. Experiment results show that PAT outperforms FDR in some cases.
Keywords
Model Check, Linear Temporal Logic, Label Transition System, Binary Decision Diagram, Communicate Sequential Process
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of Third International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15
First Page
307
Last Page
322
ISBN
9783540884798
Identifier
10.1007/978-3-540-88479-8_22
Publisher
Springer Link
City or Country
Greece
Citation
SUN, Jun; LIU, Yang; and DONG, Jin Song.
Model checking CSP revisited: Introducing a process analysis toolkit. (2008). Proceedings of Third International Symposium, ISoLA 2008, Porto Sani, Greece, October 13-15. 307-322.
Available at: https://ink.library.smu.edu.sg/sis_research/5050
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-540-88479-8_22