Power Plant Control Room reference
baxter Baxter
787 Cockpit reference
Predator Drone Control Room reference
State flow in WiSAR

CFP Formal Verification in Human-Machine Systems

Overview

The goal of the workshop is to bring together the fields of formal verification, cognitive modeling, and task analysis to study the design and verification of real human-machine systems. Recent papers in each of these communities discuss modeling challenges and the application of basic formal verification in human-machine interaction; however, there is little communication between researchers in these different areas and there are many open questions that require cross-disciplinary collaboration. The workshop is to bring together experts from many communities in an environment where it is possible to explore key research areas, common solutions, near-term research problems, and advantages in combining the best of the different communities.

Submissions

We solicit papers describing original work either in-progress or finished, position papers or extended abstracts describing research or positions. Papers should follow the AAAI formatting, with a page-limit of 6 pages. Proceedings of the symposium are available here. Please consider submitting an extended version of your paper to the special issue of the IEEE Transactions on Human-Machine Systems dedicated to the same topic (http://mc.manuscriptcentral.com/thms).

Important Dates

Oct 22 Oct 18, 2013: Submission deadline
Dec 10, 2013: Notification of acceptance/rejection
Jan 10, 2014: Camera-ready papers due
Mar 1, 2014: Registration deadline
March 24-26, 2014: Symposium

Topics of Interest

  • What model classes, methodologies, and constructs are appropriate for modeling human and
        machine activities in a way that is amenable to formal verification? Examples include

    • Programming languages
    • State Machines
    • Activity models (e.g. Brahams)
    • Cognitive models (SOAR, ACT-R, DIARC, etd.)
    • Task analyses-based models (GDTA, CWA, etc.)
    • Probabilistic models
    • Behavioral game theory

  • What levels of abstraction are appropriate for such modeling, and what information is lost in using abstraction?

  • What is the role for formal verification in an evaluation space that also includes simulation as well as human in the loop experimentation?

  • What are the contexts, if any, for which the trade offs between authority between humans, autonomy, and model-based reasoning can be specified?

  • What is the impact on design for including explicit (meta-) reasoning models in the human-machine interaction loop?

  • What types of formal verification tools are appropriate, and what other lessons from formal verification apply to human-machine systems?

  • What are the ethical considerations of using verified models to allocate responsibility and authority between humans and machines?

  • What organizational structures are appropriate for human-machine collaborative work?

    • Master-slave
    • Teammates
    • Principal-agent

  • How can dynamic models evolve in the presence of learning agents, both human and machine, and in the presence of inaccurate mental models.