Model checking CSP revisited: Introducing a process analysis toolkit

• Main Authors: SUN, Jun, LIU, Yang, DONG, Jin Song
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2008
• Subjects: Model Check; Linear Temporal Logic; Label Transition System; Binary Decision Diagram; Communicate Sequential Process; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/5050; https://ink.library.smu.edu.sg/context/sis_research/article/6053/viewcontent/10.1.1.269.6050.pdf
• Institution: Singapore Management University

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 analyz...