Enhanced Operator Function Model (EOFM) and EOFM with Communications
(EOFMC)
The enhanced
operator function model (EOFM) is a task analytic modeling formalism that
allows human behavior to be included in larger formal system models to support
the formal verification of human interactive systems. EOFM is an expressive
formalism that captures the behavior of individual humans or, with the EOFM
with communications (EOFMC) extension, teams of humans as a collection of
tasks, each composed representing a hierarchy of activities and actions.
Further, EOFM has a formal semantics and associated translator that allow its
represented behavior to be automatically translated into a model checking
formalism for use in larger system verification. EOFM supports a number of
features that enable analysts to use model checking to investigate
human-automation and human-human interaction. Translator variants support the
development of different task models with methods for accounting for erroneous
human behaviors and miscommunications, the creation of specification
properties, and the automated design of human-machine interfaces.
Below you
will find various resources and tools that will allow you to use EOFM and EOFMC
in your own analyses.
NOTE: This page is currently under
development. Please check back regularly for updates.
Disclaimer: This SOFTWARE PRODUCT is provided by
THE PROVIDER "as is" and "with all faults." THE PROVIDER
makes no representations or warranties of any kind concerning the safety,
suitability, lack of viruses, inaccuracies, typographical errors, or other
harmful components of this SOFTWARE PRODUCT. There are inherent dangers in the
use of any software, and you are solely responsible for determining whether
this SOFTWARE PRODUCT is compatible with your equipment and other software
installed on your equipment. You are also solely responsible for the protection
of your equipment and backup of your data, and THE PROVIDER will not be liable
for any damages you may suffer in connection with using, modifying, or
distributing this SOFTWARE PRODUCT.
Contact
Matthew L. Bolton,
Ph.D. (mbolton at buffalo.edu)
Assistant Professor
Department of Industrial and Systems Engineering
University at Buffalo, State University of New York
http://fhsl.eng.buffalo.edu/
Language Specifications (Relax NG)
Documentation
Some
examples can be found here
Research
papers about EOFM can be found here
Translators (Java binaries)
EOFM
with Property Generation and Erroneous Behavior Generation
EOFMC with Miscommunication
Generation
EOFMC with Task-based
Erroneous Behavior Generation (also compatible with EOFM)
Visualizer Tools (requires MS Visio)
Syntax Checking Tool
Links
The Formal Human Systems Lab (the
laboratory of Matthew L. Bolton)
The Symbolic Analysis Laboratory (used for EOFM
formal verification analyses)
The oXygen XML
Editor (a really sophisticated XML editor that can be used to create and
edit EOFM and EOFMC files)