|
|
ABSTRACTS
|
Model-checking in Human-computer Interaction
|
This tutorial will start by briefly introducing some fundamental
concepts in Human-Computer Interaction (HCI) which draw particularly on the
contributions of psychology, cognitive science and sociology.
Then it will focus on Finite State Machines as a modelling formalism and
on model-checking as a verification tool.
It will explore how to build a formal model of the user's cognitively
plausible behaviour and how to use such a model to drive the design of the
computer part of the system by using model-checking as a debuggning tool.
This approach will be illustrated using a groupware system as a case study.
Model-checking will be used
- to capture the emergence of user errors in the overall system that
results from the composition of the user model with the system model;
- to show how these errors may affect the security of the system; and
- to show how the system may be improved by introducing safeguardes
which do not compromise the usability of the system.
This methodology can capture and contribute to correct errors that
cause the overall system to reach an erroneous state.
However, safety and security violation are often due to complex
patterns of user behaviour that cannot be represented as a global
error state.
Therefore a second part of the tutorial will show how observable
failures caused by these erroneus patterns of behaviour can be
expressed using temporal logic formulae.
These formulae can then be decomposed into other formulae that
characterise basic user patterns of behaviour, which directly
correspond to the user's mental processes which caused the failure.
Model-checking is used at this point to verify the soundness and
completeness of the decomposition.
This approach will be illustrated first using an air traffic control
system as the case study.
Presented by Antonio Cerone
|
|
[Presenters's Biography]
[Back to Top]
|
Retrenchment
|
Part I
- Overview of refinement and its success stories.
- Some refinement troublespots, and the introduction of retrenchment.
- Basic properties of retrenchment.
- Interaction of retrenchment and refinement.
- The Tower Pattern.
Part II
- Overview of the Mondex Electronic Purse.
- The Mondex Retrenchment Opportunities.
- The Sequence Number Retrenchment.
- The Exception Log Retrenchment.
- The Hash Function Retrenchment.
- The Balance Enquiry Retrenchment.
Presented by Richard Banach
|
|
[Presenters's Biography]
[Back to Top]
|
Formal Methods for Service-oriented Systems
|
This tutorial presents an introduction to a formal framework that is being
developed within the EU SENSORIA project for supporting service-oriented
modelling at high levels of abstraction, i.e. independently of the hosting
middleware and hardware platforms, and the languages in which services are
programmed.
More specifically, we give an account of the concepts and techniques that
support SRML ? the SENSORIA Reference Modelling Language.
This includes a logic for the specification of conversational interactions, an
algebraic semantics of composition, and a constraint-based semantics of service
level agreements.
A case study will be used for illustrating the primitives of
SRML and the methodology that is being developed within the project.
Presented by José Luiz
Fiadeiro
|
|
[Presenters's Biography]
[Back to Top]
|
|
|
BIOGRAPHIES
|
Richard Banach
|
|
University of Manchester,
UK
|
Richard Banach received a Ph.D. in Theoretical Physics, in 1979 from
Manchester University. In 1982 he joined ICL, working on the ICL 3980
mainframe. In 1986 he joined Manchester University Computer Science
Department working with the Alvey Flagship Project which designed a
complete novel system architecture. Subsequently he became more concerned
with the theory of graph rewriting, working on semantic models for the
MONSTR language, and other issues connected with graph rewriting semantics.
More recently he became interested in the development of formal abstract
models towards implementation, particularly in situations in which the
standard theories of refinement prove to be too exacting to capture the
realities of the development. (Examples include large real world
applications, and engineering applications which start from a continuous
physical model.) This spawned the introduction of retrenchment, a loosening
of the proof obligations of refinement to accomodate the realities of such
developments. The theory and applications of retrenchment remain his main
research interests at present.
|
|
[Tutorial Abstract]
[Back to Top]
|
Antonio Cerone
|
|
UNU-IIST,
Macau SAR China
|
Antonio Cerone joined the International Institute for Software Technology (IIST) of the United Nations University (UNU) as a Research Fellow in February 2004.
Before joining the UNU-IIST, Antonio held research positions at the University of Queensland,
the Advanced Computing Research Centre (ACRC) of the University of South Australia
and the University of Frankfurt.
Antonio completed his PhD in 1993 and his Master's degree in 1989, both at the University of Pisa.
He is currently Chairman of the Steering Committee of the IEEE International Conference on Software
Engineering and Formal Methods (SEFM).
Antonio's research focuses on the use of formal methods in verification of software and hardware,
and in modelling cognitive human behaviour. He is particularly interested in the verification of interactive systems, security systems, safety-critical systems, asynchronous hardware and concurrent and real-time systems.
Recently he has also developed interests in human cognitive development and in education and
pedagogy of mathematics and computer science.
|
|
[Tutorial Abstract]
[Back to Top]
|
José Luiz
Fiadeiro
|
|
University of Leicester,
UK
|
|
José Luiz Fiadeiro joined the University of Leicester as Professor of
Software Science and Engineering after having held previous academic
positions in Lisbon, and visiting research positions at Imperial College,
King's College London, PUC-Rio de Janeiro, and the SRI International.
He is chairman of the IFIP WG 1.3 (Foundations of System Specification)
and co-chairman of the Steering Committee of the Conference on Algebra and
Co-algebra in Computer Science (CALCO). His most recent work has focused
on the design principles and theories that support the engineering of complex
software-intensive systems, including the role of architectural primitives and
modelling techniques, the impact of coordination mechanisms in software evolution,
and the methodological and scientific challenges raised by service-oriented computing. |
|
[Tutorial Abstract]
[Back to Top]
|
