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

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 ZZ 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 ZZ. 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.