Fate and free will in error traces
| Autor: | Hoonsang Jin, Kavita Ravi, Fabio Somenzi |
|---|---|
| Rok vydání: | 2004 |
| Předmět: |
Model checking
business.industry Computer science media_common.quotation_subject Machine learning computer.software_genre Debugging Reachability Theory of computation Free will Alternation (formal language theory) Segmentation Artificial intelligence business computer Algorithm Software Information Systems media_common Counterexample |
| Zdroj: | TACAS |
| ISSN: | 1433-2787 1433-2779 |
| DOI: | 10.1007/s10009-004-0146-9 |
| Popis: | The ability to generate counterexamples for failing properties is often cited as one of the strengths of model checking. However, it is often difficult to interpret long error traces in which many variables appear. Besides, a traditional error trace presents only one possible behavior of the system causing the failure, with no further annotation. Our objective is to identify some structure in the error trace to make debugging easier. We present an enhanced error trace as an alternation of fated (forced) and free segments. The fated segments show unavoidable progress toward the error while the free segments show choices that, if avoided, may have prevented the error. Hence, the demarcation into segments tends to highlight critical events. The segmentation of a trace raises the questions of whether the fated segment should indeed be inevitable and whether the free segments are critical in causing the error. Addressing these questions may help the user to better analyze the failure of the property. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink