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

Paolo Ballarini 1, 2 Benoît Barbot 3 Marie Duflot 4 Serge Haddad 2, 3 Nihal Pekergin 5
2 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
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Type de document :
Article dans une revue
Performance Evaluation, Elsevier, 2015, 90, pp.53-77. 〈10.1016/j.peva.2015.04.003〉
Liste complète des métadonnées

Littérature citée [48 références]  Voir  Masquer  Télécharger

Contributeur : Marie Duflot <>
Soumis le : mercredi 28 octobre 2015 - 15:59:18
Dernière modification le : jeudi 3 mai 2018 - 16:58:02
Document(s) archivé(s) le : vendredi 28 avril 2017 - 06:48:58


Fichiers produits par l'(les) auteur(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〉



Consultations de la notice


Téléchargements de fichiers