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.
Language Specifications (Relax NG)
Some examples can be found here
Research papers about EOFM can be found here
Translators (Java binaries)
Visualizer Tools (requires MS Visio)
Syntax Checking Tool
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)