Poorly designed interfaces can pose a major danger to users in systems where safety is a key concern — for example, many inadequately created medical devices, which have rectifiable designs, have led to unnecessary fatalities. This research project is focused on modelling these complex systems of human machine interaction with finite state machines, and using them to better understand how we can eliminate unsafe behaviour. To do so, we first model and simplify complex systems and possible human interactions with them into finite state processes. We then systematically inject errors into correct models based on common human errors with the goal of violating certain safety properties. By examining the case study of an infusion pump whose combined model contains fewer than 100 states, we were able to produce 545 new machines, of which 17 led to safety violations. This demonstrates that we can reliably model and replicate some of the common mistakes that humans make when interacting with machines. The primary focus of future work is to then modify the model of the machine such that it will safeguard against such human errors.
Compile the code with cmake in standard fashion. Requires boost library -- may need to update
paths in CMakeLists.txt for this dependency.
Then run ./Verif to execute demo code, which will use modify an infusion
pump example.
Finite state machines are implemented as DFA's. Finite state machines are essentially directed
graphs, so the core of the implementation is a transition matrix. At index [t,s] of the matrix
contains the state s' reached from state s via transition t. Transitions are named via strings.
Properties are defined as DFAs as well. The key addition is that there is also a set of error states. Whenever such an error state is reached, the property will be considered to be violated. Here, there is also an algorithm to verify properties of a given state machine. The algorithm used is to build the set of reachable states in the union of the machine and the property. That is, on some transition t, we make progress in both the representations of the machine and property, if possible. If any error state is ever reached, then this would indicate a property violation.
Everything pertaining to modification is included here. The first key component is infrastructure for mappings. A mapping is a ordered pair of patterns, where the first represents correct human behaviour while the second represents that same behaviour but after a mistake is made. The other key component is the modification algorithm itself. The algorithm will loop through all possibilities of instances of patterns in a provided list of mappings. For any new machines which now violate a safety property, it is saved to a file and counted.
The pattern library includes a bunch of small state machines each representing a common human error. This will return a list of mappings, described earlier.
This is a simple tool created to parse output generated by the LTSA tool. In the ltsa tool, view the textual representation of the transitions after compiling. The parser will generate a DFA in the format of this project based on the input. This portion has not been tested robustly.