Human-Computer Interaction Verification
In the context of critical applications, like autopilot in civil aviation, confusions occurring when using these can lead to dangerous situations. Human-Computer Interaction analysis follows system observability issues, abstraction and simulation which are well studied in the formal methods field. We are working on generating interfaces for critical systems, satisfying some controllability properties, using formal techniques.
LVL Members: Sébastien Combéfis, Charles Pecheur
External Partners: NASA Ames (Dimitra Giannakopoulou, Michael Feary)
Related Publications:
- A JavaPathfinder Extension to Analyse Human-Machine Interactions. Sébastien Combéfis?, Dimitra Giannakopoulou, Charles Pecheur, Peter Mehlitz. Java Pathfinder Workshop 2011.
- Learning System Abstractions for Human Operators. Sébastien Combéfis?, Dimitra Giannakopoulou, Charles Pecheur, Michael Feary. International Workshop on Machine Learning Technologies in Software Engineering.
- A Formal Framework for Design and Analysis of Human-Machine Interaction. Sébastien Combéfis?, Dimitra Giannakopoulou, Charles Pecheur, Michael Feary. 2011 IEEE International Conference on Systems, Man, and Cybernetics.
- A Bisimulation-Based Approach to the Analysis of Human-Computer Interaction. Sébastien Combéfis?, Charles Pecheur. ACM SIGCHI Symposium on Engineering Interactive Computing Systems, EICS 2009, Pittsburgh, PA.
- Operational Model: Integrating User Tasks and Environment Information with System Model. Sébastien Combéfis?. 3rd International Workshop on Formal Methods for Interactive Systems (FMIS 2009), Eindhoven, Netherlands.
Tags: -
Find It
Sections
Verification Diagnosis Autonomy ModelChecking Planning PDDL Requirements Testing LTL ThemeCoverage HumanComputerInteraction UserModel ProjectMOVES ThemeHMI LVL Website SymbolicModelChecking CTL Actions SMV EpistemicLogic ProjectNASA PartialOrderReduction BoundedModelChecking ThemePOR TemporalLogic Simulation Tools Tutorial Publication Equivalences