N-PAT: A Nested Model-Checker
Discrete Mathematics
2020-05-13 v1 Formal Languages and Automata Theory
Abstract
N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study.
Keywords
Cite
@article{arxiv.2005.05520,
title = {N-PAT: A Nested Model-Checker},
author = {Hadrien Bride and Cheng-Hao Cai and Jin Song Dong and Rajeev Gore and Zhé Hóu and Brendan Mahony and Jim McCarthy},
journal= {arXiv preprint arXiv:2005.05520},
year = {2020}
}