***************************************************
* Fundamentals of Computer Science Seminar *
* *
* February 9-10, University of Namur *
* *
* Namur, Belgium *
* *
***************************************************
The Faculty of Computer Science of the University of Namur is proud to announce the creation of a Research Group on the Foundations of Computer Science (FOCUS). To celebrate the birth of this new group, the faculty organises a two-day seminar event on February 9-10 to which you are cordially invited.
The program is as follows; abstracts of the talks and tutorials can be found at the bottom of this mail.
Thursday February 9
-------------------
10h00 - 17h00 : The mCRL2 toolset: a hands-on tutorial (E. de Vink)
Friday Febraury 10
------------------
8h30 - 9h00 : Registration
9h00 - 9h30 : Welcome and opening
9h30 - 10h45 : Model Checking:
One Can Do Much More Than You Think! (J.-P. Katoen)
10h45 - 11h15 : Coffee break
11h15 - 12h30 : Collaborative Modeling of Dependable Embedded Systems (M. Verhoef)
12h30 - 14h00 : sandwhich lunch with poster presentation
14h00 - 14h20 : Presentation of the FOCUS group (W. Vanhoof)
14h20 - 15h20 : Around Focus' world: round trips in computer science
from applications to foundations and back (I. Linden)
15h20 - 15h50 : Coffee break
15h50 - 16h50 : Model-checking of software product lines (M. Cordy)
17h00 : Closing and drink
Participation to any of the events is free of charge, but for practical purposes registration is necessary. Registration can be done by a simple mail to clearly indicating your name, affiliation, and to which day(s) you intend to participate.
Hoping to see you soon in Namur!
---------------------------------------------------------------
The mCRL2 toolset: a hands-on tutorial (E. de Vink)
mCRL2 is a behavioral specification language in which parallel
communicating processes can be expressed. Standard datatypes are
provided and user-defined abstract datatypes can be included. An
extensive toolsuite is available for the simulation and visual
inspection of specifications, for the generation and manipulation of
state-spaces, as well as for symbolic modelchecking of an mCRL2 model
against formula of the modal mu-calculus. The mCRL2 suite aims to be a
competitive set of tools that supports formal analysis of
industrial-strength software models.
The tutorial is split up in two parts. In the first half starts off
with the basics of the process algebra, central notions of parallelism
and abstraction, and the combination of processes and data, and
continues with linearization of processes, temporal formula and formal
verification thereof. The second half consists of a number of guided
exercises to acquire hands-on experience with the mCRL2 toolset. The
projected exercises cover the basic workflow for formal analysis with
mCRL2. A short overview of industrial casestudies ends the day.
---------------------------------------------------------------
Collaborative Modeling of Dependable Embedded Systems (M. Verhoef)
The area of distributed embedded real-time control systems, or cyber physical systems, poses many challenges in industrial practice. Both productivity and quality are usually hampered by the fact that design activities are organized along discipline specific paths: mechanics, electronics, software and so on. Moreover, these disciplines have grown up separately, with their own foundations and base design on different forms of models. This inhibits our ability to reason about system-level design properties, such as for example fault tolerance and performance. This "design gap" typically leads to sub-optimal products and long development lead times. The approach advocated in this talk is to integrate existing design techniques into a unified semantic framework, which allows rapid evaluation of co-models using co-simulation. Practical application in industry of the tools and methodology developed demonstrates that this indeed removes these commonly observed hurdles.
---------------------------------------------------------------
Model Checking: One Can Do Much More Than You Think! (J.-P. Katoen)
Model checking is an automated verication technique that actively is applied to find bugs in hardware and software designs. Companies like IBM and Cadence developed their in-house model checkers, and acted as driving forces behind the design of the IEEE-standardized temporal logic PSL. On the other hand, model checking C-, C#- and .NET program code is an intensive research topic at, for instance, Microsoft and NASA.
In this talk, discuss three non-standard applications of model checking. The first example is taken from systems biology and shows the relevance of probabilistic reachability. Then, we show how to determine the optimal scheduling policy for multiple-battery systems so as to optimize the system's lifetime. Finally, we discuss a stochastic job scheduling problem that -- thanks to recent developments -- can be solved using model checking.
---------------------------------------------------------------
Around Focus' world: round trips in computer science from applications to foundations and back (I. Linden)
Building upon the experience of two practical applications, we shall show how they have inspired fundamental research, which in turn has been applied to solve real-life problems. Examples of such efforts include research activities in declarative languages, in particular, logic programming, constraint programming, concurrent programming, event calculus, semantics, process algebras, knowledge acquisition, Petri Nets and probabilistic reasoning.
---------------------------------------------------------------
Model-checking of software product lines (M. Cordy)
Software Product Lines Engineering is a paradigm that comes from other fields like automobile and becomes widespread in the software industry.
Instead of developing a single product, a number of variants are developed, that can be rapidly tailored to the needs of individual customers.
This poses a new challenge for validation and verification techniques: they are designed for a single product, but they become
impractical for such a large number of products. However, it is possible to take advantage of the similarity of the products to
avoid revalidating common parts. In this talk, we will focus on model checking, a technique that fits well with model-driven engineering.
| Period | 9 Feb 2012 → 10 Feb 2012 |
|---|
| Event type | Scientific committee |
|---|
| Location | Namur, Belgium |
|---|