UCLIC Research Seminar Series
Abstract: Formal Methods are successfully used in the verification of interactive systems, especially
for safety-critical properties. However, formal approaches are normally applied in an ad hoc manner
to restricted application domains or even just to specific case studies. Although a large numbers of cognitive
architectures have been developed during the last decades, such comprehensive, computational models of
the human mind are short of being integrated in the system and software verification process.
In this seminar, we propose a simple language to describe human tasks, which is interpreted by a cognitive
architecture implemented using the Maude rewrite system, thus supporting formal verification via Maude model checker.
The cognitive architecture may be instantiated into several users, who interact with an environment consisting
of a network of software and physical components, which can be modeled using a number of formal approaches.
In addition, we show that our approach goes beyond formal verification and supports also the validation of the
formal model of the system using real-life datasets. Finally, we show that such methodology may also be applied to the validation of research hypotheses that relate user's typology or characteristics and user's cognition.
Antonio Cerone is an Associate Professor of Computer Science of the School of Science and Technology
at Nazarbayev University. He obtained his Masters Degree in Information Science and his PhD degree in
Computer Science from the University of Pisa. Before joining NU he worked at the Goethe University
Frankfurt, the University of South Australia, The University of Queensland, the United Nations University
and the IMT School for Advanced Studies Lucca. He still holds a visiting position at the University of Pisa.
Antonio's research interests focus on the use of formal methods in various application domains:
human-computer interaction, software engineering, data-driven modelling, systems biology and ecology.
Further research areas include: cognitive science, process mining and conformance analysis, analysis of
Free/Libre Open Source Software (FLOSS) communities and development, collaborative learning.
Antonio is the founder and chair of the steering committee of the International Conference on Software
Engineering and Formal Methods (SEFM) and founder and steering committee member of the International
Symposium "From Data to Models and Back" (DataMod).