| FME 2001 - Tutorials Programme |
|---|---|
| [ FME 2001 ] |
| Monday, 12th March |
NB: parallel event will be the AVIS'01 co-located workshop
9.00-12.30
Tutorial 1a
Title: SDL 2001 (Part 1)
Lecturers: J. Fischer, Andreas Prinz, Eckhardt Holz
(Humboldt-Universität zu Berlin, Institut für Informatik, Germany ;
DResearch Digital Media Systems GmbH, Otto-Schmirgal-Strasse 3,
D-10319 Berlin)
Abstract:
Detailed description available as a PDF file
9.00-12.30
Tutorial 2a
Title: Modelling for Formal Methods (Part 1)
Lecturers: Mícheál Mac an Airchinnigh,
Andrew Butterfield,
Arthur Hughes
(University of Dublin, Trinity College, Dublin, Ireland)
Abstract:
Detailed description available as a PDF file
12.30 - 14.00 Lunch
14.00-17.30
Tutorial 1b
Title: SDL 2001 (Part 2)
Lecturers: J. Fischer, Andreas Prinz, Eckhardt Holz
(Humboldt-Universität zu Berlin, Institut für Informatik, Germany ;
DResearch Digital Media Systems GmbH, Otto-Schmirgal-Strasse 3,
D-10319 Berlin)
Abstract:
Detailed description available as a PDF file.
14.00-17.30
Tutorial 2b
Title: Modelling for Formal Methods (Part 2)
Lecturers: Mícheál Mac an Airchinnigh,
Andrew Butterfield,
Arthur Hughes
(University of Dublin, Trinity College, Dublin, Ireland)
Abstract:
Detailed description available as a PDF file
NB: parallel event will be the IEEE 1394 (FireWire) workshop
9.00-12.30
Tutorial 3
Title: From UML to Z, a support for requirements engineering with RoZ
Lecturers: Yves Ledru, Sophie Dupuy (LSR/IMAG, France)
Abstract:
Semi-formal graphical formalisms like UML correspond today to one of the major support notations for requirements specification, especially in the field of information systems. In this tutorial, we will see how these notations can be integrated with formal notations like Z. The goal of this integration is to share the benefits of both approaches: (a) graphical formalisms provide an intuitive notation which eases the communication between the analyst and his customers; (b) they also fit in the standard process of many industrial companies; (c) formal methods bring precision to the specification; (d) this precision can be exploited by several tools in order to simulate, test or verify the specifications; such activities participate to the overall validation of the specifications.
Our basic technique for this integration is a set of translation rules. These help figuring out the limits of the graphical formalism and help structuring the annotations to these diagrams. They also provide the basis for tool support.
From a formal methods point of view, this approach eases the production of formal specifications: the graphical diagrams provide the structure of the specification and formal expression is reduced to local aspects of the specification (types, constraints, operations). This structure can also be exploited by formal analysis tools to enhance their automatic character.
The integration approach will be illustrated by the RoZ tool which integrates UML and Z, based on a commercial UML environment. With this environment, the analyst can develop a classical set of UML diagrams, and whenever needed can add precision with Z annotations. The result can automatically be translated into Z for further validation activities, like assessing some consistency properties (among others mutual consistency between views, implementability).
The tutorial will include a brief introduction to UML and Z, a detailed presentation of the integration of Z annotations in the UML class diagram, and illustration on case studies of the specification process and of the use of support tools.
The scientific basis of this tutorial has been published in KBSE'96, ASE'98, ZUM'98, CAiSE2000 and other conferences. It is also based on academic material taught for several years as an introductory course to formal methods.
12.30 - 14.00 Lunch
14.00-17.30
Tutorial 4
Title: Beyond Model Checking: Formal Specification and Verification
of Practical Mission-Critical Systems
Lecturers: Ramesh Bharadwaj
(Center for High Assurance Computer Systems,
Naval Research Laboratory,
Washington DC 20375, USA)
Abstract:
This tutorial introduces an industrial-strength specification notation and method for the formal specification and verification of systems, more specifically software-intensive embedded computer systems as typified by safety-critical applications in the avionics, biomedical, aerospace, railway, telecommunications, and automotive industries. Attendees will gain a basic understanding of the method for constructing precise and unambiguous specifications that are easy to understand and change, and that satisfy a number of application independent and application specific properties such as consistency, completeness, safety, and security. They will also gain an understanding of the issues involved in scalability, verifiability, modularity, readability, maintainability, implementability, etc., of formal specifications, and will be exposed to automated tools such as model checkers and theorem provers for verification and validation.
Beginning with an introduction to the theory and method underlying our approach, this tutorial will include a hands-on application of the method and tools to an embedded system derived from a practical domain (avionics).
(Further information)