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

Additional URL

https://doi.org/10.1007/978-3-540-88479-8_22

Share

COinS