Formal Analysis and Design of Supervisor and User Interface Allowing for Non-Deterministic Choices Using Weak Bi-Simulation
Source abstract
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.
Source: crossref · Quality: baseline
Research context
OpenAlex topics: Human-Automation Interaction and Safety · Flexible and Reconfigurable Manufacturing Systems · Healthcare Technology and Patient Monitoring
SciVX discovery tags are terminology-based. OpenAlex topics are source-provided classifications.
Affiliations
Department of Industrial and Information Engineering, Hanyang University, ERICA Campus, Ansan 15588, Korea
Department of Mechanical Engineering, Hanyang University, ERICA Campus, Ansan 15588, Korea
Funding
Hanyang University
References (36)
Show source-provided references
1. Human resource strategies for effective introduction of advanced manufacturing technologies (AMT)
2. Weyers, B., Bowen, J., Dix, A., and Palanque, P. (2017). The Handbook of Formal Methods in Human-Computer Interaction, Springer.10.1007/978-3-319-51838-1 ↗
3. Model-based verification method for solving the parameter uncertainty in the train control system10.1016/j.ress.2015.09.014 ↗
4. Using affective human–machine interface to increase the operation performance in virtual construction crane training system: A novel approach10.1016/j.autcon.2010.10.005 ↗
5. A systematic approach to model checking human–automation interaction using task analytic models10.1109/TSMCA.2011.2109709 ↗
6. Ubiquitous manufacturing system based on Cloud: A robotics application10.1016/j.rcim.2016.01.007 ↗
7. A Manufacturing Big Data Solution for Active Preventive Maintenance10.1109/TII.2017.2670505 ↗
8. An apprenticeship approach for the development of operations automation knowledge bases10.1177/154193120004400162 ↗
9. Guest Editorial Special Section on Human-Centered Automation10.1109/TASE.2015.2503538 ↗
10. Meisels, I., and Saaltink, M. (1997). The Z/EVES Reference Manual (for Version 1.5), ORA. Reference Manual TR-97-5493-03.
11. Woodcock, J., and Davies, J. (1996). Using Z: Specification, Refinement, and Proof, Prentice Hall Englewood Cliffs.
12. Maynard, M. (2015). Issue: Global Manufacturing Global Manufacturing, Sage Businessresearcher.
13. Foot placement during error and pedal applications in naturalistic driving10.1016/j.aap.2016.10.019 ↗
14. Degani, A., and Kirlik, A. (1998, January 22–25). Describing the design contributors to mode error. Proceedings of the Fourth Annual Symposium on Human Interaction with Complex Systems, Dayton, OH, USA.
15. Wickens, C.D. (1999). Automation in air traffic control: The human performance issues. Automation Technology and Human Performance, Lawrence Erlbaum Associates.
16. Extracting usability information from user interface events10.1145/371578.371593 ↗
17. A usability study of a critical man–machine interface: Can layperson responders perform optimal compression rates when using a public access defibrillator with automated real-time feedback during cardiopulmonary resuscitation?10.1109/THMS.2016.2561267 ↗
18. Formal verification of human-automation interaction10.1518/0018720024494838 ↗
19. Suzuki, A., Ushio, T., and Adachi, M. (2006, January 18–21). Detection of automation surprises in discrete event systems operated by multiple users. Proceedings of the International Joint Conference, SICE-ICASE, Busan, Korea.10.1109/SICE.2006.315283 ↗
20. Design of user-interface without automation surprises for discrete event systems10.1016/j.conengprac.2006.02.008 ↗
21. Human factors in process control systems: The design of human–machine interfaces10.1016/j.ssci.2005.09.003 ↗
22. The role of human-automation consensus in multiple unmanned vehicle scheduling10.1177/0018720810368674 ↗
23. Clarke, E.M., Grumberg, O., and Peled, D. (1999). Model Checking, MIT Press.
24. A model for types and levels of human interaction with automation10.1109/3468.844354 ↗
25. Shared steering control between a driver and an automation: Stability in the presence of driver behavior uncertainty10.1109/TITS.2013.2248363 ↗
26. Formal analysis and automatic generation of user interfaces: Approach, methodology, and an algorithm10.1518/001872007X312522 ↗
27. Argos: An advanced in-vehicle data recorder on a massively sensorized vehicle for car driver behavior experimentation10.1109/TITS.2010.2046323 ↗
28. A model for discrimination and prediction of mental workload of aircraft cockpit display interface10.1016/j.cja.2014.09.002 ↗
29. Gachui, N.A. (2016). Wizard Navigation Functionality to Automated User Interfaces Using Finite State Machines. [Master’s Thesis, Jomo Kenyatta University of Agriculture and Technology].
30. Wonham, W.M. (2015). Supervisory control of discrete-event systems. Encyclopedia of Systems and Control, Springer.10.1007/978-1-4471-5058-9_54 ↗
31. Milner, R. (1989). Communication and Concurrency, Prentice Hall.
32. De Moura, L., Owre, S., and Shankar, N. (2003). The SAL language manual. Computer Science Laboratory, SRI International. Technical Report CSL-01-01.
33. Shankar, N. (2000, January 19–24). Symbolic Analysis of Transition Systems. Proceedings of the International Workshop on Abstract State Machines, Theory and Applications, London, UK.10.1007/3-540-44518-8_16 ↗
34. Lin, Y.-D., Liao, F.-Z., Huang, S.-K., and Lai, Y.-C. (2015, January 21–24). Browser fuzzing by scheduled mutation and generation of document object models. Proceedings of the 2015 International Carnahan Conference on Security Technology (ICCST), Taipei, Taiwan.10.1109/CCST.2015.7389677 ↗
35. Automatically generating specification properties from task models for the formal verification of human–automation interaction10.1109/THMS.2014.2329476 ↗
36. Using model checking to explore checklist-guided pilot behavior10.1080/10508414.2012.718240 ↗