N-PAT: A Nested Model-Checker: (System Description)

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

Descripción completa

Detalles Bibliográficos
Autores principales: Bride, Hadrien, Cai, Cheng-Hao, Dong, Jin Song, Gore, Rajeev, Hóu, Zhé, Mahony, Brendan, McCarthy, Jim
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324034/
http://dx.doi.org/10.1007/978-3-030-51054-1_22
_version_ 1783551867712700416
author Bride, Hadrien
Cai, Cheng-Hao
Dong, Jin Song
Gore, Rajeev
Hóu, Zhé
Mahony, Brendan
McCarthy, Jim
author_facet Bride, Hadrien
Cai, Cheng-Hao
Dong, Jin Song
Gore, Rajeev
Hóu, Zhé
Mahony, Brendan
McCarthy, Jim
author_sort Bride, Hadrien
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7324034
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73240342020-06-30 N-PAT: A Nested Model-Checker: (System Description) Bride, Hadrien Cai, Cheng-Hao Dong, Jin Song Gore, Rajeev Hóu, Zhé Mahony, Brendan McCarthy, Jim Automated Reasoning Article 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. 2020-06-06 /pmc/articles/PMC7324034/ http://dx.doi.org/10.1007/978-3-030-51054-1_22 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
Bride, Hadrien
Cai, Cheng-Hao
Dong, Jin Song
Gore, Rajeev
Hóu, Zhé
Mahony, Brendan
McCarthy, Jim
N-PAT: A Nested Model-Checker: (System Description)
title N-PAT: A Nested Model-Checker: (System Description)
title_full N-PAT: A Nested Model-Checker: (System Description)
title_fullStr N-PAT: A Nested Model-Checker: (System Description)
title_full_unstemmed N-PAT: A Nested Model-Checker: (System Description)
title_short N-PAT: A Nested Model-Checker: (System Description)
title_sort n-pat: a nested model-checker: (system description)
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324034/
http://dx.doi.org/10.1007/978-3-030-51054-1_22
work_keys_str_mv AT bridehadrien npatanestedmodelcheckersystemdescription
AT caichenghao npatanestedmodelcheckersystemdescription
AT dongjinsong npatanestedmodelcheckersystemdescription
AT gorerajeev npatanestedmodelcheckersystemdescription
AT houzhe npatanestedmodelcheckersystemdescription
AT mahonybrendan npatanestedmodelcheckersystemdescription
AT mccarthyjim npatanestedmodelcheckersystemdescription

Ejemplares similares