前瞻科技

关键词	项目名称匹配	项目关键词匹配	去重后	总项目
形式化方法	121	27	454	71	522	90	1599	377
程序验证	43	11	124	37	140	42
模型检测	218	59	500	123	534	131
约束求解	51	15	123	38	138	43
定理证明	38	11	188	42	188	42
程序合成	2	1	21	6	21	6
程序综合	2	1	8	3	8	3
可满足性	79	20	147	37	155	41
安全攸关系统	11	2	11	3	17	4
并发系统	28	9	27	9	40	11
概率程序设计	0	0	1	1	1	1

关键词	项目名称匹配	项目关键词匹配	去重后	总项目
形式化方法	121	27	454	71	522	90	1599	377
程序验证	43	11	124	37	140	42
模型检测	218	59	500	123	534	131
约束求解	51	15	123	38	138	43
定理证明	38	11	188	42	188	42
程序合成	2	1	21	6	21	6
程序综合	2	1	8	3	8	3
可满足性	79	20	147	37	155	41
安全攸关系统	11	2	11	3	17	4
并发系统	28	9	27	9	40	11
概率程序设计	0	0	1	1	1	1

项目类型	申请数量/个	资助数量/个	资助率/%	资助经费/万元
创新研究群体项目	5	2	40.0	2540.00
重大研究计划项目	52	10	19.2	2791.00
重大项目	3	2	66.7	1475.00
国家杰出青年科学基金项目	36	4	11.1	520.00
优秀青年科学基金项目	45	3	6.7	420.00
重点项目	23	10	43.5	2203.00
联合基金项目	24	3	12.5	362.00
面上项目	708	157	22.2	6868.50
青年科学基金项目	498	124	24.9	2733.60
地区科学基金项目	131	25	19.1	916.00
数学天元基金项目	8	3	37.5	8.50
合作类项目	48	17	35.4	818.53
其他项目	18	14	77.8	422.00

项目类型	申请数量/个	资助数量/个	资助率/%	资助经费/万元
创新研究群体项目	5	2	40.0	2540.00
重大研究计划项目	52	10	19.2	2791.00
重大项目	3	2	66.7	1475.00
国家杰出青年科学基金项目	36	4	11.1	520.00
优秀青年科学基金项目	45	3	6.7	420.00
重点项目	23	10	43.5	2203.00
联合基金项目	24	3	12.5	362.00
面上项目	708	157	22.2	6868.50
青年科学基金项目	498	124	24.9	2733.60
地区科学基金项目	131	25	19.1	916.00
数学天元基金项目	8	3	37.5	8.50
合作类项目	48	17	35.4	818.53
其他项目	18	14	77.8	422.00

申请代码	资助数量/个	占比/%
F0201	71	45.2
F0203	27	17.2
F0209	7	4.5
F0204	6	3.8
A0602	5	3.2

申请代码	资助数量/个	占比/%
F0201	71	45.2
F0203	27	17.2
F0209	7	4.5
F0204	6	3.8
A0602	5	3.2

依托单位	资助数量/个	占比/%
中国科学院软件研究所	19	12.1
清华大学	16	10.2
华东师范大学	8	5.1
西安电子科技大学	7	4.5
中山大学	7	4.5

依托单位	资助数量/个	占比/%
中国科学院软件研究所	19	12.1
清华大学	16	10.2
华东师范大学	8	5.1
西安电子科技大学	7	4.5
中山大学	7	4.5

申请代码	资助数量/个	占比/%
F0201	48	38.7
F0203	26	21.0
F0209	8	6.5
F06	5	4.0
F0601	5	4.0

申请代码	资助数量/个	占比/%
F0201	48	38.7
F0203	26	21.0
F0209	8	6.5
F06	5	4.0
F0601	5	4.0

依托单位	资助数量/个	占比/%
中国科学院软件研究所	13	10.5
华东师范大学	8	6.5
西安电子科技大学	7	5.7
上海交通大学	5	4.0
南京大学	4	3.2

依托单位	资助数量/个	占比/%
中国科学院软件研究所	13	10.5
华东师范大学	8	6.5
西安电子科技大学	7	5.7
上海交通大学	5	4.0
南京大学	4	3.2

申请代码	资助数量/个	占比/%
F0201	13	52
F0203	7	28
F0211	1	4
F06	1	4
F0601	1	4

申请代码	资助数量/个	占比/%
F0201	13	52
F0203	7	28
F0211	1	4
F06	1	4
F0601	1	4

重大研究计划项目名称	子类型	申请数量/个	资助数量/个	资助率/%	资助金额/万元
可信软件基础研究	集成项目	2	1	50.0	2000
重点支持项目	10	3	30.0	580
培育项目	27	2	7.4	100
小计	39	6	15.4	2680
网络与信息安全	面上项目	10	3	30.0	81
半导体集成化芯片系统基础研究	面上项目	2	1	50.0	30
以网络为基础的科学活动环境研究	面上项目	1	0	0	0
总计	52	10	19.2	2791

重大研究计划项目名称	子类型	申请数量/个	资助数量/个	资助率/%	资助金额/万元
可信软件基础研究	集成项目	2	1	50.0	2000
重点支持项目	10	3	30.0	580
培育项目	27	2	7.4	100
小计	39	6	15.4	2680
网络与信息安全	面上项目	10	3	30.0	81
半导体集成化芯片系统基础研究	面上项目	2	1	50.0	30
以网络为基础的科学活动环境研究	面上项目	1	0	0	0
总计	52	10	19.2	2791

NSFC形式化方法领域基金项目申请资助情况分析

PDF下载

陈厅 ¹^,² , 吴国政 ¹^,^† , 刘哲 ³ , 蒲戈光 ⁴ , 赵瑞珍 ¹ , 刘克 ¹

前瞻科技 | 综述与述评 2023,2(1): 132-140

收起

前瞻科技 | 综述与述评 2023, 2(1): 132-140

NSFC形式化方法领域基金项目申请资助情况分析

全屏

陈厅¹^,², 吴国政¹^,^†, 刘哲³, 蒲戈光⁴, 赵瑞珍¹, 刘克¹

作者信息

1.国家自然科学基金委员会信息科学部，北京 100083

2.电子科技大学计算机科学与工程学院（网络空间安全学院），成都 611731

3.南京航空航天大学计算机科学与技术学院，南京 210016

4.华东师范大学软件工程学院，上海 200062

陈厅，教授，国家自然科学基金委员会信息科学部二处流动项目主任。主要研究方向为网络安全。电子信箱：chenting@nsfc.gov.cn。

吴国政，研究员，国家自然科学基金委员会信息科学部二处处长。主要研究方向为人工智能、信息安全。电子信箱：wugz@nsfc.gov.cn。

通信作者:

^†

Fund Applications and Fundings in Formal Methods Under National Natural Science Foundation of China

Ting CHEN¹^,², Guozheng WU¹^,^†, Zhe LIU³, Geguang PU⁴, Ruizhen ZHAO¹, Ke LIU¹

Affiliations

1. Department of Information Science, National Natural Science Foundation of China, Beijing 100083, China

2. School of Computer Science and Engineering (School of Cybersecurity), University of Electronic Science and Technology of China, Chengdu 611731, China

3. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China

4. Software Engineering Institute, East China Normal University, Shanghai 200062, China

出版时间: 2023-03-20 doi: 10.3981/j.issn.2097-0781.2023.01.010

文章导航

摘要

收起

针对历年来国家自然科学基金委员会（NSFC）在形式化方法领域各类型基金申请和资助情况进行统计和分析，并对涉及的重大研究计划和重大项目予以重点阐述和分析，最后对NSFC“十四五”发展规划中涉及形式化方法的部分予以解读。

关键词

国家自然科学基金委员会 / 形式化方法 / 资助 / “十四五”规划

Abstract

收起

This paper statistically analyzes the fund applications and funding in formal methods under the National Natural Science Foundation of China (NSFC). Then, it describes and analyzes the major research plan and major projects of NSFC related to formal methods. After that, the work expounds on the content related to formal methods in the 14th Five-Year Plan of NSFC.

Key words

NSFC / formal methods / funding / 14th Five-Year Plan

引用本文

陈厅, 吴国政, 刘哲, 蒲戈光, 赵瑞珍, 刘克. NSFC形式化方法领域基金项目申请资助情况分析. 前瞻科技, 2023 , 2 (1) : 132 -140 . DOI: 10.3981/j.issn.2097-0781.2023.01.010

Ting CHEN, Guozheng WU, Zhe LIU, Geguang PU, Ruizhen ZHAO, Ke LIU. Fund Applications and Fundings in Formal Methods Under National Natural Science Foundation of China[J]. Science and Technology Foresight, 2023 , 2 (1) : 132 -140 . DOI: 10.3981/j.issn.2097-0781.2023.01.010

正文

收起

形式化方法（Formal Methods）在逻辑科学中是指分析、研究思维形式结构的方法。它把各种具有不同内容的思维形式（主要是命题和推理）加以比较，找出其中各个部分相互联结的方式^[1]。用于开发计算机系统的形式化方法是基于数学的描述系统性质的技术，这样的形式化方法提供了一个框架，可以在框架中以系统的而不是特别的方式刻划、开发和验证系统^[1]。形式化方法大量用于计算机系统的设计、开发和验证中，利用数学方法提高计算机系统的正确性、可靠性、鲁棒性和安全性。国内科研人员针对形式化方法开展了深入且富有成效的研究，取得了一系列的研究成果，国家自然科学基金委员会（NSFC）也对该领域进行了长期资助，不少科研人员通过NSFC基金项目的支持成长为该领域的专家。

文章针对该领域NSFC基金申请与资助情况进行统计分析，统计分析的项目包括：各类型NSFC项目在该领域的申请数量、资助数量、资助率、资助经费、申请数量和资助数量随时间变化情况、不同二级代码下项目的资助数量、各依托单位获资助的项目数量等。由于重大研究计划和重大项目体现了NSFC的重点布局情况，文章又对形式化方法所涉及的4个重大研究计划和2个重大项目进行了详细分析。最后，对“十四五”时期NSFC在形式化方法领域的布局情况予以剖析。

文章面向形式化方法领域的科研人员，希望统计分析结果能够为科研人员提供有价值的信息，同时也希望对“十四五”时期NSFC优先资助领域的剖析结论能够为科研人员未来科研方向及NSFC基金申请提供一定的参考。

1 基金申请与资助情况

收起

形式化方法的基础理论和关键技术不仅涉及计算机科学，还涉及数理逻辑;形式化方法不仅广泛应用于计算机领域，而且在控制、机械设计、通信、医疗等领域也有大量的应用。因此，形式化方法领域的基金项目申请主要集中在信息科学部，但也有相当数量的项目从数学物理科学部、医学科学部等申报。为了尽可能全面地统计形式化方法领域的项目申请和资助情况，文章采用关键词搜索的方式对NSFC所有项目类型的项目名称和项目关键词进行模糊匹配，检索到1988—2022年有1599个项目申请，其中377个项目获得资助，资助项目类型涵盖创新研究群体项目、重大研究计划项目、重大项目、国家杰出青年科学基金项目等16类项目，总体资助率为23.6%，资助总经费超过2.2亿元人民币。

表1给出了NSFC在形式化方法领域项目申请和资助的数量。其中，“关键词”列给出了与形式化方法紧密相关的11个关键词，文章根据这11个关键词在NSFC数据中搜索出数据并加以分析;“项目名称匹配”列表示用第一列的关键词与NSFC的数据库中申请或资助项目的项目名称进行匹配出来的项目数量;“项目关键词匹配”列表示用第一列的关键词与NSFC的数据库中申请或资助项目的项目关键词进行匹配出来的项目数量;考虑用“项目名称”和“项目关键词”匹配出的项目可能有重复，“去重后”列则代表去掉重复后的项目数量;“总项目”列代表NSFC在形式化方法领域项目申请和资助的总数。

由于重大研究计划项目和重大项目体现了NSFC在形式化方法领域的重点布局，这两类项目的统计分析放在本文第2节，本节只对其他类型的项目进行统计和分析。表2列出了NSFC在形式化方法领域各类型项目的申请数量、资助数量、资助率和资助经费。

1）创新研究群体项目

3位申请人共申请了5次创新研究群体项目，都归口于信息科学部。2位申请人的2个项目获得资助，资助率为40%，资助总经费为2540万元人民币。最近的一个创新研究群体项目已于2016年结题，近7年无新增创新研究群体项目，可能原因是形式化方法领域研究周期较长、发表论文竞争非常激烈、出成果较为困难，因此需要更多的时间形成创新群体。

2）国家杰出青年科学基金项目

18位申请人共申请了36次国家杰出青年科学基金项目，有1个项目归口管理学部，其余35个项目都归口信息科学部。4位申请人的4个项目获得资助，均归口信息科学部，资助率为11.1%，资助总经费为520万元。最近的一个国家杰出青年科学基金项目已于2011年结题，超过10年无新增国家杰出青年科学基金，可能原因是形式化方法领域发表论文竞争非常激烈、出成果较为困难，因此在和其他领域同年龄段科研人员的横向对比中不占优势。

3）优秀青年科学基金项目

30位申请人共申请了45次优秀青年科学基金项目，所有项目均归口信息科学部。仅3位申请人的3个项目获得资助，资助总经费为420万元人民币，资助率仅为6.7%，明显低于其他方向的优秀青年科学基金项目的资助率，这可能说明在38岁以下年龄段，形式化方法领域的青年学者对比其他领域的青年学者并无优势。

4）重点项目

21位申请人共申请了23次重点项目，其中1个项目归口数学物理科学部，其余22个项目均归口信息科学部。共9位申请人的10个项目获得了资助，均归口信息科学部，资助总经费为2203万元人民币，资助率高达43.5%，显著高于其他研究方向重点项目的资助率，这可能说明形式化方法领域的重点项目申请人对NSFC重点项目指南的理解更深刻，申请书的质量也更高。4个资助项目（占比40%）尚未结题，说明NSFC近5年在形式化方法领域有明确布局，同时该领域学者在指南指定的方向取得了显著的成果。

5）联合基金项目

21位申请人共申请了24次联合基金项目，其中1个项目归口数学物理科学部，其余23个项目均归口信息科学部。共3位申请人的3个项目获得了资助，均归口信息科学部，资助总经费为362万元人民币，资助率仅为12.5%，显著低于其他研究方向的联合基金资助率，这可能说明形式化方法领域的申请人在响应行业和地方需求方面需要进一步加强。

6）面上项目

403位申请人共申请了708次面上项目，其中36个项目归口数学物理科学部，2个项目归口生命科学部，2个项目归口地球科学部，11个项目归口工程与材料科学部，6个项目归口管理科学部，4个项目归口医学科学部，其余647个项目归口信息科学部。共127位申请人的157个项目获得资助，资助总经费为6868.5万元人民币，资助率为22.2%。157个资助项目分布在33个代码，其中12个项目归口数学物理科学部，1个项目归口地球科学部，1个项目归口工程与材料科学部，2个项目归口管理科学部，1个项目归口医学科学部，其余140个项目归口信息科学部。表3列出了面上项目资助数量排名前5的代码，排名第1的代码（计算机科学的基础理论）项目数占比45.2%，排名前5的代码项目数量共占73.9%。

157个资助项目来自于59家依托单位，表4列出了获资助项目数排名前5的依托单位，排名第1的依托单位获资助项目数占比12.1%，排名前5的依托单位获资助项目数共占36.4%。

图1展示了面上项目资助数量随时间变化情况。从1988年资助的第1个面上项目开始逐渐增长到2011年的11个项目后缓慢滑落到每年10个以内。

7）青年科学基金项目

321位申请人共申请了498次青年科学基金项目，19个项目归口数学物理科学部，1个项目归口地球科学部，14个项目归口工程与材料科学部，6个项目归口管理科学部，8个项目归口医学科学部，其余450个项目归口信息科学部。124位申请人的124个项目获得资助，资助总经费为2733.6万元人民币，资助率为24.9%。124个资助项目分布在23个代码，其中，2个项目归口数学物理科学部，2个项目归口工程与材料科学部，2个项目归口管理科学部，1个项目归口医学科学部，其余117个项目归口信息科学部。表5列出了资助项目数量排名前5的代码，排名第1的代码项目数占比38.7%，排名前5的代码项目数量占74.2%。

124个资助项目来自67家依托单位，表6列出了获资助项目数量排名前5的依托单位，排名第1的依托单位获资助项目数占比10.5%，排名前5的依托单位获资助项目数共占29.9%。

图2展示了青年科学基金项目资助数量随时间变化情况。从1989年资助第1个项目开始，增长到2011年的12个项目，随后逐渐回落到每年10个项目以内。

8）地区科学基金项目

56位申请人共申请了131次地区科学基金项目，其中5个项目归口数学物理科学部，5个项目归口工程与材料科学部，4个项目归口管理科学部，1个项目归口医学科学部，其余116个项目归口信息科学部。共20位申请人的25个项目获得资助，资助总经费为916万元人民币，资助率为19.1%。25个资助项目分布在6个代码，其中1个项目归口数学物理科学部，其余24个项目归口信息科学部。表7列出了资助项目数量排名前5的代码，排名第1的代码项目数量占比52%，排名前5的代码项目数量占92%。

9）数学天元基金项目

5位申请人共申请了8次数学天元基金项目，均归口数学物理科学部，共3位申请人的3个项目获得资助，资助总经费为8.5万元人民币，资助率为37.5%。数学天元基金是为凝聚数学家集体智慧，探索符合数学特点和发展规律的资助方式，推动建设数学强国而设立的专项科学基金^[2]。所以，形式化方法领域具有显著的学科交叉特征，其根基在于数理逻辑。最近的一个数学天元基金项目已于2015年结题，近7年无新增资助项目，这可能说明形式化方法领域的数理基础仍需要进一步的挖掘和探索。

10）合作类项目

合作类项目包括NSFC的国际（地区）合作交流项目和国际（地区）合作研究项目。37位申请人共申请了48次合作项目，1个项目归口生命科学部，3个项目归口医学科学部，其余44个项目均归口信息科学部。16位申请人的17个项目获得资助，资助率为35.4%，资助总经费为818.53万元人民币。17个资助项目分布在13个代码，其中3个项目归口医学科学部，其余14个项目归口信息科学部。

11）其他项目

其他项目包括NSFC的应急管理项目、专项项目和专项基金项目。16位申请人共申请了18个其他项目，其中1个项目归口管理科学部，其余17个项目归口信息科学部。12位申请人的14个项目获得资助，资助率为77.8%，资助总经费为422万元人民币。14个资助项目分布在7个代码，均归属于信息科学部。

2 重大研究计划项目和重大项目申请与资助情况

收起

2.1 重大研究计划项目

重大研究计划项目的目标是围绕国际重大战略需求和重大科学前沿，加强顶层设计，凝练科学目标，凝聚优势力量，形成具有相对统一目标或方向的项目集群，促进学科交叉与融合，培养创新人才和团队，提升中国基础研究的原始创新能力，为国民经济、社会发展和国家安全提供科学支撑^[2]。表8列出了NSFC在形式化方法领域重大研究计划项目申请与资助情况，共涉及4个重大研究计划，共有52个项目申请，10个项目获得资助，资助率为19.2%，资助总金额为2791万元人民币。

1）可信软件基础研究

“可信软件基础研究”重大研究计划项目以国家关键应用领域中软件可信性问题为主攻目标，分析、研究和解决相关科学问题，在嵌入式软件和基于网络的大型应用软件中开展示范应用，为改善国家重大工程中的软件可信性提供科学支撑^[3]。

“可信软件基础研究”重大研究计划项目从2008年开始启动，一共持续了10年，针对“软件可信性度量与建模”“可信软件的构造与验证”“可信软件的演化与控制”和“可信环境的构造与评估”4个方面的基本科学问题和关键技术开展了深入研究^[3]。“可信软件基础研究”重大研究计划项目在形式化领域支持项目数量占所有重大研究计划项目在形式化领域支持项目数量的60%，其在形式化领域资助金额占所有重大研究计划项目在形式化领域资助金额的96%，体现出形式化方法是保障软件可信性的支撑技术之一。

“可信软件基础研究”重大研究计划项目包含集成项目、重点支持项目和培育项目3种类型。与形式化方法领域相关的集成项目申请2个，1个项目获得资助，资助率为50%，资助金额为2000万元人民币。与形式化方法领域相关的重点支持项目申请10个，3个项目获得资助，资助率为30%，资助总经费为580万元人民币。与形式化方法领域相关的培育项目申请项目27个，2个项目获得资助，资助率仅为7.4%，资助总经费为100万元人民币。

总体来看，“可信软件基础研究”重大研究计划项目所取得的创新性成果和实质性贡献主要体现在以下几个方面。

（1）基础理论研究实现跨越式发展。10年中，中国在可信软件基础研究领域取得了一批在国际上有重要影响的科学研究成果，对若干重要的基础科学问题，在国际重要学术会议和刊物发表了一系列具有原始创新思想的论文，掌握和突破一批关键技术，取得一批有影响力的专利，解决了中国重大应用中的关键技术难题，引领国际可信软件学术发展，在国际可信软件基础研究方面拥有一席之地。特别是，中国学者率先通过元级思想统一整合可信性各侧面，提出了可信性元级驾驭理论，并在网构软件的可信性需求、构造、演化等方面形成了系统化成果。

（2）关键技术平台实现创新性突破。无论在单项技术或工具还是在整体平台方面，中国学者都有一批成果在指标上处于国际领跑或并跑位置。例如，在2017软件验证国际大赛中，中国参赛工具在并发程序组取得了第1名;中国学者将数据驱动技术和传统程序分析相结合，在软件缺陷修复基准测试方面将之前不足40%的正确率一次性提升到了接近80%。针对国外引进的可信软件工具不适应或不能满足中国工程实践的问题，重大研究计划集成项目面向航天可信软件领域开发了可信软件工具链和平台，对中国保持航天科技在国际领先的位置发挥了重要作用。

（3）重大示范应用有力支撑国家战略。该重大研究计划项目支持了一批国家关键领域的示范应用，取得了突出的应用成效，某些方面实现赶超，部分领域形成了国际领先的应用成果。一是在若干领域的规模化应用和效益处于国际先进水平，实现了从实验室向实际应用跨越;二是建立了面向领域可实际应用的软件可信性构造与验证方法和工具环境，实现了从实验性工具向集成实用化平台跨越;三是提出了可信软件监控与演化的一体设计体系，实现了从静态补丁式可信性演化向模型驱动监控体系结构的跨越。支撑国家重大战略需求的应用领域包括战略性新兴产业（车联网、智能交通）、航天工程（月球探测工程、嫦娥卫星）、航空工程、电子商务、电子政务、电信系统、国防军事、核电系统、国家网络空间安全等。

2）网络与信息安全

“网络与信息安全”重大研究计划项目宗旨在于：研究信息网络与安全的科学理论与关键技术，解决对国民经济发展和国防建设具有重大意义的网络与信息安全领域所涉及的重大科学问题和突破关键基础技术;以网络与信息安全的构造和运行过程中所涉及的新理论、新体系、新结构、新方法和新技术为突破口，力图实现在科学理论和技术上的源头创新，以提高中国在网络与信息安全研究领域的整体创新能力和国际竞争力，形成中国自主的知识产权^[4]。

“网络与信息安全”重大研究计划项目启动于2001年，与形式化方法领域相关的项目申请10个，其中3个项目获得资助，资助率为30%，资助总经费为81万元人民币，这3个获资助项目均是关于网络协议的形式化分析，说明形式化方法在网络安全领域也有重要应用。

3）半导体集成化芯片系统基础研究

“半导体集成化芯片系统基础研究”重大研究计划项目的宗旨在于：以超过当前国际微电子生产水平2~3代的芯片系统需要解决的重要科学问题为研究对象，开展广泛、深入的基础研究，为中国2005—2010年及以后的微电子科技与集成电路产业发展提供解决关键问题的科学方法，从而促进中国电子信息工业高速、持续地发展。该重大研究计划项目反映了微电子领域在21世纪最现实、最迫切的发展方向，即由集成电路向集成系统方向的转变^[5]。

“半导体集成化芯片系统基础研究”重大研究计划项目启动于2003年，与形式化方法领域相关的项目申请2个，其中1个项目获得资助，资助率为50%，资助总经费为30万元人民币，受资助项目关于芯片系统的验证，说明形式化方法在集成电路领域也发挥着重要作用。

4）以网络为基础的科学活动环境研究

“以网络为基础的科学活动环境研究”重大研究计划项目定位在网络计算环境的基础科学理论、综合试验平台、典型应用示范3个层次中的基本科学问题和关键技术研究，同时重点建立高能物理、大气和生物信息等网络计算环境实验应用系统。以网络计算环境中所涉及的新理论、新结构、新方法和新技术为突破口，力图实现科学理论和实验技术的原始创新。通过计划的执行，形成了一支高水平的科学研究和技术攻关队伍;对若干重要的基础科学问题，取得了一批具有原创性的科学研究成果^[6]。

“以网络为基础的科学活动环境研究”重大研究计划项目启动于2004年，与形式化方法领域相关的项目申请1项，但未获资助，该申请项目拟研究网格环境下的软件测试模型。

2.2 重大项目

重大项目面向科学前沿和国家经济、社会、科技发展及国家安全的重大需求中的重大科学问题，超前部署，开展多学科交叉研究和综合性研究，充分发挥支撑与引领作用，提升中国基础研究源头创新能力^[2]。

3位申请人共申请了3次与形式化方法相关的重大项目，2位申请人的2个项目获得资助，资助率为66.7%，资助总经费为1475万元人民币。获资助的1个重大项目为“嵌入式软件智能合成基础理论与方法”，另1个获资助的项目为上述项目的课题，故资助经费不重复计算。该资助项目针对嵌入式软件开发中的多维需求特征抽象表示、软件资产的理解和综合、模型间语义一致性保持等科学问题，提出基于软件知识产权（Intellectual Property, IP）的嵌入式软件智能合成理论与方法，构建从软件需求规约到代码实现的嵌入式软件智能合成平台，大幅提高嵌入式软件开发效率和质量，实现嵌入式软件开发模式从人工编写到智能合成的跨越^[7]。该重大项目于2022年开始启动，拟于2026年结题。

3 NSFC “十四五”发展规划解读

收起

NSFC发布了“十四五”发展规划，列出了115个优先发展领域^[7]。形式化方法虽然没有成为单独的一个优先发展领域，但其中4个优先发展领域与形式化方法有直接关联，第3个和第58个优先发展领域是形式化方法的基础，第55个优先发展领域是形式化方法的保障，第51个优先发展领域是形式化方法的应用。

第3个优先发展领域“问题驱动的应用数学前沿理论与方法”提到“信息技术中的数据隐私保护与安全”^[8]，数学是信息技术的基础支撑之一，形式化方法的研究尤其不能脱离坚实的数学基础。“数据隐私与安全”所涉及的密码学理论、密码算法、数据传输协议、数据分析算法等都需要形式化方法对其功能、性能和安全性予以验证。

第58个优先发展领域“安全科学人工智能基础理论”提到“发展通用人工智能算法，支持安全可信人工智能模型验证”^[8]。文章认为，形式化方法可以用到人工智能算法与模型的验证分析。

第55个优先发展领域“新型网络及网络安全”整个领域都与形式化方法紧密相关。例如，新型网络模型的验证、网络协议分析、量子算法和协议的形式化分析、软件安全性分析与漏洞发掘、区块链共识协议分析与验证、未来网络底层框架设计分析等。

第51个优先发展领域“宽禁带半导体”提到“高性能器件制备工艺、模型和可靠性评测方法等”，第53个优先发展领域“多功能与高效能集成电路”提到“敏捷设计与智能化设计等新工具”^[8]。文章认为，半导体行业是形式化方法的一个重要应用场景，可用于元器件模型和设计的分析和验证。

结合NSFC“十四五”发展规划，希望形式化方法领域的学者更加积极地探索本领域的基础理论、核心技术和未来热点方向，进一步推动本领域的快速发展。在此基础上，形成软件领域的新方法和技术，以期带动科研新范式的兴起。

4 结束语

收起

本文统计和分析了NSFC在形式化方法领域的申请和资助情况;对NSFC“十四五”发展规划中与形式化分析领域相关的优先发展领域进行了解读和剖析。为促进学科发展，NSFC重点支持形式化方法领域从事基础研究的科学技术人员在已有较好基础的研究方向或学科生长点开展深入、系统的创新性研究，促进该领域取得突破。同时，NSFC鼓励形式化方法领域科研人员选择有意义、有创新、合理可行的项目开展原创性、基础性、前瞻性和交叉性研究，继续支持该领域的科研人员与生命科学、医学、数学、地学、管理科学、经济学及社会科学等领域的科研人员开展合作研究，共同探索学科交叉领域的新理论、新方法和新技术，促进形式化方法和其他相关学科的共同发展;鼓励和支持形式化方法领域的科研人员密切关注国家重大战略需求并开展基础性、前瞻性研究，满足国家安全和增进人民福祉的需要。

参考文献

收起

文献

收起

参考文献引证文献

排序方式：

[1]

百度百科. 形式化方法[EB/OL]. (2021-12-08)[2022-10-09]. https://baike.baidu.com/item/形式化方法/4298196.

[2]

国家自然科学基金委员会. 2022项目指南[R/OL]. (2022-01-19)[2022-03-04]. https://www.nsfc.gov.cn/publish/portal0/tab1152/.

[3]

国家自然科学基金委员会. “可信软件基础研究”重大研究计划2014年度项目指南[R/OL]. (2014-07-22)[2022-07-24]. https://www.nsfc.gov.cn/publish/portal0/tab442/info61592.htm.

[4]

国家自然科学基金委员会. 国家自然科学基金委员会关于发布《网络与信息安全》重大研究计划2005年度项目指南及申请注意事项的通告[R/OL]. (2005-05-30)[2022-08-29]. https://www.nsfc.gov.cn/publish/portal0/tab442/info62563.htm.

[5]

国家自然科学基金委员会. 国家自然科学基金重大研究计划《半导体集成化芯片系统基础研究》2002项目申请指南[R/OL]. (2002-01-01)[2022-09-10]. https://www.nsfc.gov.cn/nsfc/cen/xmzn/its/008.htm.

[6]

国家自然科学基金委员会. 国家自然科学基金委员会关于发布《以网络为基础的科学活动环境研究》重大研究计划2003年度项目申请指南的通告[R/OL]. (2003-11-14)[2022-10-17]. https://www.nsfc.gov.cn/publish/portal0/tab442/info62648.htm.

[7]

国家自然科学基金委员会. 国家自然科学基金委员会关于发布“十四五”第一批重大项目指南及申请注意事项的通告[R/OL]. (2021-08-05)[2022-08-18]. https://www.nsfc.gov.cn/publish/portal0/tab442/info81561.htm.

[8]

国家自然科学基金委员会. 国家自然科学基金“十四五”发展规划[R/OL]. (2022-11-11)[2022-11-20]. https://www.nsfc.gov.cn/publish/portal0/tab1392/.

2023年第2卷第1期

PDF下载

2540

1359

引用本文

BibTeX

文章信息

doi: 10.3981/j.issn.2097-0781.2023.01.010

接收时间：2022-12-25
出版时间：2023-03-20
发布时间：2023-03-28

补充材料

相关文章

文章信息

作者

出版历史

收稿日期：2022-12-25
修回日期：2023-02-02

基金

作者信息

1.国家自然科学基金委员会信息科学部，北京 100083

2.电子科技大学计算机科学与工程学院（网络空间安全学院），成都 611731

3.南京航空航天大学计算机科学与技术学院，南京 210016

4.华东师范大学软件工程学院，上海 200062

通讯作者:

^†

参考文献

分享链接

https://castjournals.cast.org.cn/joweb/qzkj/CN/10.3981/j.issn.2097-0781.2023.01.010

分享至

全文二维码

扫描看全文

引用本文

BibTeX

本文的引用情况

表12种不同金属材料的力学参数

科 Family	属数 Number of genus	种数 Number of species	占总种数比例 Percentage of total species (%)	属 Genus	种数 Number of species	占总种数比例 Percentage of total species (%)
鹅膏菌科Amanitaceae	2	11	5.26	鹅膏菌属 Amanita	10	4.78
小菇科 Mycenaceae	2	12	5.74	丝盖伞属 Inocybe	5	2.39
多孔菌科 Polyporaceae	8	14	6.70	蜡蘑属 Laccaria	5	2.39
红菇科 Russulaceae	3	23	11.00	小皮伞属 Marasmius	6	2.87
				小菇属 Mycena	11	5.26
				光柄菇属 Pluteus	5	2.39
				红菇属 Russula	17	8.13
				栓菌属 Trametes	5	2.39

关闭全屏

BibTeX
EndNote
RefWorks
TxT

访问统计

友情链接

联系我们

官方微信公众号

关键词	项目名称匹配		项目关键词匹配		去重后		总项目
关键词	申请数量	资助数量	申请数量	资助数量	申请数量	资助数量	申请数量	资助数量
形式化方法	121	27	454	71	522	90	1599	377
程序验证	43	11	124	37	140	42
模型检测	218	59	500	123	534	131
约束求解	51	15	123	38	138	43
定理证明	38	11	188	42	188	42
程序合成	2	1	21	6	21	6
程序综合	2	1	8	3	8	3
可满足性	79	20	147	37	155	41
安全攸关系统	11	2	11	3	17	4
并发系统	28	9	27	9	40	11
概率程序设计	0	0	1	1	1	1