Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-540-88479-8-22
Title: Model checking CSP revisited: Introducing a process analysis toolkit
Authors: Sun, J. 
Liu, Y. 
Dong, J.S. 
Issue Date: 2008
Source: Sun, J.,Liu, Y.,Dong, J.S. (2008). Model checking CSP revisited: Introducing a process analysis toolkit. Communications in Computer and Information Science 17 CCIS : 307-322. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-540-88479-8-22
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. © 2008 Springer-Verlag.
Source Title: Communications in Computer and Information Science
URI: http://scholarbank.nus.edu.sg/handle/10635/40017
ISBN: 3540884785
ISSN: 18650929
DOI: 10.1007/978-3-540-88479-8-22
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

80
checked on Dec 13, 2017

Page view(s)

41
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.