User menu

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

Statistical abstraction and model-checking of Large Heterogeneous Systems

Primary tabs

Basu, Ananda Bensalem, Saddek Bozga, Marius Delahaye, Benoît Legay, Axel [UCL]

We propose a new simulation-based technique for verifying applications running within a large heterogeneous system. Our technique starts by performing simulations of the system in order to learn the context in which the application is used. Then, it creates a stochastic abstraction for the application, which takes the context information into account. This smaller model can be verified using efficient techniques such as statistical model checking. We have applied our technique to an industrial case study: the cabin communication system of an airplane. We use the BIP toolset to model and simulate the system. We have conducted experiments to verify the clock synchronization protocol i.e., the application used to synchronize the clocks of all computing devices within the system.

Document type Article de périodique (Journal article)
Publication date 2012
Language Anglais
Journal information "International Journal on Software Tools for Technology Transfer" - Vol. 14, no. 1, p. 53-72 (2012)
Peer reviewed yes
Publisher Springer Nature
issn 1433-2779
e-issn 1433-2787
Links
  1. ARINC 664, Aircraft Data Network, Part 7: Avionics Full Duplex Switched Ethernet (AFDX) Network (2005)
  2. II61588: Precision clock synchronization protocol for networked measurement and control systems (2004)
  3. Alur Rajeev, Dill David L., A theory of timed automata, 10.1016/0304-3975(94)90010-8
  4. Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Siffakis, E.: Verification of an afdx infrastructure using simulations and probabilities. In: Proceedings of 1st Conference on Runtime Verification (RV), Malta, 2010. Springer, Berlin (2010)
  5. Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time systems in BIP. In: SEFM06, Pune, India. pp. 3–12 (2006)
  6. Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: FORTE 2010, pp. 32–48. LNCS 6117, Springer, Berlin (2010)
  7. Bensalem, S., Delahaye, B., Legay, A.: Statistical model checking: present and future. In: Proceedings of 1st Conference on Runtime Verification (RV), Malta, 2010. Springer, Berlin (2010)
  8. Bucklew James Antonio, Introduction to Rare Event Simulation, ISBN:9781441918932, 10.1007/978-1-4757-4078-3
  9. Charara, H., Fraboul, C.: Modelling and simulation of an avionics full duplex switched ethernet. In: Proceedings of the Advanced Industrial Conference on Telecommunications/Service Assurance with Partial and Intermittent Resources Conference/E-Learning on Telecommunication Workshop. IEEE (2005)
  10. Charara, H., Scharbarg, J.L., Ermont, J., Fraboul, C.: Methods for bounding end-to-end delays on AFDX network. In: ECRTS. IEEE Computer Society (2006)
  11. Clarke, E.M., Donzé, A., Legay, A.: Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator. In: HVC. LNCS, vol. 5394, pp. 149–163. Springer, Berlin (to appear, 2008)
  12. Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in biolab: applications to the automated analysis of t-cell receptor signaling pathway. In: CMSB. LNCS, vol. 5307, pp. 231–250. Springer, Berlin (2008)
  13. Efron, B., Tibshirani, R.: An Introduction to the bootstrap. Hall/CRC Press Monographs on Statistics and Applied Probability (1994)
  14. Grosu, R., Smolka, S.A.: Monte carlo model checking. In: TACAS. LNCS, vol. 3440, pp. 271–286. Springer, Berlin (2005)
  15. He, R., Jennings, P., Basu, S., Ghosh, A.P., Wu, H.: A bounded statistical approach for model checking of unbounded until properties. In: ASE 2010, 25th IEEE/ACM International Conference on Automated Software Engineering, Antwerp, Belgium, September 20–24, 2010. pp. 225–234. ACM (2010)
  16. Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: VMCAI. LNCS, vol. 2937, pp. 73–84. Springer, Berlin (2004)
  17. Hoeffding Wassily, Probability Inequalities for Sums of Bounded Random Variables, 10.2307/2282952
  18. Jansen, D.N., Katoen, J.P., Oldenkamp, M., Stoelinga, M., Zapreev, I.S.: How fast and fat is your probabilistic model checker? an experimental performance comparison. In: HVC. LNCS, vol. 4899. Springer, Berlin (2007)
  19. Jennings, P., Ghosh, A.P., Basu, S.: A two-phase approximation for model checking probabilistic unbounded until properties of probabilistic systems. ACM Transactions on Software Engineering and Methodology (TOSEM) (2011)
  20. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: CMSB. LNCS, vol. 5688, pp. 218–234. Springer, Berlin (2009)
  21. Katoen, J.P., Zapreev, I.S.: Simulation-based ctmc model checking: An empirical evaluation. In: Proceedings of 6th International Conference on the Quantitative Evaluation of Systems (QEST). pp. 31–40. IEEE Computer Society (2009)
  22. Laplante, S., Lassaigne, R., Magniez, F., Peyronnet, S., de Rougemont, M.: Probabilistic abstraction for model checking: an approach based on property testing. ACM Trans. Comput. Log. 8(4) (2007)
  23. Parekh A.K., Gallager R.G., A generalized processor sharing approach to flow control in integrated services networks: the multiple node case, 10.1109/90.298432
  24. Rabih, D.E., Pekergin, N.: Statistical model checking using perfect simulation. In: Proceedings of 7th International Conference on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol. 5799, pp. 120–134. Springer, Berlin (2009)
  25. Scharbarg, J.L., Fraboul, C.: Simulation for end-to-end delays distribution on a switched ethernet. In: ETFA. IEEE (2007)
  26. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: CAV. pp. 202–215. LNCS 3114. Springer, Berlin (2004)
  27. Steinkellner, S., Andersson, H., Lind, I., Krus, P.: Hosted simulation for heterogeneous aircraft system development. In: Proceedings of 26th International Congress of the Aeronautical Sciences (2008)
  28. Wald A., Sequential Tests of Statistical Hypotheses, 10.1214/aoms/1177731118
  29. Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)
  30. Younes, H.L.S.: Error control for probabilistic model checking. In: VMCAI. pp. 142–156. LNCS 3855. Springer, Berlin (2006)
  31. Younes Håkan L. S., Kwiatkowska Marta, Norman Gethin, Parker David, Numerical vs. statistical probabilistic model checking, 10.1007/s10009-005-0187-8
  32. Younes Håkan L.S., Simmons Reid G., Statistical probabilistic model checking with a focus on time-bounded properties, 10.1016/j.ic.2006.05.002
  33. Zolotarev, V.M.: One-dimensional stable distribution. American Mathematical Society, Providence (1986)
Bibliographic reference Basu, Ananda ; Bensalem, Saddek ; Bozga, Marius ; Delahaye, Benoît ; Legay, Axel. Statistical abstraction and model-checking of Large Heterogeneous Systems. In: International Journal on Software Tools for Technology Transfer, Vol. 14, no. 1, p. 53-72 (2012)
Permanent URL https://hdl.handle.net/2078.1/210670