2008 | OriginalPaper | Buchkapitel
Model Checking CSP Revisited: Introducing a Process Analysis Toolkit
verfasst von : Jun Sun, Yang Liu, Jin Song Dong
Erschienen in: Leveraging Applications of Formal Methods, Verification and Validation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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
p
rocess
a
nalysis
t
oolkit 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.