Formal analysis and design of supervisor and user interface allowing for non-deterministic choices using weak bi-simulation

Abstract

In human machine systems, a user display should contain sufficient information to encapsulate expressive and normative human operator behavior. Failure in such system that is commanded by supervisor can be difficult to anticipate because of unexpected interactions between the different users and machines. Currently, most interfaces have non-deterministic choices at state of machine. Inspired by the theories of single user of an interface established on discrete event system, we present a formal model of multiple users, multiple machines, a supervisor and a supervisor machine. The syntax and semantics of these models are based on the system specification using timed automata that adheres to desirable specification properties conducive to solving the non-deterministic choices for usability properties of the supervisor and user interface. Further, the succinct interface developed by applying the weak bi-simulation relation, where large classes of potentially equivalent states are refined into a smaller one, enables the supervisor and user to perform specified task correctly. Finally, the proposed approach is applied to a model of a manufacturing system with several users interacting with their machines, a supervisor with several users and a supervisor with a supervisor machine to illustrate the design procedure of human-machine systems. The formal specification is validated by z-eves toolset.