TY - GEN
T1 - Cognitive Aspects in the Formal Modelling of Multi-party Human-Computer Interaction
AU - Cerone, Antonio
AU - Zhalgendinov, Olzhas
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.
PY - 2026
Y1 - 2026
N2 - The unpredictability of human behaviour makes formal analysis of human-computer interaction (HCI) already difficult when one single user is interacting with one computer system. However, nowadays interaction normally involves several users, i.e., human components, interacting simultaneously with separate interfaces which communicate with and/or act upon the same computer resources. Independently of whether human components aim at using computer resources to communicate with each other or to concurrently act upon and modify stored information, interfaces should be designed in order to protect users from the potential negative effects caused by the behaviour of other users. In this research paper, we define a framework that combines the formal modelling of cognitive aspects of human components and the modelling of the actual computer system into an overall model that can be formally analysed using model-checking. We use the Behaviour and Reasoning Description Language (BRDL) to model human cognition and implement our framework using Real-time Maude, whose model-checker is then used to carry out formal verification.
AB - The unpredictability of human behaviour makes formal analysis of human-computer interaction (HCI) already difficult when one single user is interacting with one computer system. However, nowadays interaction normally involves several users, i.e., human components, interacting simultaneously with separate interfaces which communicate with and/or act upon the same computer resources. Independently of whether human components aim at using computer resources to communicate with each other or to concurrently act upon and modify stored information, interfaces should be designed in order to protect users from the potential negative effects caused by the behaviour of other users. In this research paper, we define a framework that combines the formal modelling of cognitive aspects of human components and the modelling of the actual computer system into an overall model that can be formally analysed using model-checking. We use the Behaviour and Reasoning Description Language (BRDL) to model human cognition and implement our framework using Real-time Maude, whose model-checker is then used to carry out formal verification.
KW - Behaviour and Reasoning Description Language
KW - Formal Analysis
KW - Human Cognition
KW - Human-computer Interaction
KW - LTSs
UR - https://www.scopus.com/pages/publications/105014335639
UR - https://www.scopus.com/inward/citedby.url?scp=105014335639&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-94748-3_14
DO - 10.1007/978-3-031-94748-3_14
M3 - Conference contribution
AN - SCOPUS:105014335639
SN - 9783031947476
T3 - Lecture Notes in Computer Science
SP - 165
EP - 181
BT - Software Engineering and Formal Methods. SEFM 2024 Collocated Workshops - ReacTS 2024 and CIFMA 2024, Revised Selected Papers
A2 - Proença, José
A2 - Fervari, Raul
A2 - Martins, Manuel A.
A2 - Kahle, Reinhard
A2 - Pluck, Graham
PB - Springer Science and Business Media Deutschland GmbH
T2 - 22nd International Conference on Software Engineering and Formal Methods, SEFM 2024, Collocated Workshops, International Workshop on Reconfigurable Transition Systems: Semantics, Logics and Applications, ReacTS 2024 and 6th International Workshop on Cognition: Interdisciplinary Foundations, Models and Applications, CIFMA 2024
Y2 - 4 November 2024 through 5 November 2024
ER -