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
N1 - Publisher Copyright:
© 2023 IEEE.
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 -