论文部分内容阅读
A formal methodology is proposed to reduce the amount of information displayed to remote human operators at interfaces to large-scale process control plants of a certain type.The reduction proceeds in two stages.In the first stage,minimal reduced subsets of components,which give full information about the state of the whole system,are generated by determining functional dependencies between components.This is achieved by using a temporal logic proof obligation to check whether the state of all components can be inferred from the state of components in a subset in specified situations that the human operator needs to detect,with respect to a finite state machine model of the system and other human operator behavior.Generation of reduced subsets is automated with the help of a temporal logic model checker.The second stage determines the interconnections between components to be displayed in the reduced system so that the natural overall graphical structure of the system is maintained.A formal definition of an aesthetic for the required subgraph of a graph representation of the full system,containing the reduced subset of components,is given for this purpose. The methodology is demonstrated by a case study.
A formal methodology is proposed to reduce the amount of information displayed to remote human operators at interfaces to large-scale process control plants of a certain type. The reduction proceeds in two stages. In the first stage, minimal reduced subsets of components, which give full information about the state of the whole system, are generated by determining functional dependencies between components. This is achieved by using a temporal logic proof obligation to check whether the state of all components can be inferred from the state of components in a subset in specified situations that the human operator needs to detect, with respect to a finite state machine model of the system and other human operator behavior. Generation of reduced subsets is automated with the help of a temporal logic model checker. The second stage determines the interconnections between components to be displayed in the reduced system so that the natural overall graphical structure of the system is maintained ormal definition of an aesthetic for the required subgraph of a graph representation of the full system, containing the reduced subset of components, is given for this purpose. The methodology is demonstrated by a case study.