HYASM: A Tool to Verify Hierarchical Systems

Angelo Ferrando; Vadim Malvone; Aniello Murano; Silvia Stranieri

doi:10.1109/WETICE57085.2023.10477788

HYASM: A Tool to Verify Hierarchical Systems

Angelo Ferrando
, Vadim Malvone
, Aniello Murano
, Silvia Stranieri

University of Genoa
University of Naples Federico II

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Hierarchical state machines represent a natural and useful framework to model and reason about modern systems. These machines encompass the ability to model hierarchical systems where some of the components can be reused in different contexts, e.g., by hierarchically calling subsystems. However, classical model checkers lack support to properly deal with hierarchical systems. Mostly, they treat the hierarchical calls as generic, possibly recursive, procedure calls. In this paper, we present HYASM a model checker for hierarchical systems as an extension of the tool YASM, a symbolic model-checker based on the CEGAR paradigm. Our tool uses a suitable flattening approach over hierarchical state machines, and experimental results show that our approach works very well in practice.

Original language	English
Title of host publication	2023 IEEE International Conference on Enabling Technologies
Subtitle of host publication	Infrastructure for Collaborative Enterprises, WETICE 2023
Publisher	IEEE Computer Society
ISBN (Electronic)	9798350350432
DOIs	https://doi.org/10.1109/WETICE57085.2023.10477788
Publication status	Published - 1 Jan 2023
Event	2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023 - Paris, France Duration: 14 Dec 2023 → 16 Dec 2023

Publication series

Name	Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE
ISSN (Print)	1524-4547

Conference

Conference	2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023
Country/Territory	France
City	Paris
Period	14/12/23 → 16/12/23

Keywords

Hierarchical State Machines
Model Checking
Temporal Logics

Access to Document

10.1109/WETICE57085.2023.10477788

Cite this

Ferrando, A., Malvone, V., Murano, A., & Stranieri, S. (2023). HYASM: A Tool to Verify Hierarchical Systems. In 2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023 (Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE). IEEE Computer Society. https://doi.org/10.1109/WETICE57085.2023.10477788

@inproceedings{fe5cda61baf64feb8701ed0d64bd6e17,

title = "HYASM: A Tool to Verify Hierarchical Systems",

abstract = "Hierarchical state machines represent a natural and useful framework to model and reason about modern systems. These machines encompass the ability to model hierarchical systems where some of the components can be reused in different contexts, e.g., by hierarchically calling subsystems. However, classical model checkers lack support to properly deal with hierarchical systems. Mostly, they treat the hierarchical calls as generic, possibly recursive, procedure calls. In this paper, we present HYASM a model checker for hierarchical systems as an extension of the tool YASM, a symbolic model-checker based on the CEGAR paradigm. Our tool uses a suitable flattening approach over hierarchical state machines, and experimental results show that our approach works very well in practice.",

keywords = "Hierarchical State Machines, Model Checking, Temporal Logics",

author = "Angelo Ferrando and Vadim Malvone and Aniello Murano and Silvia Stranieri",

note = "Publisher Copyright: {\textcopyright} 2023 IEEE.; 2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023 ; Conference date: 14-12-2023 Through 16-12-2023",

year = "2023",

month = jan,

day = "1",

doi = "10.1109/WETICE57085.2023.10477788",

language = "English",

series = "Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE",

publisher = "IEEE Computer Society",

booktitle = "2023 IEEE International Conference on Enabling Technologies",

}

Ferrando, A, Malvone, V, Murano, A & Stranieri, S 2023, HYASM: A Tool to Verify Hierarchical Systems. in 2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023. Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE, IEEE Computer Society, 2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023, Paris, France, 14/12/23. https://doi.org/10.1109/WETICE57085.2023.10477788

HYASM: A Tool to Verify Hierarchical Systems. / Ferrando, Angelo; Malvone, Vadim; Murano, Aniello et al.
2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023. IEEE Computer Society, 2023. (Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - HYASM

T2 - 2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023

AU - Ferrando, Angelo

AU - Malvone, Vadim

AU - Murano, Aniello

AU - Stranieri, Silvia

PY - 2023/1/1

Y1 - 2023/1/1

N2 - Hierarchical state machines represent a natural and useful framework to model and reason about modern systems. These machines encompass the ability to model hierarchical systems where some of the components can be reused in different contexts, e.g., by hierarchically calling subsystems. However, classical model checkers lack support to properly deal with hierarchical systems. Mostly, they treat the hierarchical calls as generic, possibly recursive, procedure calls. In this paper, we present HYASM a model checker for hierarchical systems as an extension of the tool YASM, a symbolic model-checker based on the CEGAR paradigm. Our tool uses a suitable flattening approach over hierarchical state machines, and experimental results show that our approach works very well in practice.

AB - Hierarchical state machines represent a natural and useful framework to model and reason about modern systems. These machines encompass the ability to model hierarchical systems where some of the components can be reused in different contexts, e.g., by hierarchically calling subsystems. However, classical model checkers lack support to properly deal with hierarchical systems. Mostly, they treat the hierarchical calls as generic, possibly recursive, procedure calls. In this paper, we present HYASM a model checker for hierarchical systems as an extension of the tool YASM, a symbolic model-checker based on the CEGAR paradigm. Our tool uses a suitable flattening approach over hierarchical state machines, and experimental results show that our approach works very well in practice.

KW - Hierarchical State Machines

KW - Model Checking

KW - Temporal Logics

U2 - 10.1109/WETICE57085.2023.10477788

DO - 10.1109/WETICE57085.2023.10477788

M3 - Conference contribution

AN - SCOPUS:85190366843

T3 - Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE

BT - 2023 IEEE International Conference on Enabling Technologies

PB - IEEE Computer Society

Y2 - 14 December 2023 through 16 December 2023

ER -

Ferrando A, Malvone V, Murano A, Stranieri S. HYASM: A Tool to Verify Hierarchical Systems. In 2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023. IEEE Computer Society. 2023. (Proceedings of the Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE). doi: 10.1109/WETICE57085.2023.10477788

HYASM: A Tool to Verify Hierarchical Systems

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this