Course: Formal Methods
University of Twente
29 June-3 July, 2015
IPA organises Advanced Courses on each of its major research fields: Algorithmics and Complexity, Formal Methods and Software Engineering and Technology. Each of these Advanced Courses intends to give an overview of (part of) the research of IPA in this specific field.
The Advanced Course, which is hosted by IPA at the University of Twente, focusses on subject areas in formal methods where successful research is being conducted by groups in IPA. From several of these areas, risk analysis, functional programming, probabilistic model checking, graph transformations and supervisory control, topics are taken to which an entire course day is dedicated. Course days consist of lectures mixed with active training (exercises, assignments, etc.).
Dates, Location and Programme
The lectures will take place in Hal B 2F, (in Carré, see this 3D map or on Google Maps) at the University of Twente. The overall schedule of the course is as follows: course days will start at 10.00 and last until approximately 16.30 hours. Short coffee breaks are planned at around 11.00 and around 14.45 and an organised lunch break at, roughly, 12.30-13.30. A more detailed planning and more information will be posted below in due time. The tentative agenda, including tentative topic titles, will be announced asap.
Lecturers include Jan Kuper (UT), Arend Rensink (UT), Michel Reniers and/or Asia van de Mortel (TU/e), Joost-Pieter Katoen (RWTH) and Mariëlle Stoelinga (UT).
Slides and additional handouts (if available) for the lectures can be downloaded here.
| MONDAY 29 June | Mariëlle Stoelinga (UT) |
| Risk management meets model checking At this course day, I will discuss several prominent risk modeling and analysis techniques, such as fault trees, event trees and reliability block diagrams. For each of these formalisms, I will discuss their use, modeling power, and their analytical methods. In particular, we will deploy various formal methods, such as model checking, BDDs and stochastic methods. |
|
| TUESDAY 30 June | Jan Kuper (UT) |
| Functional Programming and Applications In practice, most programs are written in an imperative and/or object oriented language such as C, C++, Java, Python. Contrasting such languages is the family of declarative languages, to which functional programming languages belong. A functional program is a set of function definitions together with an evaluation mechanism, rather than a sequence of actions which describe actions that have to be performed. The consequence is that a mathematical programming language is strongly mathematical in nature.Depending on the background of the participants we will present several concepts and abstraction mechanisms that are central in functional programming languages, such as recursion (in particular its relation with mathematical induction), pattern matching, higher order functions, lambda abstraction.Typing is an important issue in a functional language. We will discuss several type constructions such as list types, function types, algebraic data types, recursive types, and also type derivation. Many constructions in a functional language are polymorphic, and they are well suited to serve as embedded languages.We will discuss the functional programming language Haskell, and use this for the exercises. Haskell is a so-called lazylanguage, meaning that an expression is only evaluated when its value is needed. That offers, among other things, the possibility of infinite lists.If time allows we will also discuss some further issues such as propositions-as-types, and hardware specification with Haskell. |
|
| WEDNESDAY 1 July | Joost-Pieter Katoen (RWTH Aachen) |
| The What, Why, and How of Probabilistic Verification Probabilities are ubiquitous. They are used in autonomous computing, systems biology, security, machine learning, reliability engineering, approximate computing, to mention a few. This tutorial addresses how verification techniques can be used to jointly address correctness and probabilities. I’ll give a gentle introduction to what probabilistic verification is, why it is practically relevant and how it can be employed in practice. I’ll conclude by addressing the main trends and challenges.Programme:10:00-11:00 What are discrete-time Markov chains? 11:30-12:30 Reachability probabilities 13:45-14:45 Probability of omega-regular properties 15:15-16:30 Timed reachability in continuous-time Markov chains |
|
| THURSDAY 2 July | Asia van de Mortel (TU/e) and Michel Reniers (TU/e) |
| Model-based engineering of supervisory controllers Many electronic control systems, such as in modern manufacturing and health care equipment or in vehicles, are combinations of both discrete-event and time-driven systems. For instance in vehicles, the enabling and disabling of a cruise control are typically event driven, whereas the control of the vehicle speed is time driven (e.g. PID). Different methods, such as loop shaping, can be used to design and tune controllers for time-driven systems. For the design of controllers for discrete-event systems, supervisory control theory (SCT) can be used. SCT provides a method to synthesize such controllers, called supervisors, based on specifications of system components represented by automata and requirements represented by both automata and simple logic expressions. The supervisor synthesized is by construction guaranteed to be non-blocking. Whenever the system components or requirements change, a new supervisor can be synthesized using adapted specifications. Supervisor synthesis can be incorporated in model-based systems engineering processes. Several tools are available to support this way of working allowing for thorough system analysis and systematic testing in an early phase of the development.The purpose of this lecture is to introduce supervisory control synthesis methods (supported by tools, http://cif.se.wtb.tue.nl) in combination with the model-based systems engineering paradigm that can contribute to product development. To this end, we explain how to:
|
|
| FRIDAY 3 July | Arend Rensink (UT) |
| Graph Transformation for Modelling Statics and Dynamics Graph grammars originated as a generalisation of context-sensitive string grammars, in order to study graph generation and parsing, but are now applied far and wide outside that domain. Being a rule-based formalism, graph transformation can be useful wherever graphs are a natural model for the domain at hand; this includes, but is by no means limited to, biological and social networks, architecture, security, and especially: static and dynamic aspects of any and all domain-specific languages.In this part of the IPA course, you will get a brief introduction into the theoretical background of graph transformation, and a longer introduction into one of the tools around that support its application for modelling purposes, namely GROOVE (sf.net/projects/groove). On the basis of a series of problems of growing complexity, you will learn what is involved in constructing graph-based models and bringing them to life using graph transformation. |
Course Material
Course material, if any, will be handed out during the course or distributed prior to the course. Where possible, this material will be made available for downloading via this page.
Costs
The courses are intended for IPA PhD students, giving them an overview of IPA’s research. For IPA PhD students, participation is free of charge (including overnight accommodation if necessary, see below), but registration is required. Other IPA-members can attend if there is capacity left, and the same holds for members of associated research schools. For these categories we will charge costs for the course material, lunches, etc, and IPA will not provide overnight accommodation. Contact us for information regarding pricing. For all categories, in case of no show extra charges may apply.
Registration
You can register using the online registration form. The form allows you to specify which course days you will attend. To make the course count as one of the required elements in the “Opleidings- en Begeleidingsplan” of an IPA Ph.D student, at least 80 percent of the course days must be attended. If you require overnight accommodation in Twente for one or more nights during the course, please specify this in the “Remarks” box of the form. Registration closes on 12 June, 2015.
Accommodation
Overnight accommodation is included, if needed. You can specify your accommodation needs on the registration form.