User menu

Accès à distance ? S'identifier sur le proxy UCLouvain

Statistical Model Checking QoS properties of Systems with SBIP

Primary tabs

Bensalem, Saddek Bozga, Marius Delahaye, Benoît Jégourel, Cyrille Legay, Axel [UCL] Nouri, Ayoub

BIP is a component-based framework supporting rigorous design of embedded systems. This paper presents SBIP, an extension of BIP that relies on a new stochastic semantics that enables veri cation of large-size systems by using Statistical Model Checking. The approach is illustrated on several industrial case studies.

Document type Communication à un colloque (Conference Paper)
Publication date 2012
Language Anglais
Conference "Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium, ISoLA 2012" (du 15/10/2012 au 18/10/2012)
Host document "Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change Lecture Notes in Computer Science" (ISBN : 9783642340253)
Publisher Springer Berlin Heidelberg (Berlin, Heidelberg)
Links
  1. Basu Ananda, Bensalem Saddek, Bozga Marius, Caillaud Benoît, Delahaye Benoît, Legay Axel, Statistical Abstraction and Model-Checking of Large Heterogeneous Systems, Formal Techniques for Distributed Systems (2010) ISBN:9783642134630 p.32-46, 10.1007/978-3-642-13464-7_4
  2. Basu Ananda, Bensalem Saddek, Bozga Marius, Delahaye Benoît, Legay Axel, Sifakis Emmanuel, Verification of an AFDX Infrastructure Using Simulations and Probabilities, Runtime Verification (2010) ISBN:9783642166112 p.330-344, 10.1007/978-3-642-16612-9_25
  3. Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Systems in BIP. In: SEFM 2006, pp. 3–12 (September 2006)
  4. Bensalem, S., Delahaye, B., Legay, A.: Statistical model checking: Present and future. In: RV. Springer (2010)
  5. Bensalem Saddek, de Silva Lavindra, Griesmayer Andreas, Ingrand Felix, Legay Axel, Yan Rongjie, A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems, Software Composition (2011) ISBN:9783642220449 p.116-132, 10.1007/978-3-642-22045-6_8
  6. Bogdoll Jonathan, Ferrer Fioriti Luis María, Hartmanns Arnd, Hermanns Holger, Partial Order Methods for Statistical Model Checking and Simulation, Formal Techniques for Distributed Systems (2011) ISBN:9783642214608 p.59-74, 10.1007/978-3-642-21461-5_4
  7. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
  8. Falcone Yliès, Jaber Mohamad, Nguyen Thanh-Hung, Bozga Marius, Bensalem Saddek, Runtime Verification of Component-Based Systems, Software Engineering and Formal Methods (2011) ISBN:9783642246890 p.204-220, 10.1007/978-3-642-24690-6_15
  9. Grosu Radu, Smolka Scott A., Monte Carlo Model Checking, Tools and Algorithms for the Construction and Analysis of Systems (2005) ISBN:9783540253334 p.271-286, 10.1007/978-3-540-31980-1_18
  10. Havelund Klaus, Roşu Grigore, Synthesizing Monitors for Safety Properties, Tools and Algorithms for the Construction and Analysis of Systems (2002) ISBN:9783540434191 p.342-356, 10.1007/3-540-46002-0_24
  11. Hérault Thomas, Lassaigne Richard, Magniette Frédéric, Peyronnet Sylvain, Approximate Probabilistic Model Checking, Lecture Notes in Computer Science (2004) ISBN:9783540208037 p.73-84, 10.1007/978-3-540-24622-0_8
  12. Hoeffding Wassily, Probability Inequalities for Sums of Bounded Random Variables, 10.1080/01621459.1963.10500830
  13. Jansen David N., Katoen Joost-Pieter, Oldenkamp Marcel, Stoelinga Mariëlle, Zapreev Ivan, How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison, Hardware and Software: Verification and Testing ISBN:9783540779643 p.69-85, 10.1007/978-3-540-77966-7_9
  14. Jegourel Cyrille, Legay Axel, Sedwards Sean, Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking, Computer Aided Verification (2012) ISBN:9783642314230 p.327-342, 10.1007/978-3-642-31424-7_26
  15. Jegourel Cyrille, Legay Axel, Sedwards Sean, A Platform for High Performance Statistical Model Checking – PLASMA, Tools and Algorithms for the Construction and Analysis of Systems (2012) ISBN:9783642287558 p.498-503, 10.1007/978-3-642-28756-5_37
  16. Katoen, J.-P., Zapreev, I.S.: Simulation-based ctmc model checking: An empirical evaluation. In: QEST, pp. 31–40. IEEE Computer Society (2009)
  17. Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker mrmc. In: QEST, pp. 167–176. IEEE Computer Society (2009)
  18. Krunz, M., Sass, R., Hughes, H.: Statistical characteristics and multiplexing of MPEG streams. In: INFOCOM, pp. 455–462 (April 1995)
  19. Krunz Marwan, Tripathi Satish K., On the characterization of VBR MPEG streams, 10.1145/258623.258688
  20. Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: QEST, pp. 322–323. IEEE (2004)
  21. Laplante Sophie, Lassaigne Richard, Magniez Frédéric, Peyronnet Sylvain, de Rougemont Michel, Probabilistic abstraction for model checking : An approach based on property testing, 10.1145/1276920.1276922
  22. Parzen, E.: Stochastic Processes. Holden Day (1962)
  23. El Rabih Diana, Pekergin Nihal, Statistical Model Checking Using Perfect Simulation, Automated Technology for Verification and Analysis (2009) ISBN:9783642047602 p.120-134, 10.1007/978-3-642-04761-9_11
  24. Roşu Grigore, Bensalem Saddek, Allen Linear (Interval) Temporal Logic – Translation to LTL and Monitor Synthesis, Computer Aided Verification (2006) ISBN:9783540374060 p.263-277, 10.1007/11817963_25
  25. Sen Koushik, Viswanathan Mahesh, Agha Gul, Statistical Model Checking of Black-Box Probabilistic Systems, Computer Aided Verification (2004) ISBN:9783540223429 p.202-215, 10.1007/978-3-540-27813-9_16
  26. Wald A., Sequential Tests of Statistical Hypotheses, 10.1214/aoms/1177731118
  27. Wijesekera Duminda, Srivastava Jaideep, Quality of service (QoS) metrics for continuous media, 10.1007/bf00429748
  28. Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Carnegie Mellon (2005)
  29. Zuliani, P., Baier, C., Clarke, E.M.: Rare-event verification for stochastic hybrid systems. In: HSCC, pp. 217–226. ACM (2012)
  30. Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink/stateflow verification. In: HSCC, pp. 243–252. ACM (2010)
Bibliographic reference Bensalem, Saddek ; Bozga, Marius ; Delahaye, Benoît ; Jégourel, Cyrille ; Legay, Axel ; et. al. Statistical Model Checking QoS properties of Systems with SBIP.Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 5th International Symposium, ISoLA 2012 (du 15/10/2012 au 18/10/2012). In: Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change Lecture Notes in Computer Science, Springer Berlin Heidelberg : Berlin, Heidelberg2012
Permanent URL https://hdl.handle.net/2078.1/210640