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.



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


Language Specifications (Relax NG)





A Pedagogic Paper

A Pedagogic Book Chapter

Basic Tutorial

EOFM Syntax

EOFM to SAL Translation

Installing SAL on Windows

Running the EOFM Visualizer

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





The Formal Human Systems Lab (the laboratory of Matthew L. Bolton)

Ellen J. Bass

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)