This project is based on the use of formal methodologies
for the modelling and analysis of complex systems, which may involve
one or more of the following components: software, hardware,
humans, groupware and bioware.
This project will further extend the applicability of these
methodologies and tools, by involving quantitative analysis using
probabilistic model-checking and the integration between
model-checking and theorem-proving methodologies.
Particular emphasis is given at the concept of interaction,
which may involve software/hardware and humans/groupware (interactive systems),
or individual molecules or cells in biological systems.
In fact, interaction causes the emergence of system behaviours that
affect the evolution, safety and security of the overall system.
Interactive systems are characterised by complex patterns of
behaviours involving highly interleaved, concurrent, ongoing
cognitive activities (e.g., air traffic control) or determined
by social factors (e.g., collaborative systems, e-voting,
group authentication protocols).
Patterns of behaviours leading to security or safety failures
will be decomposed into more elementary patterns which can
be given a psychological interpretation.
Model-checking is used to verify the soundness and
completenss of the decomposition taxonomy.
Interaction in biological systems usually involves very
sophisticated mechanisms (e.g, the movement of molecules
across membranes), which cannot be easily modeled using the
low-level primitives offered by traditional process calculi.
On the other hand, the use of ad hoc calculi for the kind
of phenomenum under investigation is not a good practice in
a domain such as biology, where new kinds of phenomena are
frequently discovered.
The project involves the study of flexible
formalisms based on basic primitives that can be combined
together at a higher abstraction level to define sophisticated
operators suitable for describing new kinds of phenomena.
Analysis involves both qualitative aspects, such as
existence of stable states, and quantitative aspects, such as
the probability of reaching a certain state in a given time.
The project includes collaborations with: Bond University,
Australia; Queensland University of Technology, Australia;
the University of Queensland, Australia; University of Pisa,
Italy; CNR-ISTI, Italy; Queen Mary University London, UK;
the Interaction Centre of the University College London, UK.