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 verification of Discrete Event Processes (DESP). HASL employs Linear Automaton (LHA) to select prefixes relevant execution paths DESP. LHA allows rather elaborate information be collected on-the-fly during path selection, providing user with powerful means express sophisticated measures. A formula consists an and expression Z referring moments random variables. simulation-based statistical engine is employed obtain confidence interval estimate expected value Z. In essence, provides unifying framework where reasoning naturally blended reward-based analysis. Moreover, we have implemented tool, named COSMOS, performing analysis DESP modelled by Petri nets. Using this tool developed two detailed case studies: flexible manufacturing system genetic oscillator.