About | Contact Us | Register | Login
ProceedingsSeriesJournalsSearchEAI
5th International ICST Conference on Performance Evaluation Methodologies and Tools

Research Article

HASL: an Expressive Language for Statistical Verification of Stochastic Models

Download723 downloads
Cite
BibTeX Plain Text
  • @INPROCEEDINGS{10.4108/icst.valuetools.2011.245710,
        author={Paolo Ballarini and Hilal Djafri and Marie Duflot and Serge Haddad and Nihal Pekergin},
        title={HASL: an Expressive Language for Statistical Verification of Stochastic Models},
        proceedings={5th International ICST Conference on Performance Evaluation Methodologies and Tools},
        publisher={ICST},
        proceedings_a={VALUETOOLS},
        year={2012},
        month={6},
        keywords={stochastic process model checking statistical estimation},
        doi={10.4108/icst.valuetools.2011.245710}
    }
    
  • Paolo Ballarini
    Hilal Djafri
    Marie Duflot
    Serge Haddad
    Nihal Pekergin
    Year: 2012
    HASL: an Expressive Language for Statistical Verification of Stochastic Models
    VALUETOOLS
    ICST
    DOI: 10.4108/icst.valuetools.2011.245710
Paolo Ballarini1, Hilal Djafri2, Marie Duflot1, Serge Haddad2,*, Nihal Pekergin1
  • 1: LACL
  • 2: LSV
*Contact email: haddad@lsv.ens-cachan.fr

Abstract

We introduce the Hybrid Automata Stochastic Logic HASL, a new temporal logic formalism for the verification of discrete event stochastic processes (DESP). HASL employs Linear Hybrid Automata (LHA) as machineries to select prefixes of relevant execution paths of a DESP. The advantage with LHA is that rather elaborate information can be collected on-the-fly during path selection, providing the user with a 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. We illustrate the HASL approach by means of some examples and a discussion about its expressiveness. We also provide empirical evidence obtained through COSMOS, a prototype software tool for HASL verification

Keywords
stochastic process model checking statistical estimation
Published
2012-06-26
Publisher
ICST
http://dx.doi.org/10.4108/icst.valuetools.2011.245710
Copyright © 2011–2025 ICST
EBSCOProQuestDBLPDOAJPortico
EAI Logo

About EAI

  • Who We Are
  • Leadership
  • Research Areas
  • Partners
  • Media Center

Community

  • Membership
  • Conference
  • Recognition
  • Sponsor Us

Publish with EAI

  • Publishing
  • Journals
  • Proceedings
  • Books
  • EUDL