微信服务号

微信订阅号

2025年4月1日 19:22 星期二
首页 > 过刊浏览>2015年第26卷第8期 >1853-1870. DOI:10.13328/j.cnki.jos.004838
PDF HTML阅读 XML下载 导出引用 引用提醒
面向随机模型检验的模型抽象技术
作者:
基金项目:

国家自然科学基金(61021062, 61472179); 中国博士后科学基金(2013M531328); 山东省自然科学基金(ZR2012FQ 013); 山东省高等学校科技计划(J13LN10); 泰安市科技发展计划(201330629)


Model Abstraction for Stochastic Model Checking
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [90]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    随机模型检验是经典模型检验理论的延伸和推广,由于其结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且运算处理的是关于状态的概率向量而非经典模型检验中的位向量,所以状态爆炸问题在随机模型检验中更为严重.抽象作为缓解状态空间爆炸问题的重要技术之一,已经开始被应用到随机模型检验领域并取得了一定的进展.以面向随机模型检验的模型抽象技术为研究对象,首先给出了模型抽象技术的问题描述,然后按抽象模型构造技术分类归纳了其研究方向及目前的研究进展,最后对比了目前的模型抽象技术及其关系,总结出其还未能给出模型抽象问题的满意答案,并指出了有效解决模型抽象问题未来的研究方向.

    Abstract:

    Stochastic model checking is a recent extension and generalization of the classical model checking. Stochastic model checking combines the classical model checking algorithms and linear equation solving or linear programming algorithms, moreover, it processes the probability vector instead of the bit vector. Consequently, the state explosion problem is more severe in stochastic model checking than classical model checking. Abstraction is an important means to tackle the state explosion problem, and it has made some progress in applying to the field of stochastic models testing. This study focus on model abstraction for stochastic model checking. First, the problem of model abstraction is formally presented. Then, the advances in the research area are classified and summarized according to the construction technology of abstraction model. At last, the various abstraction technologies are compared in regard to the effectiveness of solving the model abstraction problem, and the future research topics for improvement in solving the model abstraction problem are pointed out.

    参考文献
    [1] Liu K, Shan ZG, Wang J, He JF, Zhang ZT, Qin YW. Overview on major research plan of trustworthy software. Bulletin of National Natural Science Foundation of China, 2008,22(3):145-151 (in Chinese with English abstract).
    [2] Baier C, Katoen JP. Principles of Model Checking. London: The MIT Press, 2008. 745-790.
    [3] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proc. of the Workshop on Logic of Programs. Berlin, Heidelberg: Springer-Verlag, 1981. 52-71. [doi: 10.1007/BFb0025774]
    [4] Queille JP, Sifakis J. Specification and verification of concurrent systems in CESAR. In: Proc. of the 5th Colloquium on Int'l Symp. on Programming. Berlin, Heidelberg: Springer-Verlag, 1982. 337-351. [doi: 10.1007/3-540-11494-7_22]
    [5] Lin HM, Zhang WH. Model checking: Theories, techniques and applications. Acta Electronica Sinica, 2002,30(12A):1907-1912 (in Chinese with English abstract).
    [6] Clarke EM, Emerson EA, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52(11):74-84. [doi: 10.1145/1592761.1592781]
    [7] Kwiatkowska M, Norman G, Parker D. Stochastic model checking. In: Proc. of the 7th Int'l Conf. on Formal Methods for Performance Evaluation. Berlin, Heidelberg: Springer-Verlag, 2007. 220-270. [doi: 10.1007/978-3-540-72522-0_6]
    [8] Ndukwu U, Mclver A. An expectation transformer approach to predicate abstraction and data independence for probabilistic programs. Electronic Proceedings in Theoretical Computer Science, 2010,28:129-143. [doi: 10.4204/EPTCS.28.9]
    [9] Baier C, Haverkort BR, Hermanns H, Katoen JP. Performance evaluation and model checking join forces. Communication of the ACM, 2010,53(9):74-85. [doi: 10.1145/1810891.1810912]
    [10] Duflot M, Kwiatkowska M, Norman G, Parker D, Peyronnet S, Picaronny C, Sproston J. Practical applications of probabilistic model checking to communication protocols. In: Gnesi S, Margaria T, eds. Proc. of the Formal Methods for Industrial Critical Systems: A Survey of Applications. Washington: IEEE Computer Society Press, 2012. 133-150. [doi: 10.1002/9781118459898. ch7]
    [11] Calinescu R, Grunske L, Kwiatkowska M, Mirandola R, Tamburrelli G. Dynamic QoS management and optimisation in service-based systems. IEEE Trans. on Software Engineering, 2011,37(3):387-409. [doi: 10.1109/TSE.2010.92]
    [12] Kwiatkowska M, Norman G, Parker D. Probabilistic model checking for systems biology. In: Iyengar MS, ed. Proc. of the Symbolic Systems Biology. Sudbury: Jones and Bartlett Publishers, 2010. 31-59.
    [13] Clarke EM, Grumberg O, Long DE. Model checking and abstraction. In: Proc. of the 19th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. New York: ACM Press, 1992. 343-354.
    [14] Huth M. An abstraction framework for mixed non-deterministic and probabilistic systems. In: Baier C, Haverkort B, Hermanns H, Katoen J P, Siegle M, eds. Proc. of the Validation of Stochastic Systems. Berlin, Heidelberg: Springer-Verlag, 2004. 419-　444. [doi: 10.1007/978-3-540-24611-4_12]
    [15] Liu Y, Miao HK, Zeng HW, Ma Y, Liu P. Nondeterministic probabilistic Petri net: A new method to study qualitative and quantitative behaviors of system. Journal of Computer Science and Technology, 2013,28(1):203-216. [doi: 10.1007/s11390-013- 1323-7]
    [16] Beauquier D. On probabilistic timed automata. Theoretical Computer Science, 2003,292(1):65-84. [doi: 10.1016/S0304-3975(01) 00215-8]
    [17] Kwiatkowska M, Norman G, Segala R, Sproston J. Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 2002,282(1):101-150. [doi: 10.1016/S0304-3975(01)00046-9]
    [18] Howard RA. Dynamic Programming and Markov Processes. Hoboken: John Wiley and Sons, 1960.
    [19] Bertsekas DP. Dynamic Programming and Optimal Control. 3rd ed., Cambridge: MIT Press, 2011.
    [20] Hermanns H. Interactive Markov Chains and the Quest for Quantified Quality. Berlin, Heidelberg: Springer-Verlag, 2002.
    [21] Kwiatkowska M, Norman G, Sproston J, Wang F. Symbolic model checking for probabilistic timed automata. Information and Computation, 2007,205(7):1027-1077. [doi: 10.1016/j.ic.2007.01.004]
    [22] de Alfaro L. Formal verification of probabilistic systems [Ph.D. Thesis]. Stanford: Stanford University, 1997.
    [23] Cloth L, Haverkort B, Hermanns H, Katoen JP, Baier C. Model checking pathCSL. In: Proc. of the 6th Int'l Workshop Performability Modeling of Computer and Communication Systems. 2003. 19-22.
    [24] Kuntz M, Siegle M. A stochastic extension of the logic PDL. In: Proc. of the 6th Int'l Workshop Performability Modeling of Computer and Communication Systems. 2003. 58-61.
    [25] Baier C, Cloth L, Haverkort BR, Kuntz M, Siegle M. Model checking Markov chains with actions and state labels. IEEE Trans. on Software Engineering, 2007,33(4):209-224. [doi: 10.1109/TSE.2007.36]
    [26] Liu Y. Quantitative verification of trustworthy service flow by stochastic model checking. Journal of Software Engineering, 2014, 8(3):152-168. [doi: 10.3923/jse.2014.152.168]
    [27] de Alfaro L, Roy P. Magnifying-Lens abstraction for Markov decision processes. In: Proc. of the 19th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2007. 325-338. [doi: 10.1007/978-3-540-73368-3_38]
    [28] Didier F, Henzinger T, Mateescu M, Wolf V. Sabre: A tool for stochastic analysis of biochemical reaction networks. In: Proc. of the 7th Int'l Conf. on Quantitative Evaluation of Systems. Washington: IEEE Computer Society Press, 2010. 193-194. [doi: 10. 1109/QEST.2010.33]
    [29] Della PG, Intrigila B, Melatti I, Tronci E, Venturini ZM. Bounded probabilistic model checking with the murphi verifier. In: Proc. of the 5th Int'l Conf. on Formal Methods in Computer-Aided Design. Berlin, Heidelberg: Springer-Verlag, 2004. 214-229. [doi: 10.1007/978-3-540-30494-4_16]
    [30] Zhou CH, Liu ZF, Wang CD. Bounded model checking for probabilistic computation tree logic. Ruan Jian Xue Bao/Journal of Software, 2012,23(7):1656-1668 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4089.htm [doi: 10.3724/SP. J.1001.2012.04089]
    [31] Filieri A, Ghezzi C, Tamburrelli G. Run-Time efficient probabilistic model checking. In: Proc. of the 33rd ACM/IEEE Int'l Conf. on Software Engineering. Washington: IEEE Computer Society Press, 2011. 341-350. [doi: 10.1145/1985793.1985840]
    [32] Larsen K, Skou A. Bisimulation through probabilistic testing. Information and Computation, 1991,94(1):1-28. [doi: 10.1016/ 0890-5401(91)90030-6]
    [33] Milner R. A Calculus of Communicating Systems. Berlin, Heidelberg: Springer-Verlag, 1980.
    [34] Park D. Concurrency and automata on infinite sequences. In: Proc. of the 5th GI- Conf. on Theoretical Computer Science. Berlin, Heidelberg: Springer-Verlag, 1981. 167-183. [doi: 10.1007/BFb0017309]
    [35] Buchholz P. Exact and ordinary lumpability infinite Markov chains. Journal of Applied Probability, 1994,31(1):59-75. [doi: 10. 2307/3215235]
    [36] Segala R, Lynch N. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 1995,2(2):250-273.
    [37] Paige R, Tarjan R. Three partition refinement algorithms. SIAM Journal of Computation, 1987,16(6):973-989. [doi: 10.1137/ 0216062]
    [38] Huynh T, Tian L. On some equivalence relations for probabilistic processes. Fundamenta Informaticae, 1992,17(3):211-234.
    [39] Aziz A, Singhal V, Balarin F, Brayton RK, Sangiovanni-Vincentelli AL. It usually works: The temporal logic of stochastic systems. In: Proc. of the 7th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 1995. 155-　165. [doi: 10.1007/3-540-60045-0_48]
    [40] Hermanns H, Katoen J. Automated compositional Markov chain generation for a plain-old telephone system. Science of Computer Programming, 2000,36(1):97-127. [doi: 10.1016/S0167-6423(99)00019-2]
    [41] Derisavi S. A symbolic algorithm for optimal Markov chain lumping. In: Proc. of the 13th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2007. 139-154. [doi: 10.1007/978-3-540- 71209-1_13]
    [42] Christian D, Katoen JP, Parker D. SMT-Based bisimulation minimization of markov models. In: Proc. of the 14th Int'l Conf. on Verification, Model Checking and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2013. 28-47. [doi: 10.1007/978- 3-642-35873-9_5]
    [43] Song L, Zhang LJ, Godskesen JC, Nielson F. Bisimulations meet PCTL equivalences for probabilistic automata. Logical Methods in Computer Science, 2013,9(2):1-34.
    [44] Baier C, Hermanns H. Weak bisimulation for fully probabilistic processes. In: Proc. of the 9th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 1997. 119-130. [doi: 10.1007/3-540-63166-6_14]
    [45] Philippou A, Lee I, Sokolsky O. Weak bisimulation for probabilistic systems. In: Proc. of the 11th Int'l Conf. on Concurrency Theory. Berlin, Heidelberg: Springer-Verlag, 2000. 334-349. [doi: 10.1007/3-540-44618-4_25]
    [46] Cattani S, Segala R. Decision algorithms for probabilistic bisimulation. In: Proc. of the 13th Int'l Conf. on Concurrency Theory. Berlin, Heidelberg: Springer-Verlag, 2002. 371-385. [doi: 10.1007/3-540-45694-5_25]
    [47] Hermanns H, Turrini A. Deciding probabilistic automata weak bisimulation in polynomial time. In: Proc. of the 32nd Int'l Conf. on Foundations of Software Technology and Theoretical Computer Science. Saarbrücken/Wadern: Dagstuhl Publishing, 2012. 435-447.
    [48] Jonsson B, Larsen KG. Specification and refinement of probabilistic processes. In: Proc. of the 6th Annual IEEE Symp. on Logic in Computer Science. Washington: IEEE Computer Society Press, 1991. 266-277. [doi: 10.1109/LICS.1991.151651]
    [49] Milner R. An algebraic definition of simulation between programs. In: Proc. of the 2nd Int'l Joint Conf. on Artificial Intelligence. London: William Kaufmann Inc., 1971. 481-489.
    [50] Clarke EM, Grumberg O, Long DE. Model checking and abstraction. ACM Trans. on Programming Languages and Systems, 1994, 16(5):1512-1542. [doi: 10.1145/186025.186051]
    [51] Baier C, Katoen JP, Hermanns H, Wolf V. Comparative branching-time semantics for Markov chains. Information and Computation, 2005,200(2):149-214. [doi: 10.1016/j.ic.2005.03.001]
    [52] Zhang LJ. Decision algorithms for probabilistic simulations [Ph.D. Thesis]. Saarbrücken: Saarland University, 2008.
    [53] Gallo G, Grigoriadis MD, Tarjan RE. A fast parametric maximum flow algorithm and applications. SIAM Journal on Computing, 1989,18(1):30-55. [doi: 10.1137/0218003]
    [54] Zhang LJ, Hermanns H, Eisenbrand F, Jansen DN. Flow faster: Efficient decision algorithms for probabilistic simulations. Logical Methods in Computer Science, 2008,4(4:6):1-23. [doi: 10.2168/LMCS-4(4:6)2008]
    [55] Btic models. In: Proc. of the 16th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2010. 353-357. [doi: 10.1007/978-3-642-12002-2_30]
    [92] Chadha R, Viswanathan M. A counterexample guided abstraction-refinement framework for Markov decision processes. ACM Trans. on Computational Logic, 2010,12(1):1-49. [doi: 10.1145/1838552.1838553]
    [93] D'Argenio P, Jeannet B, Jensen H, Larsen K. Reachability analysis of probabilistic systems by successive refinements. In: Proc. of the Joint Int'l Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification. Berlin, Heidelberg: Springer-Verlag, 2001. 39-56. [doi: 10.1007/3-540-44804-7_3]
    [94] Kwiatkowska M, Norman G, Parker D. Game-Based abstraction for Markov decision processes. In: Proc. of the 3rd Int'l Conf. on Quantitative Evaluation of Systems. Washington: IEEE Computer Science Press, 2006. 157-166. [doi: 10.1109/QEST.2006.19]
    [95] Condon A. The complexity of stochastic games. Information and Computation, 1992,96(2):203-224. [doi: 10.1016/0890-5401(92) 90048-K]
    [96] Kattenbelt M, Kwiatkowska M, Norman G, Parker D. A game-based abstraction refinement framework for Markov decision processes. Formal Methods in System Design, 2010,36(3):246-280. [doi: 10.1007/s10703-010-0097-6]
    [97] Wachter B, Zhang LJ. Best probabilistic transformers. In: Proc. of the 11th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2010. 362-379. [doi: 10.1007/978-3-642-11319-2_26]
    [98] Huth M, Jagadeesan R, Schmidt D. Modal transition systems: A foundation for three-valued program analysis. In: Proc. of the 10th European Symp. on Programming Languages and Systems. Berlin, Heidelberg: Springer-Verlag, 2001. 155-169. [doi: 10. 1007/3-540-45309-1_11]
    [99] Godefroid P, Jagadeesan R. On the expressiveness of 3-valued models. In: Proc. of the 4th Int'l Conf. on Verification, Model Checking, and Abstract Interpretation. Berlin, Heidelberg: Springer-Verlag, 2003. 206-222. [doi: 10.1007/3-540-36384-X_18]
    [100] Fecher H, Leucker, M, Wolf, V. Don't know in probabilistic systems. In: Proc. of the 13th Int'l Conf. on Model Checking Software. Berlin, Heidelberg: Springer-Verlag, 2006. 71-88. [doi: 10.1007/11691617_5]
    [101] Wang Y. Reasoning about uncertain information compositionally. In: Proc. of the 3rd Int'l School and Symp. on Real-Time and Fault-Tolerant Systems. Berlin, Heidelberg: Springer-Verlag, 1994. 680-693.
    [102] Katoen JP, Klink D, Leucker M, Wolf V. Three-Valued abstraction for continuous-time Markov chains. In: Proc. 19th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2007. 316-329. [doi: 10.1007/978-3-540-73368-3_37]
    [103] Katoen JP? Klink D, Leucker M, Wolf V. Three-Valued abstraction for probabilistic systems. Journal on Logic and Algebraic Programming, 2012,81(4):356-389. [doi: 10.1016/j.jlap.2012.03.007]
    [104] Klink D. Three-Valued abstraction for stochastic systems [Ph.D. Thesis]. Aachen: RWTH Aachen University, 2010.
    [105] Huth M, Piterman N, Wagner D. p-Automata: New foundations for discrete-time probabilistic verification. Performance Evaluation, 2012,69(7-8):356-378. [doi: 10.1016/j.peva.2012.05.005]
    [106] Song L, Zhang LJ, Hermanns H, Godskesen JC. Incremental bisimulation abstraction refinement. In: Proc. of the 13th Int'l Conf. on Application of Concurrency to System Design. Washington: IEEE Computer Science Press, 2013. 98-107. [doi: 10.1109/ ACSD.2013.5]
    [107] Crafa S, Ranzato F. Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation. Formal Methods in System Design, 2012,40(3):356-376. [doi: 10.1007/s10703-012-0147-3]
    [108] Cousot P, Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of the 4th ACM SIGACT-SIGPLAN Symp. on Principles of programming languages. New York: ACM Press, 1977. 238-252. [doi: 10.1145/512950.512973]
    [109] Cousot P, Cousot R. Systematic design of program analysis frameworks. In: Proc. of the 6th ACM SIGACT-SIGPLAN Symp. on Principles of programming languages. New York: ACM Press, 1979. 269-282. [doi: 10.1145/567752.567778]
    [110] Draeger K, Kwiatkowska M, Parker D, Qu HY. Local abstraction refinement for probabilistic timed programs. Theoretical Computer Science, 2014,538:37-53. [doi: 10.1016/j.tcs.2013.07.013]
    [111] Sher F, Katoen JP. Compositional abstraction techniques for probabilistic automata. In: Proc. of the 7th IFIP Int'l Conf. on Theoretical Computer Science. Berlin, Heidelberg: Springer-Verlag, 2012. 325-341. [doi: 10.1007/978-3-642-33475-7_23]
    [112] Komuravelli A, Pasareanu CS, Clarke EM. Assume-Guarantee abstraction refinement for ばrobabilistic systems. In: Proc. of the 24th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2012. 310-326. [doi: 10.1007/978-3-642- 31424-7_25]
    [113] Timmer M, Stoelinga M, van de Pol J. Confluence reduction for probabilistic systems. In: Proc. of the 17th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2011. 311-325. [doi: 10. 1007/978-3-642-19835-9_29]
    [114] Mitchell TM. Machine Learning. New York: McGraw-Hill Science/Engineering/Math, 1997.
    [115] Mao H, Chen Y, Jaeger M, Nielsen TD, Larsen KG, Nielsen B. Learning Markov decision processes for model checking. Electronic Proc. in Theoretical Computer Science, 2012,103:49-63. [doi: 10.4204/EPTCS.103.6]
    [116] Kwiatkowska M, Norman G, Parker D, Qu H. Assume-Guarantee verification for probabilistic systems. In: Proc. of the 16th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2010. 23-37. [doi: 10.1007/978-3-642-12002-2_3]
    [117] Fioriti LMF, Hermanns H. Heuristics for probabilistic timed automata with abstraction refinement. In: Proc. of the 16th Int'l GI/ITG Conf. on Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance. Berlin, Heidelberg: Springer-Verlag, 2012. 151-165. [doi: 10.1007/978-3-642-28540-0_11]
    [118] Hahn EM. Model checking stochastic hybrid systems [Ph.D. Thesis]. Saarbrücken: Saarland University, 2013.
    [119] Simaitis A. Automatic verification of competitive stochastic systems [Ph.D. Thesis]. Oxford: University of Oxford, 2014.l T. Dynamic symmetry reduction. In: Proc. of the 11th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2005. 382-396. [doi: 10.1007/978-3-540-31980- 1_25]
    [85] Wahl T, Blanc N, Emerson EA. SVISS: Symbolic verification of symmetric systems. In: Proc. of the 14th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 2008. 459-462. [doi: 10. 1007/978-3-540-78800-3_34]
    [86] Donaldson A, Miller A, Parker D. Language-Level symmetry reduction for probabilistic model checking. In: Proc. of the 6th Int'l Conf. on Quantitative Evaluation of Systems. Washington: IEEE Computer Science Press, 2009. 289-298. [doi: 10.1109/QEST. 2009.21]
    [87] Christopher P. Probabilistic symmetry reduction [Ph.D. Thesis]. University of Glasgow, 2012.
    [88] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided abstraction refinement. In: Proc. of the 12th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2000. 154-169. [doi: 10.1007/10722167_15]
    [89] Wachter B, Zhang LJ, Hermanns H. Probabilistic model checking modulo theories. In: Proc. of the 4th Int'l Conf. on Quantitative Evaluation of Systems. Washington: IEEE Computer Science Press, 2007. 129-138. [doi: 10.1109/QEST.2007.10]
    [90] Hermanns, H, Wachter, B, Zhang L. Probabilistic CEGAR. In: Proc. of 2008 the 20th Int'l Conf. on Computer Aided Verification. Berlin, Heidelberg: Springer-Verlag, 2007. 162-175. [doi: 10.1007/978-3-540-70545-1_16]
    [91] Hahn EM, Hermanns H, Wachter B, Zhang L. PASS: Abstraction refinement for infinite probabilis?????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

刘阳,李宣东,马艳.面向随机模型检验的模型抽象技术.软件学报,2015,26(8):1853-1870

复制
分享
文章指标
  • 点击次数:5558
  • 下载次数: 7662
  • HTML阅读次数: 3579
  • 引用次数: 0
历史
  • 收稿日期:2014-07-08
  • 最后修改日期:2015-03-27
  • 在线发布日期: 2015-08-05
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19765710位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号