Invited Speakers
| Prof. Egon Boerger, University of Pisa, Italy |
| Contribution to a Rigorous Analysis of Web Application Frameworks |
| Abstract: We suggest an approach for accurate modeling and analysis of web application frameworks. |
| Prof. Muffy Calder, University of Glasgow, United Kingdom - FME invited speaker |
| Process Algebra for Event-Driven Runtime Verification: a case study of wireless network management |
| Abstract: TBA |
| Prof. Ian J. Hayes, University of Queensland, Australia |
| Integrated operational semantics: small-step, big-step and multi-step |
| Abstract: Plotkin’s structural operational semantics provides a tried and tested method for defining the semantics of a programming language via sets of rules that define valid transitions between program configurations. Mosses’ modular structural operational semantics (MSOS) recasts the approach by making use of rules consisting of labelled transitions, allowing a more modular approach to defining language semantics. MSOS can be adapted by using "syntactic" labels that allow local variables and aliasing to be defined without augmenting the semantics with environments and locations. The syntactic labels allow both state-based constructs of imperative languages and event-based constructs of process algebras to the specified in an integrated manner. To illustrate the integrated approach we compare its rules with Plotkin’s original rules for both small-step and big-step operational semantics. One issue that arises is that defining concurrency requires the use of a small-step approach to handle interleaving, while defining a specification command requires a big-step approach. The integrated approach can be generalised to use a sequence of (small) steps as a label; we call this a multi-step operational semantics. This approach allows both concurrency and non-atomic specification commands to be defined. |
TUTORIALS 18 JUNE
MORNING
Practical Predicative Programming Primer by
Eric C.R. Hehner, Department of Computer Science, University of Toronto
Eric Hehner joined the faculty of the University of Toronto in 1974, becoming a full professor in 1983, and Bell University Chair in Software Engineering in 2001. His research has been mainly on the subject of formal programming methods, particularly the mathematics of program construction. He is the first winner of the annual Computer Science undergraduate teaching award. He has been a Visiting Scientist at Xerox Research Center, Palo Alto, a Visiting Fellow at Oxford University, a Visiting Researcher at the University of Texas, Austin, a Professeur Invité at the Université de Grenoble, a Visiting Professor at UBC, Vancouver, and at the University of Southampton. He is a member of IFIP Working Group 2.1 on Algorithmic Languages and Calculi, and IFIP Working Group 2.3 on Programming Methodology. He is an editor of Acta Informatica and of Formal Aspects of Computing. He has written two books "the Logic of Programming", Prentice-Hall, 1984, and "a Practical Theory of Programming", first edition Springer-Verlag 1993, current edition online, and many journal and conference papers. He has given well over a hundred invited lectures at institutions around the world. He has taught short courses in Marktoberdorf Germany, Macau China, Turku Finland, and Tandil Argentina. His students have gone on to head major corporations and departments of computer science.
Abstract:
The tutorial will introduce Netty, a tool to assist in the construction of calculational proofs, including refinement from specifications to programs. The tutorial will also teach the fundamentals of predicative programming, moving on to advanced topics if time permits.
Topics:
- Netty: a calculational proof assistant
- specification and refinement
- standard language constructs
- data refinement
- concurrency
- interactive variables
- communication channels
- probabilistic programming
Background:
The material comes from the book "a Practical Theory of Programming", which will be provided free at the tutorial.
AFTERNOON
Safety, Dependability and Performance Analysis of Extended AADL Models by
Joost-Pieter Katoen He is a full professor for Computer Science at RWTH Aachen University. His research interests include concurrency theory, model checking, timed and probabilistic systems, and semantics. He coauthored more than 100 journal and conference papers, and recently published a comprehensive book (with Christel Baier) titled Principles of Model Checking.
Thomas Noll He is a docent for Computer Science at RWTH Aachen University. He is working on formal models and verification methods for hardware/software systems, and has published more than 50 papers in that area.
Alessandro Cimatti He is senior research scientist at Fondazione Bruno Kessler (FBK; Trento, Italy). He is the leader of the Research Unit on Embedded Systems (ES) of the Center for Information and Communication Technology of FBK. His research interests include model checking, timed and hybrid systems, and satisfiability modulo theory. He coauthored over 80 papers in international conferences and journals, and has led several technology transfer projects on the application of formal methods to the design of safety critical systems.
Marco Bozzano He is senior research scientist, working in the ES Research Unit of the Center for Information and Communication Technology of FBK. His research interests include model checking and formal safety analysis. He coauthored more than 30 journal and conference papers, and one book (with Adolfo Villafiorita) titled Design and Safety Assessment of Critical Systems (CRC Press - Taylor & Francis Group, November 2010).
Abstract:
This tutorial presents a component-based modeling approach to system-software co-engineering of real-time embedded systems, in particular aerospace systems. Our method is centered around the standardized Architecture Analysis and Design Language (AADL) modeling framework. Taking the core features of AADL and its recent Error Model Annex, we have set up a modeling framework that supports a variety of system analysis and verification methods. Its major distinguishing aspects are the possibility to describe hardware and software components and its nominal operations, hybrid (and timing) aspects, as well as probabilistic faults and their propagation and recovery. Moreover, it supports dynamic (i.e., on-the-fly) reconfiguration of components and inter-component connections. The operational semantics gives a precise interpretation of specifications by providing a mapping onto networks of event-data automata. These networks are then subject to different kinds of formal analysis such as model checking, safety and dependability analysis, and performance evaluation. We demonstrate tool support realizing these analyses and report on industrial case studies that have been carried out in the context of aerospace systems. The tool is publicly available.
Topics:
The tutorial will be organized in four blocks of roughly 45 minutes each, covering the system specification formalism and the different analysis techniques as supported by our framework. Each block is composed of a short general introduction to the respective topic, followed by a demonstration of its realization in our toolset employing running examples from the aerospace domain.
More concretely, the following tutorial structure is envisaged:
0. Introduction and Overview
1. System modeling using AADL
- specifying basic nominal behavior
- adding timing and hybridity
- adding errors
- understanding the operational behavior of systems
2. Checking functional correctness
- model simulation
- deadlock checking
- model checking of functional properties
3. Safety and dependability analysis
- (dynamic) Fault Tree Analysis (FTA) and evaluation
- (dynamic) Failure Modes and Effects Analysis (FMEA)
- fault tolerance evaluation
4. Fault Detection, Isolation and Recovery (FDIR) analysis and performability evaluation
- fault detection analysis
- fault isolation analysis
- fault recovery analysis
- model checking of probabilistic performance properties in degraded modes
Background:
The tutorial has not previously been held. The modeling approach and the supporting toolset have been developed within the COMPASS Project (Correctness, Modeling, and Performance of Aerospace Systems) with funding from the European Space Agency. The techniques developed in COMPASS build upon previous experience acquired in EU-funded projects, such as ESACS, ISAAC, and MISSA. The toolset and more information about COMPASS are available from http://compass.informatik.rwth-aachen.de/, including access to nine scientific papers that have emanated from this project. In particular, [1] gives a detailed account of the modeling approach and its implementation.
References:
[1] M. Bozzano, A. Cimatti, J.-P. Katoen, V.Y. Nguyen, T. Noll, M. Roveri: "Safety, dependability, and performance analysis of extended AADL models". The Computer Journal, vol. 54, no. 5, 2011