Statistical Model Checking with Change Detection

详细信息    查看全文

• 关键词：Statistical model checking ; Change detection ; CUSUM ; Monitoring ; Optimisation ; MATLAB/Simulink
• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9960
• 期：1
• 页码：157-179
• 全文大小：2,131 KB
• 参考文献：1.Agrawal, A., Simon, G., Karsai, G.: Semantic translation of simulink/stateflow models to hybrid automata using graph transformations. Electron. Notes Theoret. Comput. Sci. 109, 43–56 (2004)CrossRef MATH
  2.Barnat, J., Beran, J., Brim, L., Kratochvíla, T., Ročkai, P.: Tool chain to support automated formal verification of avionics simulink designs. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 78–92. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-32469-7_​6 CrossRef
  3.Basseville, M., Nikiforov, I.V.: Detection of Abrupt Changes: Theory and Application. Prentice-Hall Inc., Englewood Cliffs (1993)
  4.Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. Int. J. Softw. Tools Technol. Transf. 14(1), 53–72 (2012)CrossRef
  5.Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an AFDX infrastructure using simulations and probabilities. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 330–344. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-16612-9_​25 CrossRef
  6.Berendsen, J., Chen, T., Jansen, D.N.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, J., Cooper, S.B. (eds.) TAMC 2009. LNCS, vol. 5532, pp. 128–137. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-02017-9_​16 CrossRef
  7.Biere, A., Heljanko, K., Junttila, T.A., Latvala, T., Schuppan, V.: Linear Encodings of Bounded LTL Model Checking. Log. Methods Comput. Sci. 2(5) (2006). http://​dx.​doi.​org/​10.​2168/​LMCS-2(5:​5)2006
  8.Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160–164. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-40196-1_​12 CrossRef
  9.Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). doi:10.​1007/​3-540-45657-0_​29 CrossRef
  10.Clarke, E., Donzé, A., Legay, A.: Statistical Model checking of mixed-analog circuits with an application to a third order delta-sigma modulator. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol. 5394, pp. 149–163. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-01702-5_​16 CrossRef
  11.Clarke, E., Donzé, A., Legay, A.: On simulation-based probabilistic model checking of mixed-analog circuits. Formal Methods Syst. Des. 36(2), 97–113 (2010)CrossRef MATH
  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: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. Lecture Notes in Artificial Intelligence (LNAI), vol. 5307, pp. 231–250. Springer, Heidelberg (2008). doi:10.​1007/​978-3-540-88562-7_​18 CrossRef
  13.D’Argenio, P., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of markov decision processes. Int. J. Softw. Tools Technol. Transf. 17(4), 469–484 (2015)CrossRef
  14.David, A., Du, D., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for stochastic hybrid systems. In: Proceedings of the 1st International Workshop on Hybrid Systems and Biology (HSB), EPTCS, vol. 92, pp. 122–136 (2012)
  15.David, A., Du, D., Guldstrand Larsen, K., Legay, A., Mikučionis, M.: Optimizing control strategy using statistical model checking. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 352–367. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-38088-4_​24 CrossRef
  16.David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Vliet, J., Wang, Z.: Statistical model checking for networks of priced timed automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 80–96. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-24310-3_​7 CrossRef
  17.David, A., Larsen, K.G., Legay, A., Mikučionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 349–355. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​27 CrossRef
  18.Bhatt, D., Madl, G., Oglesby, D., Schloegel, K.: Towards scalable verification of commercial avionics software. In: AIAA Infotech@Aerospace 2010. Infotech@Aerospace Conferences, American Institute of Aeronautics and Astronautics, April 2010
  19.Grabiec, B., Traonouez, L.-M., Jard, C., Lime, D., Roux, O.H.: Diagnosis using unfoldings of parametric time petri nets. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 137–151. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-15297-9_​12 CrossRef
  20.Havelund, K., Roşu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342–356. Springer, Heidelberg (2002). doi:10.​1007/​3-540-46002-0_​24 CrossRef
  21.Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94–124 (1998)MathSciNet CrossRef MATH
  22.Höfner, P., McIver, A.: Statistical model checking of wireless mesh routing protocols. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 322–336. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-38088-4_​22 CrossRef
  23.Hérault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73–84. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-24622-0_​8 CrossRef
  24.Jegourel, C., Legay, A., Sedwards, S.: Importance splitting for statistical model checking rare properties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 576–591. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39799-8_​38 CrossRef
  25.Jessen, J.J., Rasmussen, J.I., Larsen, K.G., David, A.: Guided controller synthesis for climate controller using Uppaal Tiga . In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 227–240. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-75454-1_​17 CrossRef
  26.Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009). doi:10.​1007/​978-3-642-03845-7_​15 CrossRef
  27.Kim, Y., Kim, M., Kim, T.-H.: Statistical model checking for safety critical hybrid systems: an empirical evaluation. In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 162–177. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39611-3_​18 CrossRef
  28.Koh, C.H., Palaniappan, S.K., Thiagarajan, P., Wong, L.: Improved statistical model checking methods for pathway analysis. BMC Bioinf. 13(17), 1–12 (2012)
  29.Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.​1007/​978-3-642-22110-1_​47 CrossRef
  30.Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.​1007/​978-3-642-16612-9_​11 CrossRef
  31.Mathworks: polyspace a static analysis tools for C/C++ and Ada, December 2014. http://​www.​mathworks.​fr/​products/​polyspace/​
  32.Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606–620. Springer, Heidelberg (2006). doi:10.​1007/​11901433_​33 CrossRef
  33.Page, E.S.: Continuous inspection schemes. Biometrika 41(1/2), 100–115 (1954). http://​www.​jstor.​org/​stable/​2333009 MathSciNet CrossRef MATH
  34.Prover: Prover-Plugin, December 2014. http://​www.​prover.​com/​products/​prover_​plugin/​
  35.Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004). doi:10.​1007/​978-3-540-27813-9_​16 CrossRef
  36.Verdier, G., Hilgert, N., Vila, J.: Adaptive threshold computation for CUSUM-type procedures in change detection and isolation problems. Comput. Stat. Data Anal. 52(9), 4161–4174 (2008)MathSciNet CrossRef MATH
  37.Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117–186 (1945)MathSciNet CrossRef MATH
  38.Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)
  39.Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow/Simulink verification. Formal Methods Syst. Des. 43(2), 338–367 (2013)CrossRef MATH
  
• 作者单位：Axel Legay (14)
  Louis-Marie Traonouez (14)
  
  14. Inria Rennes – Bretagne Atlantique, 263 Avenue du Général Leclerc - Bât 12, Rennes, France
  
• 丛书名：Transactions on Foundations for Mastering Change I
• ISBN：978-3-319-46508-1
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9960

文摘

Statistical Model Checking (SMC) is a powerful and widely used approach that consists in estimating the probability for a system to satisfy a temporal property. This is done by monitoring a finite number of executions of the system, and then extrapolating the result by using statistics. The answer is correct up to some confidence that can be parameterized by the user. It is known that SMC mitigates the state-space explosion problem and allows to approximate undecidable queries. The approach has been implemented in several toolsets such as Plasma Lab, and successfully applied in a wide range of diverse areas such as systems biology, robotic, or automotive. In this paper, we add two new modest contributions to the cathedral of results on SMC. The first contribution is an algorithm that can be used to monitor changes in the probability distribution to satisfy a bounded-time property at runtime. Concretely, the algorithm constantly monitors the execution of the deployed system, and raises a flag when it observes that the probability has changed significantly. This is done by extending the applicability of the CUSUM algorithm used in signal processing into the formal validation setting. Our second contribution is to show how the programming interface of Plasma Lab can be exploited in order to make SMC technology directly available in toolsets used by designers. This integration is done by exploiting simulation facilities of design tools. Our approach thus differs from the one adopted by other SMC/formal verification toolsets which assume the existence of formal semantics for the design language, as well as a compiling chain to the rather academic one used by validation tool. The concept results in the integration of Plasma Lab as a library of the Simulink toolset. The contributions are illustrated by using Plasma Lab to verify a Simulink case study modelling a pig shed temperature controller.