Software/system verification aims to assure that a software application or a computer system fully satisfies all the expected requirements.

Formal verification uses mathematical techniques and tools to achieve such a goal in a very rigorous way, by formalizing the requirements as properties expressed in some logic formalism anc checking whether such properties are verified by a formal model of the software/system. However, although a software application or a computer system appear to work correctly and safely when analysed in isolation from the human environment in which it is supposed to work, things may still go wrong when the application/system works in interaction with human operators or users. In fact, the same cognitive skills that enable humans to perform complex tasks may also become the source of critical errors in the interaction with systems and devices designed as supports for such tasks. It is thus essential to verify the desired properties of an interactive system using a model that not only includes a user-centered description of the task, but also incorporates a representation of human cognitive processes within the task execution.

A cognitive architecture has to be intended as a comprehensive model of the human mind, with a computational power that supports the insilico replication of experiments carried out in cognitive psychology as well as some form of prediction and analysis. A cognitive architecture is based on and implements a theory of cognition, which conceptulizes the structure of mind in terms of its processing and storage components and the way such components work together to produce human thinking and behaviour.

CAFAISHA (Cognitive Architecture for the Formal Analysis of Interactive Systems and Human Activities) is a cognitive architecture for the modelling of automatic and deliberate human behaviour as it occurs and evolves in a living environment as well as in interaction with machine interfaces. It features an environment that supports timed modelling, a spatial topology consisting of an arbitrary number of systems, interfaces and human components, a model of short-term memory that includes closure, decay and chunking, and a model of long-term memory that evolves throughout the time by exploiting experiences to build new knowledge about the interaction, thus mimicking the creation of expectations and mental models. CAFAISHA can be used for modelling and analysing interactive systems and human activities as well as exploring alternative cognitive theories, such as different models of the closure phenomenon, using the same set of real-life examples in order to understand which one appears to best match real data. Formal analysis is carried out using model-checking

Research carried out by Antonio Cerone