|
|
1. Software engineering and formal methods
|
|
Lecturer:
|
Antonio Cerone
|
|
|
IIST,
United Nations University,
Macau SAR China
|
|
[Abstract]
[Lecturer's Biography]
|
|
|
2. Formal verification of security protocols
|
|
Lecturer:
|
Siraj A. Shaikh
|
|
|
Department of Informatics and Sensors,
Cranfield University,
UK
|
|
[Abstract]
[Lecturer's Biography]
|
|
|
3. Formal methods for human-computer interaction
|
|
Lecturer:
|
Antonio Cerone
|
|
|
IIST,
United Nations University,
Macau SAR China
|
|
[Abstract]
[Lecturer's Biography]
|
|
|
4. Specification and verification of e-contracts
|
|
Lecturer:
|
Gerardo Schneider
|
|
|
Department of Informatics,
University of Oslo,
Norway
|
|
[Abstract]
[Lecturer's Biography]
|
|
|
5. Specification-based Testing of Embedded Systems
|
|
Lecturer:
|
Holger Schlingloff
|
|
|
Department
of Computer Science,
Humboldt University, Berlin,
Germany
|
|
[Abstract]
[Lecturer's Biography]
|
|
|
6. Algebraic Specification of Software and Hardware
|
|
Lecturer:
|
Markus Roggenbach
|
|
|
Department of Computer Science,
Swansea University,
UK
|
|
[Abstract]
[Lecturer's Biography]
|
|
|
COURSE ABSTRACTS
|
|
|
1. Software engineering and formal methods
|
The course will discuss the motivation and the importance of introducing formal methods
in the design and verification of systems
It will then present how to encorporate formal methods within software engineering
methodologies, especially for those application which are critical for safety
and security.
Finally the course will give a short introduction to some specific formal notations, such as
the CSP process algebra and Temporal Logics, as well as to formal verification techniques,
such as model-checking and theorem-proving, which will be extensively applied in the oher
courses.
Lecturer: Antonio Cerone
|
|
[Lecturer's Biography]
[Back to Course List]
|
|
|
2. Formal verification of security protocols
|
In an increasingly interconnected world, computer networks have become the bedrock for global communications and electronic commerce, giving birth to a need for a variety of security protocols. This in turn has placed great emphasis on the design and analysis of such protocols; a task which is error-prone and deceptive in nature. Formal approaches to analysing security protocols have developed into a comprehensive body of knowledge, building on a wide variety of formalisms and treating a diverse range of security properties. This course introduces the participants to one such approach by Schneider. This involves modelling security protocols using the process algebra CSP and verify them using Schneider’s rank functions approach.
The course will introduce the basic building blocks in CSP, describing notation and features relevant to the modelling of security protocols. The idea of rank functions is introduced with application to the verification of authentication properties. A variety of example protocols will be used to demonstrate the approach and the participants will be encouraged to engage in an exercise of modeling and analysis.
Lecturer: Siraj A. Shaikh
|
|
[Lecturer's Biography]
[Back to Course List]
|
|
|
3. Formal methods for human-computer interaction
|
The course will show model-checking-based methodologies for the formal specification and analysis of
human-computer interaction and will introduce tools to automate the verification process.
The formal analysis will focus on safety and security properties and on their relationship with
usability.
The methodology will be illustrated through simple examples and then applied to more complex case
studies from different application domains such as a groupware system and an air traffic control system.
Lecturer: Antonio Cerone
|
|
[Lecturer's Biography]
[Back to Course List]
|
|
|
4. Specification and verification of e-contracts
|
Internet-based applications like virtual organizations and web services usually communicate
through service exchanges. Such exchanges are subject to certain understanding on
the different roles the participants play, including assumptions on their correct and incorrect behaviours,
and their rights and obligations in order to avoid misunderstanding and ambiguities.
This motivates the need of establishing an agreement before any transaction is performed, through
a contract, guaranteeing the rights and duties of each signatory. Such documents may also contain
clauses determining penalties in case of contract violations, and be as unambiguous as possible to
avoid conflicting interpretations. In this tutorial we present how ideas from conventional contracts
may be used in software applications. We describe the problems and some solutions to the definition
and (formal) analysis of contracts stipulating the obligations, rights and prohibitions of the
different (service) signatories. We show how contracts could be used in the context of web
services and component-based applications.
Lecturer: Gerardo Schneider
|
|
[Lecturer's Biography]
[Back to Course List]
|
|
|
5. Specification-based testing of embedded systems
|
Embedded systems are the basis for the computer revolution of the 21st
century. As computers start to interact with the environment via
actuators and sensors, a wealth of new applications becomes possible.
However, there are new challenges for the design and validation of such
systems, especially in safety-critical applications. In this course, we
describe formal methods for specifying the intended behaviour of
embedded systems, model-based development and model checking for
assessing the correctness of the design, and automated test generation
algorithms for hardware-in-the-loop testing of control devices.
All theoretical concepts are supported by practical examples from
industrial projects in aerospace, automotive, rail and medical systems.
Lecturer: Holger Schlingloff
|
|
[Lecturer's Biography]
[Back to Course List]
|
|
|
6. Algebraic specification of software and hardware
|
The course introduces standard techniques of Algebraic Specification in a
problem driven way. To this end, various examples (telephone directory,
logical gates, a simple von Neumann computer, sorting algorithms, etc. )
are modelled using the language
CASL, which is the
current de facto standard in algebraic specification. Online examples for
learning-by-doing and the use of automated theorem proving tools provide
practical insight.
Lecturer: Markus Roggenbach
|
|
[Lecturer's Biography]
[Back to Course List]
|
|
|
LECTURERS' BIOGRAPHIES
|
|
|
Antonio Cerone
joined the International Institute for
Software Technology (IIST) of the United Nations University (UNU)
as a Research Fellow in February 2004.
His 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.
|
|
[Course Abstract]
[Back to Course List]
|
|
|
Markus Roggenbach
is a lecturer of Computer Science in the School of
Physical Sciences at Swansea University, Wales, United Kingdom. He studied
Mathematics and Computer Science in Braunschweig and Karlsruhe. He
received his Ph.D. with a dissertation on "Abstract Characterizations of
Bisimulation" from Mannheim University. As a post-doc in Bremen, he
actively participated in the international Common Framework Initiatiative
for algebraic specification and development of software. In 2003, he moved
to Swansea, where he built up a research group on "Processes and Data".
His research activities concern the modelling, verification, and
validation of distributed systems. His interests span over semantics,
logics, design of specification languages, interactive theorem proving,
testing, formal methods and their industrial applications, with the main
focus on algebraic specification and process algebra. In 2008, he became a
member of the IFIP WG 1.3 Foundations of System Specification.
|
|
[Course Abstract]
[Back to Course List]
|
|
|
Holger Schlingloff
is professor of software engineering at Humboldt
University, Berlin, and at the same time scientific leader of the
embedded systems group at the Fraunhofer Institute for Computer
Architecture and Software Technology. He studied computer science at the
TU Munich and received his Ph.D. with a dissertation "On the temporal
logic of trees". The, he became manager of the Bremen Institute for Safe
Systems in the Technologie-Zentrum Informatik at Bremen university.
After his habilitation (on "Partial state space analysis of
safety-critical systems") in 2002 he moved to Berlin. His current
interests include specification formalisms, model-based design methods,
theory of testing, and the application of formal methods to real-world
problems.
|
|
[Course Abstract]
[Back to Course List]
|
|
|
Gerardo Schneider
holds a Ph.D. degree in Computer Science from the VERIMAG laboratory, University of Grenoble I (France). Before starting his Ph.D. studies, Gerardo was a research fellow at UNU/IIST where he worked with formal semantics using Duration Calculus.
He joined the University of Oslo in 2005, and previously he was a researcher at INRIA/IRISA (France) and Uppsala University (Sweden) working on different topics related to formal verification of distributed and real-time systems. His current research is focused on the representation and analysis of contracts in the context of the project "COSoDIS: Contract-Oriented Software Development for Internet Services".
|
|
[Course Abstract]
[Back to Course List]
|
|
Siraj
Ahmed Shaikh
is a Research Officer at the Department of Informatics and Sensors, Cranfield University (UK). Previously he has been a Postdoctoral Research Fellow at the United Nations University-International Institute of Software Technology (UNU-IIST) in Macau SAR China. His main areas of interests are computer and network security. His research has looked at formal analysis, design and performance analysis of security protocols, intrusion detection and computer science education.
He completed his MSc in Computer Networking in 2001 and his PhD in 2006. He is a Member of the Working Group 6.9: Communication Systems for Developing Countries - Technical Committee on Communication Systems (TC6) of the International Federation for Information Processing (IFIP), and also a Member of the British Computer Society (MBCS).
|
|
[Course Abstract]
[Back to Course List]
|
|
