Efficient approximate verification of Promela models via symmetry markers
| Autor: | Bosnacki, D., Donaldson, A.F., Leuschel, M., Massart, T., Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. |
|---|---|
| Přispěvatelé: | Algorithms, Geometry and Applications |
| Jazyk: | angličtina |
| Rok vydání: | 2007 |
| Předmět: | |
| Zdroj: | Automated Technology for Verification and Analysis ISBN: 9783540755951 ATVA Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007) 22-25 October 2007, Tokyo, Japan, 300-315 STARTPAGE=300;ENDPAGE=315;TITLE=Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007) 22-25 October 2007, Tokyo, Japan |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/978-3-540-75596-8_22 |
| Popis: | We present a new verification technique for Promela which exploits state-space symmetries induced by scalarset values used in a model. The technique involves efficiently computing a marker for each state encountered during search. We propose a complete verification method which only partially exploits symmetry, and an approximate verification method which fully exploits symmetry. We describe how symmetry markers can be efficiently computed and integrated into the Spin tool, and provide an empirical evaluation of our technique using the Topspin symmetry reduction package, which shows very good performance results and a high degree of precision for the approximate method (i.e. very few non-symmetric states receive the same marker). We also identify a class of models for which the approximate technique is precise. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|