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

Paolo Ballarini 1 Benoît Barbot 2 Marie Duflot 3 Serge Haddad 4, 2 Nihal Pekergin 5
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
4 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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 metadatas

Cited literature [48 references]  Display  Hide  Download

https://hal.inria.fr/hal-01221815
Contributor : Marie Duflot <>
Submitted on : Wednesday, October 28, 2015 - 3:59:18 PM
Last modification on : Friday, October 4, 2019 - 1:11:30 AM
Long-term archiving on : Friday, April 28, 2017 - 6:48:58 AM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

722

Files downloads

356