5th International ICST Conference on Performance Evaluation Methodologies and Tools

Research Article

HASL: an Expressive Language for Statistical Verification of Stochastic Models

Download107 downloads
  • @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