User menu

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

Plasma Lab: A Modular Statistical Model Checking Platform

Primary tabs

Legay, Axel [UCL] Sedwards, Sean Traonouez, Louis-Marie

We present an overview of Plasma Lab, a modular statistical model checking (SMC) platform that facilitates multiple SMC algorithms , multiple modelling and query languages and has multiple modes of use. Plasma Lab may be used as a stand-alone tool with a graphical development environment or invoked from the command line for high performance scripting applications. Plasma Lab is written in Java for maximum cross-platform compatibility, but it may interface with tools and libraries written in arbitrary programming languages. Plasma Lab's API also allows it to be incorporated as a library within other tools. We first describe the motivation and architecture of Plasma Lab, then proceed to describe some of its important algorithms, including those for rare events and nondeterminism. We conclude with a number of industrially-relevant case studies and applications.

Document type Communication à un colloque (Conference Paper) – Présentation orale avec comité de sélection
Publication date 2016
Language Anglais
Conference "ISoLA" (du 10/10/2016 au 14/10/2016)
Peer reviewed yes
Host document "Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques Lecture Notes in Computer Science" (ISBN : 9783319471655)
Publisher Springer International Publishing (Cham)
Publication status Publié
Affiliation UCL - SST/ICTM/INGI - Pôle en ingénierie informatique
Links
  1. Agrawal Aditya, Simon Gyula, Karsai Gabor, Semantic Translation of Simulink/Stateflow Models to Hybrid Automata Using Graph Transformations, 10.1016/j.entcs.2004.02.055
  2. Arnold Alexandre, Boyer Benoît, Legay Axel, Contracts and Behavioral Patterns for SoS: The EU IP DANSE approach, 10.4204/eptcs.133.6
  3. Basseville, M., Nikiforov, I.V.: Detection of Abrupt Changes: Theory and Application. Prentice-Hall, Inc., Upper Saddle River (1993)
  4. Biere Armin, Heljanko Keijo, Junttila Tommi, Latvala Timo, Schuppan Viktor, Linear Encodings of Bounded LTL Model Checking, 10.2168/lmcs-2(5:5)2006
  5. Boyer Benoît, Corre Kevin, Legay Axel, Sedwards Sean, PLASMA-lab: A Flexible, Distributable Statistical Model Checking Library, Quantitative Evaluation of Systems (2013) ISBN:9783642401954 p.160-164, 10.1007/978-3-642-40196-1_12
  6. Boyer Benoît, Legay Axel, Traonouez Louis-Marie, A Formalism for Stochastic Adaptive Systems, Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (2014) ISBN:9783662452301 p.160-176, 10.1007/978-3-662-45231-8_12
  7. Colombo Alessio, Fontanelli Daniele, Legay Axel, Palopoli Luigi, Sedwards Sean, Motion planning in crowds using statistical model checking to enhance the social force model, 10.1109/cdc.2013.6760437
  8. Colombo Alessio, Fontanelli Daniele, Legay Axel, Palopoli Luigi, Sedwards Sean, Efficient customisable dynamic motion planning for assistive robots in complex human environments, 10.3233/ais-150338
  9. D’Argenio Pedro R., Hartmanns Arnd, Legay Axel, Sedwards Sean, Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata, Lecture Notes in Computer Science (2016) ISBN:9783319336923 p.99-114, 10.1007/978-3-319-33693-0_7
  10. D’Argenio Pedro, Legay Axel, Sedwards Sean, Traonouez Louis-Marie, Smart sampling for lightweight verification of Markov decision processes, 10.1007/s10009-015-0383-0
  11. 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
  12. Jegourel Cyrille, Legay Axel, Sedwards Sean, Importance Splitting for Statistical Model Checking Rare Properties, Computer Aided Verification (2013) ISBN:9783642397981 p.576-591, 10.1007/978-3-642-39799-8_38
  13. Jegourel Cyrille, Legay Axel, Sedwards Sean, An Effective Heuristic for Adaptive Importance Splitting in Statistical Model Checking, Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (2014) ISBN:9783662452301 p.143-159, 10.1007/978-3-662-45231-8_11
  14. Jegourel, C., Legay, A., Sedwards, S., Traonouez, L.: Distributed verification of rare properties using importance splitting observers. In: ECEASST, vol. 72 (2015)
  15. Kwiatkowska Marta, Norman Gethin, Parker David, Controller dependability analysis by probabilistic model checking, 10.1016/j.conengprac.2006.07.003
  16. Legay Axel, Sedwards Sean, Traonouez Louis-Marie, Scalable Verification of Markov Decision Processes, Software Engineering and Formal Methods (2015) ISBN:9783319152004 p.350-362, 10.1007/978-3-319-15201-1_23
  17. Legay, A., Sedwards, S., Traonouez, L.: Estimating rewards & rare events in nondeterministic systems. In: ECEASST, vol. 72 (2015)
  18. Legay Axel, Traonouez Louis-Marie, Statistical Model Checking of Simulink Models with Plasma Lab, Communications in Computer and Information Science (2016) ISBN:9783319295091 p.259-264, 10.1007/978-3-319-29510-7_15
  19. Legay Axel, Traonouez Louis-Marie, Statistical Model Checking with Change Detection, Transactions on Foundations for Mastering Change I (2016) ISBN:9783319465074 p.157-179, 10.1007/978-3-319-46508-1_9
  20. Ngo Van Chan, Legay Axel, Joloboff Vania, PSCV: A Runtime Verification Tool for Probabilistic SystemC Models, Computer Aided Verification (2016) ISBN:9783319415277 p.84-91, 10.1007/978-3-319-41528-4_5
  21. Okamoto Masashi, Some inequalities relating to the partial sum of binomial probabilities, 10.1007/bf02883985
  22. Page E. S., Continuous Inspection Schemes, 10.2307/2333009
  23. Wald A., Sequential Tests of Statistical Hypotheses, 10.1214/aoms/1177731118
  24. 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
Bibliographic reference Legay, Axel ; Sedwards, Sean ; Traonouez, Louis-Marie. Plasma Lab: A Modular Statistical Model Checking Platform.ISoLA (du 10/10/2016 au 14/10/2016). In: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques Lecture Notes in Computer Science, Springer International Publishing : Cham2016
Permanent URL https://hdl.handle.net/2078.1/210628