Using task analytic models to visualize model checker counterexamples
DOI: 10.1109/icsmc.2010.5641711
archive: archived pipeline: cataloged verified
Get this paper ↗ (DOI — opens at the source; we link to it, we don't host it)
Summary
This paper addresses the challenge of interpreting model checker counterexamples in the context of human-automation interaction (HAI). While model checking is an effective formal verification method for identifying specification violations in complex systems, its outputs—typically lists of variable values at each execution step—are difficult for analysts to interpret, particularly when human behavior is involved. The authors propose a visualization method that leverages task analytic models to make these counterexamples more intelligible, specifically by showing how human task behavior interacts with other system components to cause a violation. The methodology integrates an Enhanced Operator Function Model (EOFM), an XML-based language for modeling human task behavior, with the Symbolic Analysis Laboratory (SAL), a formal verification framework. EOFMs represent human activities hierarchically, specifying preconditions, completion conditions, and decomposition operators. The authors developed a prototype visualization tool implemented in Microsoft Visio and Visual Basic for Applications. This tool takes an instantiated EOFM and a SAL-generated counterexample as input. It organizes system variables into architectural designations (mission, human task behavior, human-device interface, device automation, and environment) and renders the human task behavior using EOFM’s visual notation. The visualization supports three key features: encapsulation of variables into high-level designations, interactive refinement allowing analysts to inspect detailed variable states and task execution graphs, and highlighting of changes in variable values and task states across execution steps. To demonstrate the approach, the authors applied the visualization to a formal model of a driver operating a car with cruise control near a traffic light. The specification required that the car never reach an intersection while moving if the light is red. The model checker produced a counterexample where the driver failed to stop. The visualization revealed that the driver attempted to "roll to a stop" by releasing the gas pedal but had previously enabled cruise control and failed to disable it. By stepping through the counterexample, the analyst could see that the driver’s action of releasing the gas was overridden by the automation because the cruise control remained active, leading to the violation. The visualization clearly displayed the execution state of the human task model (e.g., "Executing" vs. "Done") alongside the system variables, pinpointing the specific interaction error. The significance of this work lies in providing a structured way to analyze HAI failures using formal methods. By combining the abstracted view of system architecture with the detailed, diagrammatic representation of human tasks, the visualization helps analysts determine how human behavior contributes to specification violations. The authors note that while the encapsulation and table-like features scale well for systems with many variables, the diagrammatic representation of human tasks may face scalability challenges in applications with very large task models. The approach has been successfully applied to other domains, including medical devices and aircraft systems, suggesting its utility for safety-critical system design.
Key finding
The proposed visualization method effectively interprets model checker counterexamples by integrating task analytic visual notation with architectural variable encapsulation to reveal human-automation interaction errors.
Methodology
simulation_modeling
Provenance
The full processing record for this entry. Every stage of this paper's journey through the pipeline is logged — what ran, with which tool and model, how many attempts it took, and when it last completed. Discovered via author_sweep_intake on 2026-05-28.
| Stage | Outcome | Tool | Model | Prompt | Attempts | Completed |
|---|---|---|---|---|---|---|
| discover | success | author_sweep | — | — | 2 | 2026-05-28 |
| archive | success | canonical_url | — | — | 1 | 2026-06-06 |
| extract | success | cached | — | — | 3 | 2026-06-10 |
| clean | success | clean | — | — | 1 | 2026-06-04 |
| chunk | success | chunk | — | — | 1 | 2026-06-04 |
| embed | success | embed | Qwen/Qwen3-Embedding-8B | — | 1 | 2026-06-04 |
| enrich | success | — | — | — | 1 | 2026-05-28 |
| promote | success | — | — | — | 1 | 2026-06-04 |
| summarize | success | llm | qwen3.6-27b-prismaquant | summ-v5 | 2 | 2026-06-10 |
| tag | success | vector_similarity | — | — | 15 | 2026-06-11 |
| verify | success | — | — | — | 2 | 2026-06-10 |
Summary generated by qwen3.6-27b-prismaquant on 2026-06-10; verification: verified.
Topics
Ranked by relevance to this paper. Hover a topic for its definition.
Information type
What kind of knowledge this paper contributes, grouped by family — independent of topic (what it is about) and method (how it was studied).
- Theoretical Contribution: computational model