Titolo:
| Model Checking CSLTA: Using Timed Automata to Specify Properties of Stochastic Systems |
Relatore:
| Dott. Jeremy Sproston. |
Luogo:
| Aula 2 Collegio Raffaello (Piazza della Repubblica, 13). |
Orario:
| 16:00 - 17:30. |
Numero di crediti:
| 0.25. |
Vincoli di partecipazione:
| Nessuno. |
Sommario:
|
Continuous-time Markov chains are widely used to study the performance of
computer and telecommunication systems. Stochastic temporal logics such as
Continuous Stochastic Logic (CSL) and their associated model-checking
algorithms allow a formal and unified approach to the verification of
functional and performance properties of stochastic systems.
In this talk the stochastic logic CSLTA will be introduced. The logic CSLTA extends CSL by allowing timing properties to be expressed using a restricted class of timed automata. This extension allows us to specify a larger class of timing properties than in CSL. In particular, and in contrast to CSL, the logic CSLTA permits the specification of properties referring to the probability of a finite sequence of timed events, such as "with probability at least 0.75, a message sent at time t by a system A will be received before time t+5 by system B, and the acknowledgment will be back at A before time t+7". A model-checking algorithm for verifying CSLTA properties will also be introduced. |
Riferimento:
| Prof. Marco Bernardo. |
| Ultima modifica: 15/12/2009 | Approvato da: Presidente CCdL |