PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
Tytuł artykułu

A GPGPU–based simulator for prism: statistical verification of results of PMC

Treść / Zawartość
Identyfikatory
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
We describe a GPGPU–based Monte Carlo simulator integrated with Prism. It supports Markov chains with discrete or continuous time and a subset of properties expressible in PCTL, CSL and their variants extended with rewards. The simulator allows an automated statistical verification of results obtained using Prism’s formal methods.
Twórcy
autor
  • RWTH Aachen University, Schinkelstr. 2, 52062 Aachen, Germany
autor
  • Polish Academy of Sciences Institute of Theoretical and Applied Informatics ul. Bałtycka 5, 44-100 Gliwice, Poland
  • Jan Długosz University in Częstochowa Institute of Mathematics and Computer Science Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland
Bibliografia
  • [1] Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time markov chains. Transactions on Computational Logic (TOCL) 1(1), 162–170 (2000). DOI http://dx.doi.org/10.1145/343369.343402.
  • [2] Chafik, O.: Javacl. https://github.com/nativelibs4java/JavaCL (2016)
  • [3] Copik, M.: GPU-accelerated stochastic simulator engine for PRISM model checker. Bachelor’s Thesis, Silesian University of Technology, Gliwice, Poland (2014)
  • [4] Fox, B.L., Glynn, P.W.: Computing poisson probabilities. Commun. ACM 31(4), 440–445 (1988). DOI http://dx.doi.org/10.1145/42404.42409
  • [5] Gross, D., Miller, D.: The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research 32(2), 343–361 (1984). DOI http://dx.doi.org/10.1287/opre.32.2.343
  • [6] Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal aspects of computing 6(5), 512–535 (1994) DOI http://dx.doi.org/10.1007/ BF01211866
  • [7] Herault, T., Lassaigne, R., Peyronnet, S.: Apmc 3.0: Approximate verification of discrete and continuous time markov chains. In: Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, QEST ’06, pp. 129–130. IEEE Computer Society, (2006). DOI http://dx.doi.org/10.1109/QEST.2006.5
  • [8] Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM’07), LNCS, vol. 4486, pp. 220–270. Springer (2007)
  • [9] Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: G. Gopalakrishnan, S. Qadeer (eds.) Proc. 23rd International Conference on Computer Aided Verification (CAV’11), LNCS, vol. 6806, pp. 585– 591. Springer (2011). DOI http://dx.doi.org/10.1007/978-3-642-22110-1_47
  • [10] Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: An overview. In: International Conference on Runtime Verification, pp. 122–135. Springer (2010). DOI http://dx.doi.org/10.1007/978-3-642-16612-9_11
  • [11] Pourranjbar, A., Hillston, J., Bortolussi, L.: Don’t just go with the flow: Cautionary tales of fluid flow approximation. In: Computer Performance Engineering - 9th European Workshop, pp. 156–171 (2012). DOI http://dx.doi.org/10.1007/ 978-3-642-36781-6_11
  • [12] Salmon, J.K., Moraes, M.A., Dror, R.O., Shaw, D.E.: Parallel random numbers: As easy as 1, 2, 3. In: Proceedings of 2011 International Conference for High Performance Computing, Networking, Storage and Analysis, SC ’11, pp. 16:1–16:12. ACM, (2011). DOI http://dx.doi.org/10.1145/2063384.2063405.
  • [13] Stone, J.E., Gohara, D., Shi, G.: OpenCL: A parallel programming standard for heterogeneous computing systems. Computing in science & engineering 12(1-3), 66– 73 (2010). DOI http://dx.doi.org/10.1109/MCSE.2010.69
  • [14] Younes, H., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT) 8(3), 216–228 (2006). DOI http://dx.doi.org/10.1007/ s10009-005-0187-8
  • [15] Younes, H.L.S.: Ymer: A statistical model checker. In: Proceedings of the 17th International Conference on Computer Aided Verification, CAV’05, pp. 429– 433. Springer-Verlag, Berlin, Heidelberg (2005). DOI http://dx.doi.org/10.1007/ 11513988_43
  • [16] Younes, H.L.S.: Ymer. https://github.com/hlsyounes/ymer (2016)
Typ dokumentu
Bibliografia
Identyfikator YADDA
bwmeta1.element.baztech-bdb9cb01-7d09-4e0d-a93b-3ab8d4a17723
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.