复杂系统规约、分析与验证发展现状与展望

doi:10.3981/j.issn.2097-0781.2023.01.001

前瞻科技 ›› 2023, Vol. 2 ›› Issue (1): 7-22.DOI: 10.3981/j.issn.2097-0781.2023.01.001

复杂系统规约、分析与验证发展现状与展望

詹乃军¹^,²(), 王戟³^,⁴^,^†()

1.中国科学院软件研究所天基综合信息系统重点实验室，北京 100190
2.中国科学院软件研究所计算机科学国家重点实验室，北京 100190
3.国防科技大学计算机学院，长沙 410073
4.国防科技大学高性能计算国家重点实验室，长沙 410073

收稿日期:2022-12-31 修回日期:2023-01-20 出版日期:2023-03-20 发布日期:2023-03-24
通讯作者: ^†
作者简介:詹乃军，中国科学院特聘研究员，博士研究生导师。国家杰出青年科学基金获得者。中国科学院软件研究所计算机科学国家重点实验室执行主任。中国计算机学会形式化方法专业委员会副主任。主要研究领域为计算软件与理论。电子信箱：znj@ios.ac.cn。
王戟，研究员，博士研究生导师。国家杰出青年科学基金获得者。中国计算机学会形式化方法专业委员会主任。主要研究领域为高可信软件。电子信箱：wj@nudt.edu.cn。
基金资助:
国家重点研发计划(2022YFA1005101);国家自然科学基金(62192732);国家自然科学基金(62032024);国家自然科学基金(61732001);中国科学院稳定支持基础研究领域青年团队计划(YSBR-040)

Challenges and Trends for Specification, Analysis, and Verification of Complex Systems

ZHAN Naijun¹^,²(), WANG Ji³^,⁴^,^†()

1. Science & Technology on Integrated Information System Laboratory, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
2. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
3. College of Computer Science and Technology, National University of Defense Technology, Changsha 410073, China
4. State Key Laboratory of High-Performance Computing, National University of Defense Technology, Changsha 410073, China

Received:2022-12-31 Revised:2023-01-20 Online:2023-03-20 Published:2023-03-24
Contact: ^†

摘要/Abstract

摘要：

形式化方法包括计算系统（软硬件和网络）的规约、构造、分析与验证的数学基础、技术和工具。随着安全攸关系统在国民经济和国防等关键领域的应用越来越多，复杂系统可信性问题日益凸显。形式化方法已经成为开发安全可靠的安全攸关系统的关键技术之一，也是解决中国“缺芯少魂”的核心技术之一，同时也是国际学术前沿。文章回顾国内外形式化方法研究现状，分析国内外研究差距，并提出加强中国这方面基础研发的若干建议。

关键词: 形式化方法, 安全攸关系统, 形式规约, 形式分析与验证

Abstract:

Formal methods provide mathematical theories, techniques, and tools for the specification, construction, analysis, and verification of computing systems (including hardware, software, and networks). As safety-critical systems are more widely applied to key fields related to national economics and defense, the trustworthiness problem of complex systems becomes prominent and challenging. Formal methods have become a key technology for developing dependable safety-critical systems and solving China’s problem of deficient microchips and operating systems. They are also the frontiers of international academics. This paper reviews the current status of formal methods, analyzes the gap between China and other countries in this regard, and proposes some suggestions on ways of strengthening the basic research on formal methods in China.

Key words: formal methods, safety-critical systems, formal specification, formal analysis and verification

詹乃军, 王戟. 复杂系统规约、分析与验证发展现状与展望[J]. 前瞻科技, 2023, 2(1): 7-22.

ZHAN Naijun, WANG Ji. Challenges and Trends for Specification, Analysis, and Verification of Complex Systems[J]. Science and Technology Foresight, 2023, 2(1): 7-22.

参考文献 84

[1]	王戟, 詹乃军, 冯新宇, 等. 形式化方法概貌[J]. 软件学报, 2019, 30(1): 33-61.
[2]	Booch G, Rumbaugh J, Jacobson I. The unified modeling language user guide[M]. 2nd ed. Boston: Addison-Wesley Professional, 2005.
[3]	MathWorks. Simulink^® User’s guide[EB/OL]. [2023-02-01]. http://www.mathworks.com/help/pdf_doc/simulink/sl_using.pdf, 2013.
[4]	Modelica Association. Modelica language specification, Version 3.5[EB/OL]. [2023-02-01]. https://specification.modelica.org/master/.
[5]	Ansys SCADE Suite[EB/OL]. [2023-02-01]. https://www.ansys.com/products/embedded-software/ansys-scade-suite.
[6]	Petri C A, Reisig W. Petri net[J]. Scholarpedia, 2008, 3(4), doi: 10.4249/scholarpedia.6477. DOI
[7]	Statecharts H D. A visual formalism for complex systems[J]. Science of Computer Programming, 1987, 8(3): 231-274. DOI URL
[8]	Büchi J R, Landweber L H. Solving sequential conditions by finite-state strategies[J]. Transactions of the American Mathematical Society, 1969, 138(1): 295-311. DOI URL
[9]	The maude system[EB/OL]. (2022-07-11) [2023-02-01]. http://maude.cs.illinois.edu/w/index.php/The_Maude_System#Maude_Documentation.
[10]	Futatsugi K, Goguen J A, Jouannaud J P, et al. Principles of OBJ2[C]// Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. New York: ACM Press, 1985, 52-66.
[11]	Guttag J V, Horning J. LARCH: Languages and tools for formal specification[M]. Berlin, Heidelberg: Springer, 1993.
[12]	Hoare C A R. Communicating sequential processes[M]// Prentice Hall International Series in Computer Science. New York: Prentice Hall, 1985.
[13]	Milner R. A. Calculus of communicating systems[M]. Berlin, Heidelberg: Springer, 1980.
[14]	Bergstra J A, Klop J W. Algebra of communicating processes with abstraction[J]. Theoretical Computer Science, 1985, 37(85): 77-121. DOI URL
[15]	Lamport L. Proving the correctness of multiprocess programs[J]. IEEE Transactions on Software Engineering, 1977, 3(2): 125-143.
[16]	Alpern B, Schneider F. Recongnizing safety and liveness[J]. Distributed Computing, 1987, 2(3): 117-126. DOI URL
[17]	Hoare C A R. An axiomatic basis for computer programming[J]. Communications of the ACM, 1969, 12(10): 576-580. DOI URL
[18]	The Isabelle proof assistant[EB/OL]. [2023-02-01]. https://isabelle.in.tum.de/.
[19]	The Coq proof assistant[EB/OL]. [2023-02-01]. https://coq.inria.fr/.
[20]	Event-B/Rodin[EB/OL]. [2023-02-01]. http://www.event-b.org/.
[21]	Clarkson M B, Schneider F B. Hyperproperties[J]. Journal of Computer Security, 2010, 18(6): 1157-1210. DOI URL
[22]	Jones C B. Systematic software development using VDM[M]. 2nd ed. New York: Prentice Hall, 1990.
[23]	Woodcock J, Davies J. Using Z: Specification, proof and fefinement[M]. New York: Prentice Hall, 1996.
[24]	Benton N. Simple relational correctness proofs for static analyses and program transformations[J]. ACM SIGPLAN Notices, 2004, 39(1): 14-25.
[25]	Miné A, Mauborgne L, Rival X, et al. Taking static analysis to the next level: Proving the absence of run-time errors and data races with astrée[C]// Proceedings of the 8th European Congress on Embedded Real Time Software and Systems (ERTS 2016). 2016: 570-579.
[26]	Czajka L, Kaliszyk C. Hammer for Coq: Automation for dependent type theory[J]. Journal of Automated Reasoning, 2018, 61(1-4): 423-453. DOI
[27]	Paulson L. A mechanised proof of Gödel’s incompleteness theorems using nominal Isabelle[J]. Journal of Automated Reasoning, 2015, 55(1): 1-37. DOI URL
[28]	Awodey S, Pelayo A, Warren M. Voevodsky’s univalence axiom in homotopy type theory[J]. Notices of the American Mathematical Society, 2013, 60(9): 1164-1167. DOI URL
[29]	Klein G, Andronick J, Elphinstone K, et al. Comprehensive formal verification of an OS microkernel[J]. ACM Transaction on Computer Systems, 2014, 32(1): 1-70.
[30]	Stewart G, Beringer L, Cuellar S, et al. Compositional CompCert[J]. ACM SIGPLAN Notices, 2015, 50(1): 275-287.
[31]	Voronkov A. The anatomy of vampire[J]. Journal of Automated Reasoning, 1995, 15(2): 237-265. DOI URL
[32]	Zhan B. AUTO2, a saturation-based heuristic prover for higher-order logic[C]// Blanchette J, Merz S.Proceedings of the 7th International Conference on Interactive Theorem Proving, ITP 2016. Berlin, Heidelberg: Springer, 2016: 441-456.
[33]	Argelich J, Manyà F. Exact Max-SAT solvers for over-constrained problems[J]. Journal of Heuristics, 2006, 12(4): 375-392. DOI URL
[34]	de Moura L, Bjørner N. Z3: An efficient SMT solver[C]// Ramakrishna C R, Rehof J. Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 2008, 337-340.
[35]	Barbosa H, Barrett C, Brain M, et al. cvc5: A versatile and industrial-strength SMT solver[C]// Fisman D, Rosu G.Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. Berlin, Heidelberg: Springer, 2022, 415-442.
[36]	Vardi M Y, Wolper P. An automata-theoretic approach to automatic program verification[C]. LICS, 1986: 322-331.
[37]	Clarke E M, Grumberg O, Peled D. Model checking[M]. Cambridge, MA: MIT Press, 1999.
[38]	Baier C, Katoen J P. Principles of model checking[M]. Cambridge, MA: MIT Press, 2008.
[39]	Cimatti A, Griggio A. Software model checking via IC3[C]// Madhusudan P, Seshia S A.Proceedings of the 24th International Conference on Computer Aided Verification, CAV 2012. Berlin, Heidelberg: Springer, 2012: 277-293.
[40]	Larsen K, Pettersson P, Wang Y. Uppaal in a nutshell[J]. International Journal on Software Tools for Technology Transfer, 1997, 1(1-2): 134-152. DOI URL
[41]	PRISM[EB/OL]. [2023-02-01]. https://www.prismmodelchecker.org.
[42]	Hahn E, Li Y, Schewe S, et al. ISCASMC: A web-based probabilistic model checker[C]// Jones C, Pihlajasaari P, Sun J. Proceedings of the 19th International Symposium on Formal Methods, FM 2014. Berlin, Heidelberg: Springer, 2014: 312-317.
[43]	Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic[C]// Kozen D.Proceedings of the 1st Workshop on Logics of Programs. Berlin, Heidelberg: Springer, 1981: 52-71.
[44]	PVS specification and verification system[EB/OL]. [2023-02-01]. http://pvs.csl.sri.com/.
[45]	Olderog E R, Dierks H. Real-time systems: Formal specification and automatic verification[M]. New York: Cambridge University Press, 2008.
[46]	Gu R, Shao Z, Chen H, et al. CertiKOS: An extensible architecture for building certified concurrent OS kernels[C]// Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation. Berkeley: USENIX Association, 2016: 653-669.
[47]	Xu F, Fu M, Feng X, et al. A practical verification framework for preemptive OS kernels[C]// Chaudhuri S, Farzan A.Proceedings of the 28th International Conference on Computer Aided Verification, CAV 2016. Cham: Springer, 2016: 59-79.
[48]	唐稚松. 时序逻辑程序设计与软件工程(上): 时序逻辑语言[M]. 北京: 科学出版社, 1999.
[49]	唐稚松. 时序逻辑程序设计与软件工程(下): 软件工程方法与工具[M]. 北京: 科学出版社, 2002.
[50]	Zhou C. Weakest environment of communicating processes[C]// Proceedings of the 1982 AFIPS National Computer Conference. Arlington: AFIPS Press, 1982: 679-690.
[51]	Zhou C, Hoare C A R, Ravn A. A calculus of durations[J]. Information Processing Letters, 1991, 40(5): 269-276. DOI URL
[52]	Alur R, Dill D. A theory of timed automata[J]. Theoretical Computer Science, 1994, 126(2): 183-235. DOI URL
[53]	Hennessy M, Li W, Plotkin G. A first attempt at translating CSP into CCS[C]// Yang Y, Ma M. Proceedings of the 2nd International Conference on Distributed Computing Systems. Paris: DBLP, 1981: 105-115.
[54]	Hoare C A R, He J. Unifying theories of programm- ing[M]. New York: Prentice Hall, 1988.
[55]	Hennessy M, Lin H. Proof systems for message-passing process algebras[C]// Best E. Proceedings of the 4th International Conference on Concurency Theory, CONCUR 1993. Berlin, Heidelberg: Springer, 1993: 202-216.
[56]	Zhan N, Wang S, Zhao H. Formal verification of simulink/stateflow diagrams[M]. Berlin, Heidelberg: Springer, 2017.
[57]	Liu J, Lü L, Quan Z, et al. A calculus for hybrid CSP[C]// Ued, K. Proceedings of the 8th Asian Symposoium on Programming Languages and Systems, APLAS 2010. Berlin, Heidelberg: Springer, 2010: 1-15.
[58]	Wang S, Zhan N, Zou L. An improved HHL prover: An interactive theorem prover for hybrid systems[C]// Butler M, Conchon S, Zaïdi F. Proceedings of the 17th International Conference on Formal Methods and Software Engineering, ICFEM 2015. Berlin, Heidelberg: Springer, 2015: 282-399.
[59]	Liu J, Zhan N, Zhao H. Computing semi-algebraic invariants for polynomial dynamical systems[C]// Proceedings of the Ninth ACM International Conference on Embedded Software. Piscataway: IEEE Press, 2011: 97-106.
[60]	Wang Q, Chen M, Xue B, et al. Encoding inductive invariants as barrier certificates synthesis via difference-of-convex programming[J]. Information and Computation, 289, doi: 10.1016/j.ic.2022.104965. DOI
[61]	Zou L, Lü L, Wang S, et al. Verifying Chinese train control system under a combined scenario by theorem proving[C]//Cohen E, Rybalchenko A.Proceedings of the International Conference on Verified Software:Theories, Tools, Experiments. Berlin, Heidelberg: Springer, 2014: 262-280.
[62]	Zhao H, Yang M, Zhan N, et al. Formal verification of a descent guidance control program of a lunar lander[C]// Jones C, Pihlajasaari, P, Sun J. Proceedings of the Formal Methods, 19th International Symposium, FM 2014. Berlin, Heidelberg: Springer, 2014: 733-748.
[63]	Bu L, Li Y, Wang L, et al. BACH: Bounded reachability checker for linear hybrid automata[C]// Proceedings of the 2008 Formal Methods in Computer-Aided Design. Piscataway: IEEE Press, 2008: 1-4.
[64]	Bu L, Xie Z, Lyu L, et al. BRICK: Path enumeration based bounded reachability checking of C program[C]// Fisman D, Rosu G. Proceedings of the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. Berlin, Heidelberg: Springer, 2022: 408-412.
[65]	Yi X, Chen L, Mao X, et al. Efficient automated repair of high floating-point errors in numerical libraries[J]. Proceedings of the ACM on Programming Languages, 2019, 3: 1-29.
[66]	Chen L, Miné A, Wang J, et al. An abstract domain to discover interval linear equalities[C]// Barthe G, Hermenegildo M. Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010.Berlin, Heidelberg: Springer, 2010: 112-128.
[67]	Chen L, Miné A, Wang J, et al. Interval polyhedra: An abstract domain to infer interval linear relationships[C]// Palsberg J, Su Z. Proceedings of the 16th International Symposium on Static Analysis, SAS 2009. Berlin, Heidelberg: Springer, 2009: 309-325.
[68]	Feng X. Local rely-guarantee reasoning[C]. POPL. New York: ACM Press, 2009: 315-327.
[69]	Liang L, Feng X, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations[J]. ACM SIGPLAN Notices, 2012, 47(1): 455-468. DOI URL
[70]	Xu F, Fu M, Feng X, et al. A practical verification framework for preemptive OS kernels[C]// Chaudhuri S, Farzan A. Proceedings of the 28th International Conference on Computer Aided Verification, CAV 2016. Berlin, Heidelberg: Springer, 2016: 59-79.
[71]	Zhao Y, Sanán D. Rely-guarantee reasoning about concurrent memory management in Zephyr RTOS[C]// Dillig I, Tasiran S. Proceedings of the 31st International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2019: 515-533.
[72]	Sanán D, Zhao Y, Lin S, et al. CSim2: Compositional top-down verification of concurrent systems using rely-guarantee[J]. ACM Transactions on Programming Languages and Systems, 2021, 43(1): 1-46.
[73]	Cao Q, Beringer L, Gruetter S, et al. VST-Floyd: A separation logic tool to verify correctness of C programs[J]. Journal of Automated Reasoning, 2018, 61(1-4): 367-422. DOI
[74]	Wang Y, Zhang L, Shao S, et al. Verified compilation of C programs with a nominal memory model[J]. Proceedings of the ACM on Programming Languages, 2022, 6: 1-31.
[75]	He F, Yu Q, Cai L. Efficient summary reuse for software regression verification[J]. IEEE Transactions on Software Engineering, 2022, 48(4): 1417-1431. DOI URL
[76]	Chen J, He F. Leveraging control flow knowledge in SMT solving of program verification[J]. ACM Transactions on Software Engineering and Methodology, 2021, 30(4): 1-26.
[77]	Cai S, Zhang X, Fleury M, et al. Better decision heuristics in CDCL through local search and target phases[J]. Journal of Artificial Intelligence Research, 2022, 74: 1515-1563. DOI URL
[78]	Wang Y, Cai S, Chen J, et al. SCCWalk: An efficient local search algorithm and its improvements for maximum weight clique problem[J]. Artificial Intelligence, 2020, 280, doi: 10.1016/j.artint.2019.103230. DOI
[79]	Li H, Xia B, Zhang H, et al. Choosing the variable ordering for cylindrical algebraic decomposition via exploiting chordal structure[C]// ISSAC. 2021: 281-288.
[80]	Gan T, Xia B, Xue B, et al. Nonlinear craig interpolant generation[C]// Lahir, S, Wang C. Proceedings of the 32nd International Conference on Computer Aided Verification, CAV 2020. Berlin, Heidelberg: Springer, 2020: 415-438.
[81]	Katoen J P, Song L, Zhang L. Probably safe or live[C]// Proceedings of the Joint Meeting of the Twenty-third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). New York:ACM Press, 2014: 1-10.
[82]	Li M, Turrini A, Hahn E, et al. Probabilistic preference planning problem for markov decision processes[J]. IEEE Transactions on Software Engineering, 2022, 48(5): 1545-1559. DOI URL
[83]	Wang J, Sun Y, Fu H, et al. Quantitative analysis of assertion violations in probabilistic programs[C]// Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. New York: ACM Press, 2021: 1171-1186.
[84]	Huang M, Fu H, Chatterjee K, et al. Modular verification for almost-sure termination of probabilistic programs[J]. Proceedings of the ACM on Programming Languages, 2019, 3: 1-29.

复杂系统规约、分析与验证发展现状与展望

Challenges and Trends for Specification, Analysis, and Verification of Complex Systems

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献 84

相关文章 3

编辑推荐

Metrics

访问统计

友情链接

联系我们

官方微信公众号

[1]	丁浩然, 王肇国, 付明, 陈海波. 形式化方法与系统软件：实践与发展建议[J]. 前瞻科技, 2023, 2(1): 33-45.
[2]	吕继东, 卢万里, 唐涛, 罗正伟. 列车运行控制系统的形式化研究进展与趋势[J]. 前瞻科技, 2023, 2(1): 106-117.
[3]	陈厅, 吴国政, 刘哲, 蒲戈光, 赵瑞珍, 刘克. NSFC形式化方法领域基金项目申请资助情况分析[J]. 前瞻科技, 2023, 2(1): 132-140.