Enhancing BMC-based protocol verification using transition-by-transition FSM traversal
| dc.contributor.author | Nguyen, Minh D. | |
| dc.contributor.author | Stoffel, Dominik | |
| dc.contributor.author | Kunz, Wolfgang | |
| dc.contributor.editor | Cremers, Armin B. | |
| dc.contributor.editor | Manthey, Rainer | |
| dc.contributor.editor | Martini, Peter | |
| dc.contributor.editor | Steinhage, Volker | |
| dc.date.accessioned | 2019-10-11T07:41:17Z | |
| dc.date.available | 2019-10-11T07:41:17Z | |
| dc.date.issued | 2005 | |
| dc.description.abstract | We present a technique to automatically derive reachability information from designs to enhance Bounded Model Checking style verification. The method is well suited for typical protocol applications where the operation is controlled by a main finite state machine (FSM) interacting with a hierarchy of sub-FSMs. The algorithm traverses the global state space of the design based on single transitions of the main finite state machine. This transition-by-transition decomposition of the state space distinguishes our approach from previous ones. The experimental results clearly show the value of the new method. In our experiments, false negatives could be completely avoided and the overall verification effort was drastically reduced. | en |
| dc.identifier.isbn | 3-88579-396-2 | |
| dc.identifier.pissn | 1617-5468 | |
| dc.identifier.uri | https://dl.gi.de/handle/20.500.12116/28047 | |
| dc.language.iso | en | |
| dc.publisher | Gesellschaft für Informatik e.V. | |
| dc.relation.ispartof | Informatk 2005. Informatik Live! Band 1 | |
| dc.relation.ispartofseries | Lecture Notes in Informatics (LNI) - Proceedings, Volume P-67 | |
| dc.title | Enhancing BMC-based protocol verification using transition-by-transition FSM traversal | en |
| dc.type | Text/Conference Paper | |
| gi.citation.endPage | 305 | |
| gi.citation.publisherPlace | Bonn | |
| gi.citation.startPage | 303 | |
| gi.conference.date | 19.-22. September 2005 | |
| gi.conference.location | Bonn | |
| gi.conference.sessiontitle | Regular Research Papers |
Dateien
Originalbündel
1 - 1 von 1
Lade...
- Name:
- GI-Proceedings.67-68.pdf
- Größe:
- 190.26 KB
- Format:
- Adobe Portable Document Format