Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
Articles 1 - 2 of 2
Full-Text Articles in Physical Sciences and Mathematics
Specifying And Verifying Event-Based Fairness Enhanced Systems, Jun Sun, Yang Liu, Jin Song Dong, Hai H. Wang
Specifying And Verifying Event-Based Fairness Enhanced Systems, Jun Sun, Yang Liu, Jin Song Dong, Hai H. Wang
Research Collection School Of Computing and Information Systems
Liveness/Fairness plays an important role in software specification, verification and development. Existing event-based compositional models are safety-centric. In this paper, we describe a framework for systematically specifying and verifying event-based systems under fairness assumptions. We introduce different event annotations to associate fairness constraints with individual events. Fairness annotated events can be used to embed liveness/fairness assumptions in event-based models flexibly and naturally. We show that state-of-the-art verification algorithms can be extended to verify models under fairness assumptions, with little computational overhead. We further improve the algorithm by other model checking techniques like partial order reduction. A toolset named Pat has …
Model Checking Csp Revisited: Introducing A Process Analysis Toolkit, Jun Sun, Yang Liu, Jin Song Dong
Model Checking Csp Revisited: Introducing A Process Analysis Toolkit, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
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.