We propose two expressive and complementary techniques for the verification of safety properties of infinite-state BIP models. Both our techniques deal with the full BIP specification, while the existing approaches impose considerable restrictions: they either verify finite-state systems or they do not handle the transfer of data on the interactions and priorities. Firstly, we propose an instantiation of the ESST (Explicit Scheduler Symbolic Thread) framework to verify BIP models. The key insight is to apply symbolic reasoning to analyze the behavior of the system described by the BIP components, and an explicit-state search to analyze the behavior of the system induced by the BIP interactions and priorities. The combination of symbolic and explicit exploration techniques allow to benefit from abstraction, useful when reasoning about data, and from partial order reduction, useful to mitigate the state space explosion due to concurrency. Secondly, we propose an encoding from a BIP model into a symbolic, infinitestate transition system. This technique allows us to leverage the state of the art verification algorithms for the analysis of infinite-state systems. We implemented both techniques and we evaluated their performance against the existing approaches. The results show the effectiveness of our approaches with respect to the state of the art, and their complementarity for the analysis of safe and unsafe BIP models.

Formal Verification of Infinite-State BIP Models / Bliudze, Simon; Cimatti, Alessandro; Jaber, Mohamad; Mover, Sergio; Roveri, Marco; Saab, Wajeb; Wang, Qiang. - STAMPA. - 9364:(2015), pp. 326-343. (Intervento presentato al convegno Automated Technology for Verification and Analysis 13th International Symposium, ATVA 2015 tenutosi a Shanghai, China nel October 12-15, 2015) [10.1007/978-3-319-24953-7].

Formal Verification of Infinite-State BIP Models

Cimatti Alessandro;Mover Sergio;Roveri Marco;
2015-01-01

Abstract

We propose two expressive and complementary techniques for the verification of safety properties of infinite-state BIP models. Both our techniques deal with the full BIP specification, while the existing approaches impose considerable restrictions: they either verify finite-state systems or they do not handle the transfer of data on the interactions and priorities. Firstly, we propose an instantiation of the ESST (Explicit Scheduler Symbolic Thread) framework to verify BIP models. The key insight is to apply symbolic reasoning to analyze the behavior of the system described by the BIP components, and an explicit-state search to analyze the behavior of the system induced by the BIP interactions and priorities. The combination of symbolic and explicit exploration techniques allow to benefit from abstraction, useful when reasoning about data, and from partial order reduction, useful to mitigate the state space explosion due to concurrency. Secondly, we propose an encoding from a BIP model into a symbolic, infinitestate transition system. This technique allows us to leverage the state of the art verification algorithms for the analysis of infinite-state systems. We implemented both techniques and we evaluated their performance against the existing approaches. The results show the effectiveness of our approaches with respect to the state of the art, and their complementarity for the analysis of safe and unsafe BIP models.
2015
Proceedings of ATVA
Shanghai, China
Springer
978-3-319-24952-0
Bliudze, Simon; Cimatti, Alessandro; Jaber, Mohamad; Mover, Sergio; Roveri, Marco; Saab, Wajeb; Wang, Qiang
Formal Verification of Infinite-State BIP Models / Bliudze, Simon; Cimatti, Alessandro; Jaber, Mohamad; Mover, Sergio; Roveri, Marco; Saab, Wajeb; Wang, Qiang. - STAMPA. - 9364:(2015), pp. 326-343. (Intervento presentato al convegno Automated Technology for Verification and Analysis 13th International Symposium, ATVA 2015 tenutosi a Shanghai, China nel October 12-15, 2015) [10.1007/978-3-319-24953-7].
File in questo prodotto:
File Dimensione Formato  
atva2015.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 420.9 kB
Formato Adobe PDF
420.9 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/258736
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 15
social impact