HASL: A new approach for performance evaluation and model checking from concepts to experimentation - Archive ouverte HAL Access content directly
Journal Articles Performance Evaluation Year : 2015

HASL: A new approach for performance evaluation and model checking from concepts to experimentation

(1) , (2) , (3) , (4, 2) , (5)
1
2
3
4
5

Abstract

We introduce the Hybrid Automata Stochastic Language (HASL), a new temporal logic formalism for the verification of Discrete Event Stochastic Processes (DESP). HASL employs a Linear Hybrid Automaton (LHA) to select prefixes of relevant execution paths of a DESP. LHA allows rather elaborate information to be collected on-the-fly during path selection, providing the user with powerful means to express sophisticated measures. A formula of HASL consists of an LHA and an expression Z referring to moments of path random variables. A simulation-based statistical engine is employed to obtain a confidence interval estimate of the expected value of Z. In essence, HASL provides a unifying verification framework where temporal reasoning is naturally blended with elaborate reward-based analysis. Moreover, we have implemented a tool, named COSMOS, for performing analysis of HASL formula for DESP modelled by Petri nets. Using this tool we have developed two detailed case studies: a flexible manufacturing system and a genetic oscillator.
Fichier principal
Vignette du fichier
main.pdf (560.14 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01221815 , version 1 (28-10-2015)

Identifiers

Cite

Paolo Ballarini, Benoît Barbot, Marie Duflot, Serge Haddad, Nihal Pekergin. HASL: A new approach for performance evaluation and model checking from concepts to experimentation. Performance Evaluation, 2015, 90, pp.53-77. ⟨10.1016/j.peva.2015.04.003⟩. ⟨hal-01221815⟩
4572 View
405 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More