Conference proceeding
Using Task Analytic Models to Visualize Model Checker Counterexamples
IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS (SMC 2010), pp 2069-2074
01 Jan 2010
Featured in Collection : UN Sustainable Development Goals @ Drexel
Abstract
Model checking is a type of automated formal verification that searches a system model's entire state space in order to mathematically prove that the system does or does not meet desired properties. An output of most model checkers is a counterexample: an execution trace illustrating exactly how a specification was violated. In most analysis environments, this output is a list of the model variables and their values at each step in the execution trace. We have developed a language for modeling human task behavior and an automated method which translates instantiated models into a formal system model implemented in the language of the Symbolic Analysis Laboratory (SAL). This allows us to use model checking formal verification to evaluate human-automation interaction. In this paper we present an operational concept and design showing how our task modeling visual notation and system modeling architecture can be exploited to visualize counterexamples produced by SAL. We illustrate the use of our design with a model related to the operation of an automobile with a simple cruise control.
Metrics
7 Record Views
25 citations in Scopus
Details
- Title
- Using Task Analytic Models to Visualize Model Checker Counterexamples
- Creators
- Matthew L. Bolton - Univ Virginia, Dept Syst & Informat Engn, Charlottesville, VA 22903 USAEllen J. Bass - University of VirginiaIEEE
- Publication Details
- IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS (SMC 2010), pp 2069-2074
- Series
- IEEE International Conference on Systems Man and Cybernetics Conference Proceedings
- Publisher
- IEEE
- Number of pages
- 6
- Resource Type
- Conference proceeding
- Language
- English
- Academic Unit
- Information Science
- Web of Science ID
- WOS:000295015301055
- Scopus ID
- 2-s2.0-78751553663
- Other Identifier
- 991019292228704721
UN Sustainable Development Goals (SDGs)
This publication has contributed to the advancement of the following goals:
InCites Highlights
Data related to this publication, from InCites Benchmarking & Analytics tool:
- Web of Science research areas
- Computer Science, Artificial Intelligence
- Computer Science, Cybernetics
- Computer Science, Information Systems