微信服务号

微信订阅号

2025-4-21- 17
Home > Archive>Volume 26, Issue 8, 2015 >1853-1870. DOI:10.13328/j.cnki.jos.004838
PDF HTML XML Export Cite reminder
Model Abstraction for Stochastic Model Checking
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [90]
    • |
  • Related
    • | | |
  • Comments
    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.

    Reference
    [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?????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????????
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 08,2014
  • Revised:March 27,2015
  • Online: August 05,2015
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2036718Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063