微信服务号

微信订阅号

2025-4-3- 17
Home > Archive>Volume 33, Issue 7, 2022 >2367-2410. DOI:10.13328/j.cnki.jos.006587
PDF HTML XML Export Cite reminder
Survey on Requirements Classification and Formalization of Trustworthy Systems
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [160]
    • |
  • Related [20]
    • | | |
  • Comments
    Abstract:

    Computer systems have been applied in many different areas, and the failure of these systems may bring catastrophic results. Systems in different areas have different requirements, and how to build trustworthy computer systems with high quality is the challenge faced by all these areas. Recently, formal methods with rigorous mathematical foundation have been widely recognized as effective methods for developing trustworthy software and hardware systems. Based on formal methods, this paper presents a classification of requirements of systems and their formalization, to support the design of trustworthy systems. First of all, six types of system characteristics are considered, namely, sequential systems, reactive systems, parallel and communicating systems, real-time systems, probabilistic and stochastic systems, and continuous and hybrid systems. All these systems may run in different application scenarios, with their respective requirements. Four classes of scenarios are considered, i.e., hardware systems, security protocols, information flow, and AI systems. For each class of systems and application scenarios above, the related formal methods are introduced and summarized, including formal modeling, property specification, verification methods and tools. This will allow users of formal methods to choose, based on different system characteristics and application scenarios, the appropriate formal models, verification methods and tools, which ultimately helps the design of more trustworthy systems.

    Reference
    [1] Becker S, Boskovic M, Dhama A, Giesecke S, Happe J, Hasselbring W, Koziolek H, Lipskoch H, Meyer R, Muhle M, Paul A, Ploski J, Rohr M, Swaminathan M, Warns T, Winteler D. Trustworthy software systems:A discussion of basic concepts and terminology. ACM SIGSOFT Software Engineering Notes, 2006, 31(6):1-18.
    [2] Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods:Practice and experience. ACM Computing Surveys, 2009, 41(4):Article No.19.
    [3] Gleirshcer M, Foster S, Woodcock J. New opportunities for integrated formal methods. ACM Computing Surveys, 2020, 52(6):Article No.117.
    [4] Baier C, Katoen J. Principles of Model Checking. MIT Press, 2008.
    [5] Clarke EM, Henzinger TA, Veith H. Handbook of Model Checking. Springer, 2018.
    [6] Clarke EM, Grumberg O, Kroening D, et al. Model Checking. MIT Press, 2018.
    [7] Robinson A, Voronkov A. Handbook of Automated Reasoning. Elsevier, 2001.
    [8] Harrison J. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
    [9] Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ. Symbolic model checking:1020 states and beyond. Information and Computation, 1992, 98(2):142-170.
    [10] Biere A, Cimatti A, Clarke EM, Zhu Y. Symbolic model checking without BDDs. In:Proc. of the TACAS. 1999. 193-207.
    [11] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM (JACM), 2003, 50(5):752-794.
    [12] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1):33-61(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [13] Bu L, Chen LQ, Chen Z, et al. Development and trends of research in formal methods. In:China Computer Federation Proc. 2018. 1-68(in Chinese).
    [14] Peled DA. Software Reliability Methods. Springer, 2001.
    [15] Nielson F, Nielson HR. Formal Methods, An Appetizer. Springer, 2019.
    [16] Zhang J, Zhang C, Xuan JF, Xiong YF, Wang QX, Liang B, Li L, Dou WS, Chen ZB, Chen LQ, Cai Y. Recent progress in program analysis. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1):80-109(in Chinese with English abstract). http://www. jos.org.cn/1000-9825/5651.htm[doi:10.13328/j.cnki.jos.005651]
    [17] Nielson F, Nielson HR, Hankin C. Principles of Program Analysis. Springer, 1999.
    [18] Plotkin G. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 1981, 60:17-139.
    [19] Scott DS. Outline of a mathematical theory of computation. 1970. https://www.researchgate.net/publication/242406560
    [20] Floyd RW. Assigning meanings to programs. Proc. of Symposia in Applied Mathematics, 1967, 19:19-32.
    [21] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10):576-580.
    [22] Dijkstra EW. A Discipline of Programming. Prentice Hall, 1976.
    [23] Apt KR, Olderog ER. Fifty years of Hoare's logic. Formal Aspects of Computing, 2019, 31:751-807.
    [24] Reynolds JC. Separation logic:A logic for shared mutable data structures. In:Proc. of the LICS. 2002. 55-74.
    [25] Chin WN, David C, Nguyen H, Qin S. Enhancing modular OO verification with separation logic. In:Proc. of the POPL. 2008. 87-99.
    [26] Parkinson M, Bierman GM. Separation logic, abstraction and inheritance. In:Proc. of the POPL. 2008. 75-86.
    [27] Bjorner N, Browne A, Manna Z. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 1997, 173(1):49-87.
    [28] Cook B, Podelski A, Rybalchenko A. Proving program termination. Communications of the ACM, 2011, 54(5):88-98.
    [29] Yang L, Zhou CC, Zhan NJ, et al. Recent advances in program verification through computer algebra. Frontiers of Computer Science, 2010, 4(1):1-16.
    [30] McMillan KL. Interpolation and SAT-based model checking. In:Proc. of the CAV. 2003. 1-13.
    [31] Garg P, Loding C, Madhusudan P, Neider D. ICE:A robust framework for learning invariants. In:Proc. of the CAV. 2014. 69-87.
    [32] Si X, Dai H, Raghothaman M, Naik M, Song L. Learning loop invariants for program verification. In:Advances in Neural Information Processing Systems. 2018. 7751-7762.
    [33] Yao J, Ryan G, Wong J, Jana S, Gu R. Learning nonlinear loop invariants with gated continuous logic networks. In:Proc. of the PLDI. 2020. 106-120.
    [34] Podelski A, Rybalchenko A. A complete method for the synthesis of linear ranking functions. In:Proc. of the VMCAI. 2004. 239-251.
    [35] Heizmann M, Hoenicke J, Podelski A. Termination analysis by learning terminating programs. In:Proc. of the CAV. 2014. 797-813.
    [36] Chen Y, Heizmann M, Lengál O, Li Y, Tsai M, Turrini A, Zhang L. Advanced automata-based algorithms for program termination checking. In:Proc. of the PLDI. 2018. 135-150.
    [37] Jhala R, Majumdar R. Software model checking. ACM Computing Surveys, 2009, 41(4):Article No.21.
    [38] Alur R, Benedikt M, Etessami K, Godefroid P, Reps TW, Yannakakis M. Analysis of recursive state machines. ACM Trans. on Programming Languages and Systems, 2005, 27(4):786-818.
    [39] Bouajjani A, Esparza J, Maler O. Reachability analysis of pushdown automata:Application to model checking. In:Proc. of the CONCUR. 1997. 135-150.
    [40] Esparza J, Hansel D, Rossmanith P, Schwoon S. Efficient algorithms for model checking pushdown systems. In:Proc. of the CAV. 2000. 232-247.
    [41] Alur R, Madhusudan P. Adding nesting structure to words. Journal of the ACM (JACM), 2009, 56(3):Article No.16.
    [42] Jacobs B, Smans J, Philippaerts P, Vogels F, Penninckx W, Piessens F. VeriFast:A powerful, sound, predictable, fast verifier for C and Java. In:Proc. of the NASA Formal Methods. 2011. 41-55.
    [43] Rustan K, Leino M. Dafny:An automatic program verifier for functional correctness. In:Proc. of the LPAR. 2010. 348-370.
    [44] Filliatre JC, Paskevich A. Why3-Where programs meet provers. In:Proc. of the ESOP. 2013. 125-128.
    [45] Kirchner F, Kosmatov N, Prevosto V, Signoles J, Yakobowski B. Frama-C:A software analysis perspective. Formal Aspects of Computing, 2015, 27(3):573-609.
    [46] Ball T, Levin V, Rajamani SK. A decade of software model checking with SLAM. Communications of the ACM, 2011, 54(7):68-76.
    [47] O'Hearn PW. Continuous reasoning:Scaling the impact of formal methods. In:Proc. of the LICS. 2018. 13-25.
    [48] Keller R. Formal verification of parallel programs. Communications of the ACM, 1976, 19(7):371-384.
    [49] Kropf T. Introduction to Formal Hardware Verification. Springer, 1999.
    [50] Büchi, JR. On a decision method in restricted second order arithmetic. In:Proc. of the Int'l Congress on Logic, Method, and Philosophy of Science. 1962. 1-12.
    [51] McNaughton R. Testing and generating infinite sequences by a finite automaton. Information and Control, 1966, 9:521-530.
    [52] Rabin MO. Decidability of second order theories and automata on infinite trees. Trans. of the American Mathematical Society, 1969, 141:1-35.
    [53] Vardi MY, Wolper P. An automata-theoretic approach to automatic program verification (preliminary report). In:Proc. of the LICS. 1986. 332-344.
    [54] Pnueli A. The temporal logic of programs. In:Proc. of the FOCS. 1977. 46-57.
    [55] Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching-time temporal logic. Logics of Programs, 1981, 131:52-71.
    [56] Kupferman O, Vardi MY. Model checking of safety properties. Formal Methods in System Design, 2001, 19(3):291-314.
    [57] Courcoubetis C, Vardi MY, Wolper P, Yannakakis M. Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1992, 1(2-3):275-288.
    [58] Ben-Ari M, Pnueli A, Manna Z. The temporal logic of branching time. Acta Informatica, 1983, 20:207-226.
    [59] Queille JP, Sifakis J. Specification and verification of concurrent systems in CESAR. In:Proc. of the Int'l Symp. on Programming, Vol.137. 1982. 337-351.
    [60] Clarke EM, Emerson EA, Sistla AP. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. on Programming Languages and Systems, 1986, 8(2):244-263.
    [61] Iwashita H, Nakata T, Hirose F. CTL model checking based on forward state traversal. In:Proc. of the ICCAD. 1996. 82-87.
    [62] Emerson EA, Halpern JY. "Sometimes" and "not never" revisited:On branching versus linear-time temporal logic. Journal of the ACM (JACM), 1986, 33(1):151-178.
    [63] Janin D, Walukiewicz I. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In:Proc. of the Int'l Conf. on Concurrency Theory. 1996. 263-277.
    [64] Thomas W. Infinite games and verification. In:Proc. of the Int'l Conf. on Computer Aided Verification. 2002. 58-65.
    [65] Kozen D. Results on the propositional mu-calculus. Theoretical Computer Science, 1983, 27(3):333-354.
    [66] Kozen D. A finite model theorem for the propositional mu-calculus. Studia Logica, 1988, 47(3):233-241.
    [67] Berwanger D, Gradel E, Lenzi G. The variable hierarchy of the mu-calculus is strict. Theory of Computing Systems, 2007, 40(4):437-466.
    [68] McNaughton R. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 1993, 65(2):149-184.
    [69] Jurdziński M. Small progress measures for solving parity games. In:Proc. of the Annual Symp. on Theoretical Aspects of Computer Science. 2000. 290-301.
    [70] Schewe S. Solving parity games in big steps. In:Proc. of the Int'l Conf. on Foundations of Software Technology and Theoretical Computer Science. 2007. 449-460.
    [71] Lamport L. Proving the correctness of multiprocess programs. IEEE Trans. on Software Engineering, 1977, 3(2):125-143.
    [72] Alpern B, Schneider FB. Defining liveness. Information Processing Letters, 1985, 21(4):181-185.
    [73] Manolios P, Trefler RJ. Safety and liveness in branching time. In:Proc. of the LICS. 2001. 366-374.
    [74] Manna Z, Pnueli A. A hierarchy of temporal properties. In:Proc. of the ACM Symp. on Principles of Distributed Computing. 1990. 377-410.
    [75] Cimatti A, Clarke EM, Giunchiglia F, Roveri M. NuSMV:A new symbolic model checker. Int'l Journal on Software Tools for Technology Transfer, 2000, 2(4):410-425.
    [76] Holzmann G. The model checker SPIN. IEEE Trans. on Software Engineering, 1997, 23(5):279-295.
    [77] Dill D. The Murphi verification system. In:Proc. of the CAV. 1996. 390-393.
    [78] Lamport L. Specifying Systems. Boston:Addison-Wesley, 2002.
    [79] Havelund K, Shankar N. Experiments in theorem proving and model checking for protocol verification. In:Proc. of the IBAFM. 1996. 662-681.
    [80] Biere A, Kick A. A case study on different modeling approaches based on model checking-verifying numerous versions of the alternating bit protocol with SMV. 1995. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.31.7109&rep=rep1&type=pdf
    [81] McMillan KL, Schwalbe J. Formal verification of the encore Gigamaxcache consistency protocol. In:Proc. of the Int'l Symp. on Shared Memory Multiprocessors. 1991. 242-251.
    [82] Clarke EM, Grumberg O, Hiraishi H, Jha S, Long DE, McMillan KL, Ness LA. Verification of the futurebus+cache coherence protocol. Formal Methods in System Design, 1995, 6(2):217-232.
    [83] Moon I. Modeling programmable logic controllers for logic verification. IEEE Control Systems, 1994, 14(2):53-59.
    [84] Barrett G. Model checking in practice:The T9000 virtual channel processor. IEEE Trans. on Software Engineering, 1995, 21(2):69-78.
    [85] Anderson RJ, Beame P, Burns S, Chan W, Modugno F, Notkin D, Reese JD. Model checking large software specifications. In:Proc. of the SIGSOFT FSE. 1996. 156-166.
    [86] Holzmann GJ. Protocol design:Redefining the state of the art. IEEE Software, 1992, 9(1):17-22.
    [87] Ruane LM. Process synchronization in the UTS kernel. Computer Systems, 1990, 3(3):387-421.
    [88] D'Argenio PR, Katoen JP, Ruys T, Tretmans J. Modeling and verifying a bounded retransmission protocol. In:Proc. of the Workshop Applied Formal Methods in System Design. 1996. 114-127.
    [89] Jensen HE, Larsen KG, Skou A. Modelling and analysis of a collision avoidance protocol using SPIN and UPPAAL. In:Proc. of the Spin Verification System. 1996. 261-277.
    [90] Ruys T, Langerak R. Validation of Bosch'mobile communication network architecture with SPIN. In:Proc. of the 3rd SPIN Workshop. 1997. 75-89.
    [91] Dill DL, Park S, Nowatzyk AG. Formal specification of abstract memory models. In:Proc. of the Symp. on Research on Integrated Systems. 1993. 38-52.
    [92] Dill DL, Drexler AJ, Hu AJ, Yang CH. Protocol verification as a hardware design aid. In:Proc. of the IEEE Int'l Conf. on Computer Design. 1992. 522-525.
    [93] Lenoski D, Laudon J, Gharachorloo K, Weber WD, Gupta A, Hennessy J, Horowitz M, Lam M. The Stanford DASH multiprocessor. Computer, 1992, 25(3):63-79.
    [94] Mitchell JC, Mitchell M, Stern U. Automated analysis of cryptographic protocols using Mur/spl phi/. In:Proc. of the IEEE Symp. on Security and Privacy. 1997. 141-151.
    [95] Needham RM, Schroeder MD. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978, 21(12):993-999.
    [96] Tatebayashi M, Matsuaaki N, Newman D. Key distribution protocol for digital mobile communication systems. In:Proc. of the CRYPTO. 1990. 324-333.
    [97] Lamport L. The temporal logic of actions. ACM Trans. on Programming Languages and Systems (TOPLAS), 1994, 16(3):872-923.
    [98] Beers R. Pre-RTL formal verification:An Intel experience. In:Proc. of the DAC. 2008. 806-811.
    [99] Newcombe C, Rath T, Zhang F, Munteamu B, Brooker M, Deardeuff M. How Amazon web services uses formal methods. Communications of the ACM, 2015, 58(4):66-73.
    [100] Milner R. A Calculus of Communicating Systems. New York:Springer, 1980.
    [101] Hennessy MCB, Milner R. Algebraic laws for nondeterminism and concurrency. Journal of the ACM (JACM), 1985, 32(1):137-161.
    [102] Victor B. The mobility workbench user's guide:Polyadic version 3.122. Department of Information Technology, Uppsala University, 1995. https://www.it.uu.se/profundis/mwb-dist/guide-3.122.pdf
    [103] Victor B. A verification tool for the polyadic pi-calculus[MS. Thesis]. Department of Computer Systems, Uppsala University, 1994.
    [104] Hoare CAR. Communicating Sequential Processes. Englewood:Prentice-Hall, 1985.
    [105] Brookes SD. On the relationship of CCS and CSP. In:Proc. of the ICALP. 1983. 83-96.
    [106] Bundgaard M, Milner R. Unfolding CSP. In:Proc. of the Reflections on the Work of C.A.R. Hoare. 2010. 213-228.
    [107] Roscoe AW. Understanding concurrent systems. New York:Springer, 2010.
    [108] Schneider SA, Davies J. Timed CSP:Theory and practice. In:Proc. of the REX Workshop. 1991. 640-675.
    [109] Gibson-Robinson T. FDR3-A modern refinement checker for CSP. In:Proc. of the TACAS. 2014. 187-201.
    [110] Armstrong P, Lowe G, Ouaknine J, Roscoe AW. Model Checking Timed CSP. In:HOWARD-60. A Festschrift on the Occasion of Howard Barringer's 60th Birthday, Vol.42. 2014. 2014. 13-33.
    [111] Ouaknine J. Discrete analysis of continuous behaviour in real-time concurrent systems. Technical Report, University of Oxford, 2000. https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.365293
    [112] Donovan B, Norris P, Lowe G. Analyzing a library of security protocols using Casper and FDR. In:Proc. of the Workshop on Formal Methods and Security Protocols. 1999. https://www.cs.ox.ac.uk/publications/publication676-abstract.html
    [113] Brackin SH. Evaluating and improving protocol analysis by automatic proof. In:Proc. of the 11th IEEE Computer Security Foundations Workshop. 1998.[doi:10.1109/CSFW.1998.683164]
    [114] Peterson JL. Petri Net Theory and the Modeling of Systems. Englewood:Prentice-Hall, 1981.
    [115] Murata T. Petri nets:Properties, analysis and applications. In:Proc. of the IEEE. 1989. 541-580.
    [116] Abdulla PA. General decidability theorems for infinite-state systems. In:Proc. of the LICS. 1996. 313-321.
    [117] Reisig W, Rozenberg G. Lectures on Petri Nets I:Basic Models:Advances in Petri Nets. New York:Springer, 1998.
    [118] Kostin A. Using Transition Invariants for Reachability Analysis of Petri Nets. INTECH Open Access Publisher, 2008.
    [119] Benjamin M, Bergenthum R. Travis-An online tool for the synthesis and analysis of Petri nets with final states. In:Proc. of the Int'l Conf. on Application and Theory of Petri Nets and Concurrency. 2017. 101-111.
    [120] Hillah LM, Kordon F. Petri nets repository:A tool to benchmark and debug Petri net tools. In:Proc. of the Int'l Conf. on Application and Theory of Petri Nets and Concurrency. 2017. 125-135.
    [121] Hu X, Li J, Li ZJ. Modelling and performance analysis of IEEE 802.11 DCF using coloured Petri nets. The Computer Journal, 2016, 59(10):1563-1580.
    [122] Berthelot G, Terrat R. Petri nets theory for the correctness of protocols. IEEE Trans. on Communications, 1982, 30(12):2497-2505.
    [123] PAT:Process analysis toolkit. 2021. https://pat.comp.nus.edu.sg
    [124] Sun J, Liu Y, Dong JS, Pang J. PAT:Towards flexible verification under fairness. In:Proc. of the CAV. 2009. 709-714.
    [125] Liu Y, Sun J, Dong JS. PAT 3:An extensible architecture for building multi-domain model checkers. In:Proc. of the ISSRE. 2011. 190-199.
    [126] Fernando D, Dong N, Jégourel C, Dong JS. Verification of strong Nash-equilibrium for probabilistic BAR systems. In:Proc. of the Formal Engineering Methods. 2018. 106-123.
    [127] Fernando D, Dong N, Jégourel C, Dong JS. Verification of Nash-equilibrium for probabilistic BAR systems. In:Proc. of the ICECCS. 2016. 53-62.
    [128] Thin WYMM, Dong NP, Bai GD, Dong JS. Formal analysis of a proof-of-stake blockchain. In:Proc. of the 23rd Int'l Conf. on Engineering of Complex Computer Systems (ICECCS). 2018. 197-200.
    [129] Li L, Sun J, Liu Y. A formal specification and verification framework for timed security protocols. IEEE Trans. on Software Engineering, 2017, 44(8):725-746.
    [130] Ling S, Liu S, Hao J. Towards solving decision making problems using probabilistic model checking. In:Proc. of the ICECCS. 2017. 150-153.
    [131] Alur R, Dill D. Automata for modeling real-time systems. In:Proc. of the ICALP. 1990. 322-335.
    [132] Alur R, Dill D. A theory of timed automata. Theoretical Computer Science, 1994, 126(2):183-235.
    [133] Cerans K. Decidability of bisimulation equivalences for parallel timer processes. In:Proc. of the CAV. 1992. 302-315.
    [134] Konrad S, Cheng BHC. Real-time specification patterns. In:Proc. of the ICSE. 2005. 372-381.
    [135] Bouyer P, Laroussinie F, Markey N, et al. Timed temporal logics. In:Proc. of the Models, Algorithms, Logics and Tools. 2017. 211-230.
    [136] Alur R, Courcoubetis C, Dill D. Model-checking for real-time systems. In:Proc. of the LICS. 1990. 414-425.
    [137] Alur R, Courcoubetis C, Dill D. Model-checking in dense real-time. Information and Computation, 1993, 104(1):2-34.
    [138] Bouyer P, Chevalier F, Markey N. On the expressiveness of TPTL and MTL. In:Proc. of the FSTTCS. 2005. 432-443.
    [139] Alur R, Henzinger TA. A really temporal logic. Journal of the ACM (JACM), 1994, 41(1):181-203.
    [140] Larsen KG, Pettersson P, Yi W. UPPAAL in a nutshell. Int'l Journal on Software Tools for Technology Transfer, 1997, 1(1):134-152.
    [141] Bengtsson J, Yi W. Timed automata:Semantics, algorithms and tools. In:Lectures on Concurrency and Petri Nets. 2003. 87-124.
    [142] Havelund K, Larsen KG, Skou A. Formal verification of a power controller using the real-time model checker Uppaal. In:Proc. of the Int'l AMAST Workshop on Aspects of Real-time Systems and Concurrent and Distributed Software. Berlin, Heidelberg:Springer, 1999. 277-298.
    [143] Larsen K G, Mikucionis M, Nielsen B, et al. Testing real-time embedded software using UPPAAL-TRON:An industrial case study. In:Proc. of the 5th ACM Int'l Conf. on Embedded Software. 2005. 299-306.
    [144] Larsen KG, Lorber F, Nielsen B. 20 years of UPPAAL enabled industrial model-based validation and beyond. In:Proc. of the Int'l Symp. on Leveraging Applications of Formal Methods. Cham:Springer, 2018. 212-229.
    [145] Yovine S. Kronos:A verification tool for real-time systems. Int'l Journal on Software Tools for Technology Transfer, 1997, 1(1-2):123-133.
    [146] Bozga M, Daws C, Maler O, et al. Kronos:A model-checking tool for real-time systems. In:Proc. of the Int'l Symp. on Formal Techniques in Real-time and Fault-tolerant Systems. Berlin, Heidelberg:Springer, 1998. 298-302.
    [147] Wang F, Yao LW, Yang YL. Efficient verification of distributed real-time systems with broadcasting behaviors. Real-time Systems, 2011, 47(4):285-318.
    [148] Gupta V, Henzinger TA, Jagadeesan R. Robust timed automata. In:Proc. of the HART. 1997. 331-345.
    [149] Bouyer P, Markey N, Sankur O. Robustness in timed automata. In:Proc. of the RP. 2013. 1-18.
    [150] Katoen JP. The probabilistic model checking landscape. In:Proc. of the 31st Annual ACM/IEEE Symp. on Logic in Computer Science. 2016. 31-45.
    [151] Kemeny JG, Snell JL. Finite Markov Chains. Princeton:D. Van Nostrand, 1960.
    [152] Kulkarni VG. Modeling and Analysis of Stochastic Systems. New York:Chapman& Hall, 1995.
    [153] Bellman R. A Markovian decision process. Journal of Mathematics and Mechanics, 1957, 6(5):679-684.
    [154] Vardi MY. Automatic verification of probabilistic concurrent finite state programs. In:Proc. of the 26th Annual Symp. on Foundations of Computer Science. 1985. 327-338.
    [155] Anderson WJ. Continuous-time Markov Chains:An Applications-oriented Approach. New York:Springer Science& Business Media, 2012.
    [156] Hart S, Sharir M, Pnueli A. Termination of probabilistic concurrent program. ACM Trans. on Programming Languages and Systems (TOPLAS), 1983, 5(3):356-380.
    [157] Vardi MY, Wolper P. Reasoning about infinite computations. Information and Computation, 1994, 115(1):1-37.
    [158] Klein J, Baier C. Experiments with deterministic -w-automata for formulas of linear temporal logic. Theoretical Computer Science, 2006, 363(2):182-195.
    [159] Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5):512-535.
    [160] Aziz A, Singhal V, Balarin F, Brayton RK, Sangiovanni-Vincentelli AL. It usually works:The temporal logic of stochastic systems. In:Proc. of the Int'l Conf. on Computer Aided Verification. 1995. 155-165.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

王淑灵,詹博华,盛欢欢,吴昊,易士程,王令泰,金翔宇,薛白,李静辉,向霜晴,向展,毛碧飞.可信系统性质的分类和形式化研究综述.软件学报,2022,33(7):2367-2410

Copy
Share
Article Metrics
  • Abstract:2669
  • PDF: 6403
  • HTML: 5610
  • Cited by: 0
History
  • Received:September 05,2021
  • Revised:October 14,2021
  • Online: January 28,2022
  • Published: July 06,2022
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2032327Visitors
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