Every Tuesday at 4:00pm. Room HG02.032
| 10/12/07
|
Frank Wolff, visiting from the University of Duisburg-Essen, will talk about "Economic Aspects and Controlling of Enterprise Modelling"
not usual day: Monday ** and ** different room: HG00.086 ** and ** different time: 14:00 to 15:30
|
| 11/12/07
|
Bart Theelen, visiting from the Technical University Eindhoven, will talk "On Performance Analysis of Timed Probalistic Systems"
|
| 04/12/07
|
Idris Rai, visiting from Uganda, will talk about "Virtual clustering of user requests for autonomic content delivery"
| Abstract
|
"Virtual clustering of user requests for autonomic content delivery"
Idris Rai, visiting from Uganda
Abstract:
Content delivery networks (CDNs) have traditionally been proposed to improve
Web servers performance in terms of reducing their response times and
mitigating overload conditions. These are accomplished by simply placing
surrogate servers close to end-users and redirecting new requests to the
surrogate server close to the requesting client. Traditional CDNs have
worked well with Web services. Recently, however, a number of enterprises
have been working to use CDNs to provide other commercial services over the
Internet, such as video on-demand streaming (e.g., popular TV series, sports,
movies, etc), live TV streaming, and interactive media. These services are
often bandwidth demanding and require some stringent quality guarantees. To
deliver such services therefore, proposed CDNs, as opposed to traditional
CDNs, constitute of a number of servers on the Internet which must corporate
to efficiently deliver the content. Importantly, to guarantee expected quality
of service to end-users, the new CDNs must automatically be able to adapt to
dynamic network and users activities. These lead to the need for autonomic
CDNs (aCDNs). An autonomic CDN has two separate planes; a control plane,
which monitors users and network behaviors, and a data plane, which adapts
delivery mechanisms based on the output from the control plane.
On this talk, we will present an ongoing research work on autonomic CDN to
illustrate some functions of the control plane. In particular, we will present
a mechanism to virtually cluster arriving user requests to a server based on
the requests' network proximity and available servers close to the users.
Virtual clusters are then used by the server to decide the best available
server to take the extra load in case a new server is needed to help
delivering the content.
|
|
| 02/11/07
|
Jan Friso Groote will be visiting from TU Eindhoven.
not usual day: Friday ** and ** different room: HG01.057 ** but usual time
| Abstract
|
The mCRL2 toolset
Jan Friso Groote
Technical University of Eindhoven
Abstract
mCRL2 is a process algebra based language
to model the behaviour of communicating processes. It can be
used to describe processes with both data and time. The
primary target for the language is to analyse existing
protocols and distributed systems, as well as designing
new systems. For this, the toolset is essential. The toolset
contains a number of tools to simulate, reduce, analyse
and visualize process behaviour. In this talk a quick
impression of the language will be given, together with
a demo of the tools.
An impression of the language and the tools can be found
on www.mcrl2.org. The toolset is available under the boost
license, which essentially says that the toolset can be
used for every purpose, provided proper reference to the
authors is made. The tool is especially used under this license
to allow re-use of it by other parties.
|
|
| 16/10/07
|
Erik Proper will talk about "Architecture Principles -- A Regulative Perspective on Enterprise Engineering"
| Abstract
|
"Architecture Principles -- A Regulative Perspective on Enterprise Engineering"
Erik Proper
Abstract:
In this presentation I will report on some recent work on so-called
architecture principles. Architecture principles are positioned as
a model-based means to guide, control and direct the development
of enterprises, from t-its IT portfolio to its business processes.
|
|
| 09/10/07
|
Rinus Plasmeijer will talk about "iTasks: Executable Specifications of Interactive Work Flow Systems for the Web".
| Abstract
|
"iTasks: Executable Specifications of Interactive Work Flow Systems for the Web"
Rinus Plasmeijer
Abstract:
In this talk we present the iTask system: a set of combinators to specify
work flows in a pure functional language at a very high level of abstraction.
Work flow systems are automated systems in which tasks are coordinated that have
to be executed by humans and computers.
The combinators that we propose support work flow patterns commonly found in commercial work flow systems.
Compared with most of these commercial systems, the iTask system offers several advantages:
tasks are statically typed,
tasks can be higher order,
the combinators are fully compositional,
dynamic and recursive work flows can be specified,
and last but not least, the specification is used
to generate an executable web-based multi-user work flow application.
With the iTask system, useful work flows can be defined which cannot be expressed in other systems:
work can be interrupted and subsequently directed to other workers for further processing.
The implementation is special as well.
It is based on the Clean\ iData toolkit which makes it possible to create fully dynamic, interactive, thin
client web applications.
Thanks to the generic programming techniques used in the iData toolkit, the programming effort is
reduced significantly: state handling,
form rendering, user interaction, and storage management is handled automatically.
The iTask system allows a task to be regarded as a special kind of persistent redex being reduced by
the application user via task completion.
The combinators control the order in which these redexes are made available to the application user.
The system rewrites the persistent task redexes in a similar way as functions are rewritten in lazy
functional languages.
|
|
| 25/09/07
|
Arjen Hommersom will talk about "Verification of Medical Guidelines using Background Knowledge in Task Networks".
| Abstract
|
"Verification of Medical Guidelines using Background Knowledge
in Task Networks"
Arjen Hommersom
Abstract:
The application of a medical guideline to the treatment of the
patient's disease can be seen as the execution of tasks, sequentially
or in parallel, in the face of patient data. It has been shown that
many of such guidelines can be represented as a `network of tasks',
i.e., as a sequence of steps that have a specific function or goal. In
this paper a novel methodology for verifying the quality of such
guidelines is introduced. To investigate the quality of such
guidelines we propose to include medical background knowledge to task
networks and to formalise criteria for good practice medicine a
guideline should comply to. This framework was successfully applied to
a guideline dealing with the management of diabetes mellitus type 2
using the interactive theorem prover KIV.
|
|
| 18/09/07
|
David Jansen will talk about "Probabilistic Models and Their Verification"
| Abstract
|
Probabilistic Models and Their Verification
David Jansen
Abstract:
This presentation gives an introduction to Markov chains as used in probabilistic model checking.
We will see the logic PCTL and get an overview of the model checking algorithms.
|
|
| 21/08/07
|
Lars Frantzen will talk about "Modeling and Testing with Symbolic Transition Systems in Practice".
| Abstract
|
"Modeling and Testing With Symbolic Transition Systems in Practice"
Lars Frantzen
Abstract:
Symbolic Transition Systems (STS) are state machines with a
symbolic treatment of data. This comprises variables of
different types, and guards restricting the transitions by means
of a logical formula. Testing based on STS avoids the state space
explosion problem which shows up when using non-symbolic formalisms
like Labeled Transition Systems as the underlying specification
model. But new problems have to be tackled, like deciding
satisfiability, defining symbolic coverage criteria, etc. In this
talk the model of STS will be introduced, and a prototype implementation
library to simulate STS will be presented. The exemplified application
domain will be modeling and testing Web Services.
|
|
| 10/07/07
|
summer break. Seminars will start again on 21/08/07
|
| 03/07/07
|
Janos Sarbo will talk about "Towards a theory of natural conceptualization".
| Abstract
|
"Towards a theory of natural conceptualization"
Janos Sarbo
Abstract:
"The focus of this talk is on the early phases of modeling consisting in the
primary conceptualization of the underlying application domain. To this end I
introduce a process model for the generation of meaningful concepts for a
domain description. In virtue of its close relation with cognitive activity,
this process model enables the modeler as well as the user to comprehend the
concepts of the resulting domain in a natural way."
|
|
| 26/06/07
|
Sicco Verwer, visiting from the University of Delft, will talk about "Learning timed automata: theory and practice".
| Abstract
|
"Learning timed automata: theory and practice"
Sicco Verwer
University of Delft
Abstract:
In this talk we give an introduction to the problem oflearning deterministic
finite automata (DFA). We show how the state merging algorithm learns DFA and how
to prove that DFA are efficiently learnable. After this introduction
we show how we applied similar techniques to the problem of learning timed
automata (TA). We prove a necessary and sufficient condition for TA to be
efficiently learnable and show the results of a state merging algorithm for the
class of real-time automata. These are TA with only one clock that resets at
every transition. These results show that it is possible to learn the time
constraints within automata. In addition the obtained timed automata significantly
outperform the results of an algorithm that first uses sampling on the timed
data and then subsequently calls a DFA learning algorithm on the sampled data.
|
|
| 19/06/07
|
Ansgar Fehnker, visiting from NICTA (Australia), will talk about "Goanna - A Static Model Checker".
| Abstract
|
"Goanna - A Static Model Checker"
Ansgar Fehnker
NICTA
Abstract:
System software has been under scrutiny by the software verification community
from various angles in the recent past. There are two major algorithmic
approaches to ensure the correctness of and to eliminate bugs from such
systems: software model checking and static analysis. The approaches are
typically complementary. In this talk, we present a framework that transforms
static analysis problems into model checking problems. We investigate
how highly optimised model checkers can be used in the exploration of relevant
properties while at the same time avoiding scalability and abstraction issues
typically associated with pure software model checking approaches.
|
|
| 12/06/07
|
Jan Tretmans will talk about "ioco goes eco", some informal thoughts about environmental conformance.
|
| 05/06/07
|
Frits Vaandrager will talk about some successful experiences with using the Uppaal model checker in his lectures.
| Abstract
|
"Model Checkers in Education: 10^6 Users and Beyond"
Frits Vaandrager
Abstract:
In this (informal) talk I will tell about some successful experiences with using the Uppaal model checker in a first year course
on concurrency. In particular I will report on an assignment in which students were asked to check the correctness of solutions in
Allan Downey's Little Book of Semaphores. The students found several mistakes in the book which have been acknowledged by the author.
|
|
| 29/05/07
|
Julien Schmaltz will talk about "A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware"
| Abstract
|
"A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware"
Julien Schmaltz
Abstract:
We develop formal arguments about a bit clock synchronization mechanism of time-triggered hardware. The
architecture is inspired by the FlexRay standard and described at the gate-level.
Our framework is based on a general and precise model of clock domain crossing, which
considers metastability and clock imperfections. Our approach combines this model with
the state transition representation of hardware. The result is a clear
separation of analog and digital behaviors.
Analog considerations are formalized in the logic of the Isabelle/HOL theorem prover.
Digital arguments are discharged using the NuSMV model checker.
To the best of our knowledge, this is the first verification effort
tackling asynchronous transmissions at the gate-level.
|
|
| 22/05/07
|
Machiel van der Bijl, from the University of Twente, will speak about "Flexible models and flexible test cases". Slides
|
| 15/05/07
|
Jasper Berendsen will talk about his work about "Compositional Abstraction in Real-Time Model Checking".
| Abstract
|
"Compositional Abstraction in Real-Time Model Checking"
Jasper Berendsen
Abstract:
Abstraction is an important technique to combat state space explosion in model checking. When an abstract systems satisfies a certain invariant, the concrete system will.
Compositional abstraction allows to make an abstract system, by making an abstraction of just a single component. We present a framework for real-time systems described
in the model checking tool Uppaal as networks of timed automata (NTA). The semantics for a single component is given, and we prove that the composition of the semantics
of multiple components is equivalent to the operational NTA semantics. At this point we identify a major flaw in previous work. We define timed step simulation as the formal
notion of compositional abstraction. The framework is capable to describe all major features of the Uppaal modelling language, most notably: committed locations
that ensure a certain priority, and multi-reader/multi-writer variables.
|
|
