Campus Event Calendar
Event Entry
What and Who
Statemate Composition, and the Quantification Of Catastrophic Risks
Prof. Holger Hermanns
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 16 November 2006
13:00
60 Minutes
E1 3 - Hörsaal Gebäude
016
Saarbrücken
Abstract
Stochastic temporal logics have been proposed to express
requirements like correctness, availability, survivability or performability of
trustworthy system specifications. They are accompanied by
model-checking algorithms which can be applied to certify
these requirements on a component level. So far, this approach has
been implemented in academic prototypes.
This talk reports on our efforts to link an industrial state-of-the-art
modelling tool to these state-of-the-art analysis algorithms. In a
nutshell, we enable timed reachability analysis of uniform
continuous-time Markov decision processes, which are generated from
STATEMATE models. We give a detailed explanation of several
construction, transformation, reduction, and analysis steps required
to make this possible. The entire tool flow has been implemented,
and it is applied to a nontrivial example.
This work is supported by the DFG of project S3 of SFB/TR-14 AVACS.
requirements like correctness, availability, survivability or performability of
trustworthy system specifications. They are accompanied by
model-checking algorithms which can be applied to certify
these requirements on a component level. So far, this approach has
been implemented in academic prototypes.
This talk reports on our efforts to link an industrial state-of-the-art
modelling tool to these state-of-the-art analysis algorithms. In a
nutshell, we enable timed reachability analysis of uniform
continuous-time Markov decision processes, which are generated from
STATEMATE models. We give a detailed explanation of several
construction, transformation, reduction, and analysis steps required
to make this possible. The entire tool flow has been implemented,
and it is applied to a nontrivial example.
This work is supported by the DFG of project S3 of SFB/TR-14 AVACS.
Contact
--email hidden
passcode not visible
logged in users only
Veronika Weinand, 11/15/2006 13:04
Veronika Weinand, 11/14/2006 12:40
Veronika Weinand, 11/03/2006 12:18
Veronika Weinand, 10/25/2006 15:08
Veronika Weinand, 10/24/2006 12:47
Veronika Weinand, 10/23/2006 15:06
Veronika Weinand, 10/19/2006 14:54
Veronika Weinand, 10/16/2006 17:07
Veronika Weinand, 10/16/2006 17:05 -- Created document.
Veronika Weinand, 11/14/2006 12:40
Veronika Weinand, 11/03/2006 12:18
Veronika Weinand, 10/25/2006 15:08
Veronika Weinand, 10/24/2006 12:47
Veronika Weinand, 10/23/2006 15:06
Veronika Weinand, 10/19/2006 14:54
Veronika Weinand, 10/16/2006 17:07
Veronika Weinand, 10/16/2006 17:05 -- Created document.