Formal Modelling and Analysis of Cyber-Social Systems

Computer systems have evolved from standalone systems, over networked systems, to cyber-physical systems. In all stages, human operators have been essential for the functioning of the system and for understanding system messages. Recent trends make human actors an even more central part of computer systems, resulting in what we call "cyber-social systems". In cyber-social systems, human actors and their interaction with a system are essential for the state of the system and its functioning. Both the system's operation and the human's operating it are based on an assumption of each other's behaviour. Consequently, an assessment of the state of a system must take the human actors and these interactions into account. Attacks on systems and organisations increasingly exploit human actors, for example through social engineering. This non-technical aspect of attacks complicates their formal treatment and automatic identification. Formalisation of human behaviour is difficult at best, and attacks on cyber-social systems are still mostly identified through brainstorming of experts. In this work we discuss several approaches to formalising socio-technical systems and their analysis. We discuss how to include the "socio aspects" explicitly, and show a formalisation that proves properties of this formalisation. Our work closes the gap between formal and informal approaches to socio-technical systems. To represent human behaviour, we introduce behavioural trees, which combine representations of behaviour with causal effects of external and internal events.