User menu

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

Statistical Model Checking for Stochastic Hybrid Systems

Primary tabs

David, Alexandre Mikučionis, Marius Larsen Kim, Guldstrand Bogsten Poulsen, Danny Legay, Axel [UCL] Du, Dehui

This paper presents novel extensions and applications of the UPPAAL-SMC model checker. The extensions allow for statistical model checking of stochastic hybrid systems. We show how our race-based stochastic semantics extends to networks of hybrid systems, and indicate the integration technique applied for implementing this semantics in the UPPAAL-SMC simulation engine. We report on two applications of the resulting tool-set coming from systems biology and energy aware buildings.

Document type Communication à un colloque (Conference Paper)
Publication date 2012
Language Anglais
Conference "Proceedings First International Workshop on Hybrid Systems and Biology" (du 03/09/2012 au 03/09/2012)
Host document "Electronic Proceedings in Theoretical Computer Science"
Publisher Open Publishing Association
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. Ballarini Paolo, Djafri Hilal, Duflot Marie, Haddad Serge, Pekergin Nihal, COSMOS: A Statistical Model Checker for the Hybrid Automata Stochastic Logic, 10.1109/qest.2011.24
  4. Bulychev Peter, David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach, 10.4204/eptcs.78.1
  5. Barkai Naama, Leibler Stanislas, Biological rhythms: Circadian clocks limited by noise, 10.1038/35002258
  6. Clarke Edmund, Donzé Alexandre, Legay Axel, On simulation-based probabilistic model checking of mixed-analog circuits, 10.1007/s10703-009-0076-y
  7. Basu Ananda, Bensalem Saddek, Bozga Marius, Delahaye Benoît, Legay Axel, Statistical abstraction and model-checking of large heterogeneous systems, 10.1007/s10009-011-0201-2
  8. David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Poulsen Danny Bøgsted, van Vliet Jonas, Wang Zheng, Statistical Model Checking for Networks of Priced Timed Automata, Lecture Notes in Computer Science (2011) ISBN:9783642243097 p.80-96, 10.1007/978-3-642-24310-3_7
  9. David Alexandre, Larsen Kim G., Legay Axel, Mikučionis Marius, Wang Zheng, Time for Statistical Model Checking of Real-Time Systems, Computer Aided Verification (2011) ISBN:9783642221095 p.349-355, 10.1007/978-3-642-22110-1_27
  10. Fehnker Ansgar, Ivančić Franjo, Benchmarks for Hybrid Systems Verification, Hybrid Systems: Computation and Control (2004) ISBN:9783540212591 p.326-341, 10.1007/978-3-540-24743-2_22
  11. Gong Haijun, Zuliani Paolo, Komuravelli Anvesh, Faeder James R., Clarke Edmund M., Computational Modeling and Verification of Signaling Pathways in Cancer, Algebraic and Numeric Biology (2012) ISBN:9783642280665 p.117-135, 10.1007/978-3-642-28067-2_7
  12. Gillespie Daniel T., Exact stochastic simulation of coupled chemical reactions, 10.1021/j100540a008
  13. Jha Sumit K., Clarke Edmund M., Langmead Christopher J., Legay Axel, Platzer André, Zuliani Paolo, A Bayesian Approach to Model Checking Biological Systems, Computational Methods in Systems Biology (2009) ISBN:9783642038440 p.218-234, 10.1007/978-3-642-03845-7_15
  14. Cyrille Jegourel, CAV (2012)
  15. Katoen Joost-Pieter, Zapreev Ivan S., Hahn Ernst Moritz, Hermanns Holger, Jansen David N., The ins and outs of the probabilistic model checker MRMC, 10.1016/j.peva.2010.04.001
  16. Legay Axel, Delahaye Benoît, Bensalem Saddek, Statistical Model Checking: An Overview, Runtime Verification (2010) ISBN:9783642166112 p.122-135, 10.1007/978-3-642-16612-9_11
  17. 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
  18. Larsen Kim G., Skou Arne, Bisimulation through probabilistic testing, 10.1016/0890-5401(91)90030-6
  19. Pnueli Amir, The temporal logic of programs, 10.1109/sfcs.1977.32
  20. Bulychev Peter, David Alexandre, Guldstrand Larsen Kim, Legay Axel, Li Guangyuan, Bøgsted Poulsen Danny, Stainer Amelie, Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic, Logic for Programming, Artificial Intelligence, and Reasoning (2012) ISBN:9783642287169 p.168-182, 10.1007/978-3-642-28717-6_15
  21. Martins João, Platzer André, Leite João, Statistical Model Checking for Distributed Probabilistic-Control Hybrid Automata with Smart Grid Applications, Formal Methods and Software Engineering (2011) ISBN:9783642245589 p.131-146, 10.1007/978-3-642-24559-6_11
  22. Koymans Ron, Specifying real-time properties with metric temporal logic, 10.1007/bf01995674
  23. Behrmann Gerd, Fehnker Ansgar, Hune Thomas, Larsen Kim, Pettersson Paul, Romijn Judi, Vaandrager Frits, Minimum-Cost Reachability for Priced Time Automata, Hybrid Systems: Computation and Control (2001) ISBN:9783540418665 p.147-161, 10.1007/3-540-45351-2_15
  24. Sen Koushik, Viswanathan Mahesh, Agha Gul, On Statistical Model Checking of Stochastic Systems, Computer Aided Verification (2005) ISBN:9783540272311 p.266-280, 10.1007/11513988_26
  25. 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
  26. Vilar J. M. G., Kueh H. Y., Barkai N., Leibler S., Mechanisms of noise-resistance in genetic oscillators, 10.1073/pnas.092133899
  27. Alur Rajeev, La Torre Salvatore, Pappas George J., Optimal Paths in Weighted Timed Automata, Hybrid Systems: Computation and Control (2001) ISBN:9783540418665 p.49-62, 10.1007/3-540-45351-2_8
  28. Younes Håkan L. S., Simmons Reid G., Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling, Computer Aided Verification (2002) ISBN:9783540439974 p.223-235, 10.1007/3-540-45657-0_17
  29. Zuliani Paolo, Baier Christel, Clarke Edmund M., Rare-event verification for stochastic hybrid systems, 10.1145/2185632.2185665
  30. Zuliani Paolo, Platzer André, Clarke Edmund M., Bayesian statistical model checking with application to Simulink/Stateflow verification, 10.1145/1755952.1755987
  31. Alexandre David (2012)
  32. Gómez Rodolfo, A Compositional Translation of Timed Automata with Deadlines to Uppaal Timed Automata, Lecture Notes in Computer Science (2009) ISBN:9783642043673 p.179-194, 10.1007/978-3-642-04368-0_15
  33. David Alexandre, Larsen Kim G., Legay Axel, Nyman Ulrik, Wasowski Andrzej, Timed I/O automata : a complete specification theory for real-time systems, 10.1145/1755952.1755967
  34. Alexandre David, 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (2012)
  35. David Alexandre, Larsen Kim Guldstrand, Legay Axel, Mikučionis Marius, Schedulability of Herschel-Planck Revisited Using Statistical Model Checking, Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies (2012) ISBN:9783642340314 p.293-307, 10.1007/978-3-642-34032-1_28
Bibliographic reference David, Alexandre ; Mikučionis, Marius ; Larsen Kim, Guldstrand ; Bogsten Poulsen, Danny ; Legay, Axel ; et. al. Statistical Model Checking for Stochastic Hybrid Systems.Proceedings First International Workshop on Hybrid Systems and Biology (du 03/09/2012 au 03/09/2012). In: Electronic Proceedings in Theoretical Computer Science, Open Publishing Association2012
Permanent URL https://hdl.handle.net/2078.1/210459