Research Article
HASL: an Expressive Language for Statistical Verification of Stochastic Models
@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
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