Simulation-based verification of hybrid automata stochastic logic formulas for stochastic symmetric nets

ABSTRACT

The Hybrid Automata Stochastic Logic (HASL) has been recently defined as a flexible way to express classical performance measures as well as more complex, path-based ones (generically called "HASL formulas"). The considered paths are executions of Generalized Stochastic Petri Nets (GSPN), which are an extension of the basic Petri net formalism to define discrete event stochastic processes. The computation of the HASL formulas for a GSPN model is demanded to the COSMOS tool, that applies simulation techniques to the formula computation. Stochastic Symmetric Nets (SSN) are a high level Petri net formalism, of the colored type, in which tokens can have an identity, and it is well known that colored Petri nets allow one to describe systems in a more compact and parametric form than basic (uncolored) Petri nets. In this paper we propose to extend HASL and COSMOS to support colors, so that performance formulas for SSN can be easily defined and evaluated. This requires a new definition of the logic, to ensure that colors are taken into account in a correct and useful manner, and a significant extension of the COSMOS tool.

References

1. A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic, 1(1):162--170, 2000.
2. G. Balbo, M. Beccuti, M. De Pierro, and G. Franceschinis. First Passage Time Computation in Tagged GSPNs with Queue Places. The Computer Journal, 2010. First published online July 22, 2010.
3. G. Balbo, M. Beccuti, M. D. Pierro, and G. Franceschinis. Computing first passage time distributions in stochastic well-formed nets. In ICPE'11 - Second Joint WOSP/SIPEW International Conference on Performance Engineering, pages 7--18, Karlsruhe, Germany, March 2011.
4. P. Ballarini, H. Djafri, M. Duflot, S. Haddad, and N. Pekergin. COSMOS: a statistical model checker for the hybrid automata stochastic logic. In Proceedings of the 8th International Conference on Quantitative Evaluation of Systems (QEST'11), pages 143--144, Aachen, Germany, Sept. 2011. IEEE Computer Society Press.
5. P. Ballarini, H. Djafri, M. Duflot, S. Haddad, and N. Pekergin. HASL: An expressive language for statistical verification of stochastic models. In Proceedings of the 5th International Conference on Performance Evaluation Methodologies and Tools (VALUETOOLS'11), pages 306{315, Cachan, France, May 2011.
6. B. Barbot, S. Haddad, and C. Picaronny. Coupling and importance sampling for statistical model checking. In C. Flanagan and B. König, editors, TACAS, volume 7214 of Lecture Notes in Computer Science, pages 331--346. Springer, 2012.
7. B. Barbot, S. Haddad, and C. Picaronny. Importance sampling for model checking of continuous time markov chains. In P. Dini and P. Lorenz, editors, SIMUL 2012, pages 30--35, Lisbon, Portugal, Novembre 2012. IARIA.
8. T. Chen, T. Han, J.-P. Katoen, and A. Mereacre. Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. Logic in Computer Science, Symposium on, 0:309--318, 2009.
9. G. Chiola, C. Dutheillet, G. Franceschinis, and S. Haddad. Stochastic well-formed coloured nets for symmetric modelling applications. IEEE Trans. on Computers, 42(11):1343--1360, nov 1993.
10. A. Clark and S. Gilmore. State-aware performance analysis with extended stochastic probes. In Proceedings of the 5th European Performance Engineering Workshop on Computer Performance Engineering, EPEW '08, pages 125--140, Berlin, Heidelberg, 2008. Springer-Verlag.
11. S. Donatelli, S. Haddad, and J. Sproston. Model checking timed and stochastic properties with CSLTA. IEEE Trans. Softw. Eng., 35(2):224--240, 2009.
12. E. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241 -- 266, 1982.
13. R. Gaeta. Efficient discrete-event simulation of colored petri nets. IEEE Trans. Softw. Eng., 22(9):629--639, Sept. 1996.
14. J. Hillston. Process algebras for quantitative analysis. In Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, pages 239--248, Washington, DC, USA, 2005. IEEE Computer Society.
15. M. A. Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modeling with Generalized Stochastic Petri Nets. J. Wiley, New York, NY, USA, 1995.
16. W. D. Obal, II and W. H. Sanders. State-space support for path-based reward variables. Perform. Eval., 35:233--251, May 1999.
17. A. Pnueli. The temporal logic of programs. In FOCS, pages 46--57. IEEE Computer Society, 1977.
18. K. Sen, M. Viswanathan, and G. Agha. Statistical model checking of black-box probabilistic systems. In In 16th conference on Computer Aided Verification (CAV O04), volume 3114 of LNCS, pages 202--215. Springer, 2004.
19. The CosyVerif Group. Cosyverif. http://www.cosyverif.org.
20. S. Wau Men Au-Yeung. Response Times in Healthcare Systems. PhD thesis, Imperial College, London, 2008. pubs.doc.ic.ac.uk/response-times-in-healthcare.
21. H. L. S. Younes. Ymer: A statistical model checker. In COMPUTER AIDED VERIFICATION. LNCS, pages 429--433. Springer, 2005.

Index Terms

• Computing methodologies

  • Modeling and simulation