Skip to Main content Skip to Navigation
Journal articles

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

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [48 references]  Display  Hide  Download
Contributor : Marie Duflot Connect in order to contact the contributor
Submitted on : Wednesday, October 28, 2015 - 3:59:18 PM
Last modification on : Wednesday, February 2, 2022 - 3:57:20 PM
Long-term archiving on: : Friday, April 28, 2017 - 6:48:58 AM


Files produced by the author(s)



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, Elsevier, 2015, 90, pp.53-77. ⟨10.1016/j.peva.2015.04.003⟩. ⟨hal-01221815⟩



Record views


Files downloads