Using JPF to efficiently compute workload in Multi-Agent Systems

No one likes to arrive at the airport only to realize that their flight has been delayed. Departure Sensitive Arrival Spacing (DSAS) is a new concept developed at NASA Ames Research Center that has been shown to improve flight scheduling, enabling more departing planes to leave the runway. In order to fully evaluate the concept, it’s necessary to thoroughly test its impact on the workload of the human operators. Java Pathfinder can be used to check for just such a property.