软件所形式化 周巢尘 院士
报告生成时间：2026年8月20日
个人主页：周巢尘
所属团队：中国科学院软件研究所 / 计算机科学国家重点实验室
一、学者基本信息
| 项目 | 内容 |
|---|---|
| 姓名 | 周巢尘（Zhou Chaochen） |
| 性别 | 男 |
| 出生日期 | 1937年11月1日 |
| 出生地 | 上海 |
| 当前职称 | 中国科学院软件研究所研究员、博士生导师 |
| 院士身份 | 中国科学院院士（1993年当选，信息技术科学部）；第三世界科学院院士（现发展中国家科学院院士，2000年当选） |
| 学会身份 | CCF会士；2018年度CCF终身成就奖获得者 |
| 所属机构 | 中国科学院软件研究所 |
| 曾任国际职务 | 联合国大学国际软件技术研究所（UNU-IIST）首席研究员（1992–1997）、所长（1997–2002） |
| 研究方向 | 计算机科学理论、软件形式化理论、分布式程序设计理论、实时系统形式化设计与验证（时段演算） |
| 标志性贡献 | 提出时段演算（Duration Calculus, DC），带动国际上二十几个国家的科学家参与研究 |
二、教育背景与职业履历
2.1 教育经历
| 时间 | 院校 | 学位/阶段 | 备注 |
|---|---|---|---|
| 1953–1958 | 北京大学数学力学系 | 本科 | 北大数学院54级院友，打下深厚的数学基础 |
| 1967 | 中国科学院计算技术研究所 | 研究生 | 研究生期间研读数理逻辑，师从数理逻辑学家、计算机科学家胡世华院士 |
周巢尘的学术根基是纯粹的数学与数理逻辑。其导师胡世华（1912–1998）是中国数理逻辑研究的代表人物之一，也是国内最早倡导将逻辑研究与计算机设计相结合的学者。这一"数理逻辑→计算机科学"的学术谱系，深刻塑造了周巢尘日后以逻辑为工具研究软件理论的研究风格。
2.2 职业履历
| 时间 | 单位 | 职位 | 说明 |
|---|---|---|---|
| 1985 | — | 被聘为博士生导师 | |
| 1986.6起 | 中国科学院软件研究所 | 研究员 | 长期在软件所从事计算机科学理论研究 |
| 1992–1997 | 联合国大学国际软件技术研究所（UNU-IIST，澳门） | 首席研究员（Senior Research Fellow） | 兼任 |
| 1993 | — | 当选中国科学院院士 | |
| 1997.8–2002.9 | 联合国大学国际软件技术研究所（UNU-IIST） | 所长（Director） | 兼任；离所期间保留中科院软件所教授职位 |
| 2000 | — | 当选第三世界科学院院士 |
UNU-IIST时期是周巢尘国际学术影响力的高峰期。他在澳门领导UNU-IIST期间，通过"Fellow计划"吸纳了大批发展中国家青年学者参与形式化方法研究，产出了大量高水平的UNU/IIST技术报告，其中时段演算的许多奠基性成果（包括高阶时段演算）均以UNU/IIST Report形式发表。2018年，Springer出版《Symposium on Real-Time and Hybrid Systems》论文集，献给周巢尘80岁生日，足见其国际学术声誉。
三、学生培养情况
3.1 核心学术传承者：詹乃军
周巢尘→詹乃军是中科院软件所形式化方法方向最核心的学术传承关系，其传承链条清晰且成果丰硕：
| 项目 | 内容 |
|---|---|
| 学生姓名 | 詹乃军（Naijun Zhan） |
| 师承关系 | 1997–2000年在中国科学院软件研究所攻读博士学位，导师周巢尘 |
| 博士论文 | 《高阶时段演算及其应用》（2000年）——直接继承并发展了周巢尘的时段演算理论 |
| 毕业后经历 | 2001–2004年在德国曼海姆大学数学与信息学院工作；后回软件所历任研究员、中科院特聘研究员、中国科学院大学岗位教授、计算机科学国家重点实验室（执行）主任 |
| 现任职务 | 北京大学计算机学院博雅特聘教授（2024年起，兼任）；中科院软件所研究员、博士生导师；CCF形式化方法专业委员会主任；国家杰出青年科学基金获得者 |
| 合作成果 | 与周巢尘合著《形式语义学导论》（Introduction to Formal Semantics，Academic Press，2017）；合著高阶时段演算论文（UNU/IIST Report No. 167, 1999） |
传承的延续性：詹乃军将周巢尘开创的时段演算从实时逻辑拓展到混成系统（Hybrid Systems）与信息物理融合系统（CPS）的形式化设计与验证，提出了混成霍尔逻辑（Hybrid Hoare Logic）、混成CSP（HCSP）等理论，并研制了MARS工具链。其团队完成的国产多核实时操作系统微内核全流程形式化验证（2.5万行源码、45万行Coq验证代码、修正两百余项缺陷、通过CC EAL5+安全认证），正是周巢尘"实时系统形式化设计"学术纲领在工业级安全攸关系统上的落地。詹乃军还担任FM 2021、TACAS 2027等国际顶级会议程序委员会共同主席，将这一谱系的影响力推向国际舞台。
3.2 UNU-IIST时期培养的国际学术力量
周巢尘在UNU-IIST期间（1992–2002）通过Fellow机制培养了大批国际学者，其中多人成为时段演算及实时系统形式化研究的中坚：
| 学者 | 国籍/背景 | 与周巢尘的合作及后续发展 |
|---|---|---|
| Dang Van Hung（邓文鸿） | 越南 | UNU-IIST Fellow，与周巢尘、李晓山合著《A Duration Calculus with Infinite Intervals》（FCT 1995 / UNU/IIST Report No. 40），后成为越南科学院教授、越南实时系统形式化研究的领军人物 |
| Dimitar P. Guelev | 保加利亚（索菲亚大学） | UNU-IIST Fellow（1998），与周巢尘、詹乃军共同建立高阶时段演算（Higher-Order Duration Calculus），后为保加利亚科学院教授 |
| 李晓山 | 中国 | 时段演算核心合作者，后任职丹麦、英国等地，从事程序理论工作 |
3.3 国内培养的其他学生与合作者
除詹乃军外，周巢尘在软件所长期担任博士生导师（1985年起），其学生和学术后辈形成了软件所形式化方法团队的中坚，包括张文辉（Linux内核形式化验证专家）等一批活跃于程序逻辑与形式验证领域的学者。
四、学术合作网络
4.1 软件所内部合作
中科院软件所计算机科学国家重点实验室（现基础软件与系统重点实验室等）是中国形式化方法研究的重镇，周巢尘与所内核心学者构成"双院士+中生代"的团队格局：
| 成员 | 职称/身份 | 研究方向 | 与周巢尘的关系 |
|---|---|---|---|
| 林惠民 | 中科院院士、研究员 | 并发理论、进程代数（世界上首个通用进程代数验证工具、符号互模拟理论、π-演算有穷公理化） | 软件所并列的两院院士级理论大家，共同构成实验室的理论支柱 |
| 詹乃军 | 中科院软件所研究员（兼北京大学博雅特聘教授）、CCF形式化方法专委会主任 | 实时/混成系统、程序验证、CPS | 周巢尘的博士学生和学术传承人 |
| 吴志林 | 研究员、CCF形式化方法专委会秘书长 | 程序逻辑、形式验证 | 詹乃军谱系的核心成员，承担专委会日常学术组织工作 |
| 张立军 | 研究员 | 概率模型检验、量化验证 | 实验室形式化方法方向骨干 |
| 安杰 | 副研究员、博导 | 信息物理融合系统运行时验证 | 曾在德国马普所、日本NII工作，归国加入软件所 |
这一"周巢尘/林惠民（院士）→詹乃军/张立军（杰青级）→吴志林/安杰（骨干）"的梯队，使软件所形式化方法方向的传承跨越三十年而不衰。
4.2 跨机构合作
- 北京大学：周巢尘本科母校，也是其学术传人詹乃军的现任职单位。詹乃军2024年起兼任北大计算机学院博雅特聘教授，将时段演算谱系与北大软件理论（含杨芙清院士开创的软件工程体系）相结合。
- 南京大学：詹乃军的本科/硕士母校（数学系+计算机系），数理逻辑训练背景与周巢尘的治学路径一脉相承。
- 国内形式化方法学界：通过CCF形式化方法专业委员会（詹乃军任主任、吴志林任秘书长）联结国防科技大学（董威、王戟）、华东师范大学（陈铭松）、复旦大学、南京大学（李宣东团队）、武汉大学等全国形式化方法力量。
- 欧洲（德国）：詹乃军在德国曼海姆大学（2001–2004）的经历使团队与德国形式化方法界建立深厚联系；詹乃军与德国不来梅大学教授Martin Fränzle保持长期合作（多篇混成系统与随机系统验证论文）。
4.3 国际合作
周巢尘的国际合作网络是老一辈中国计算机科学家中最具全球影响力的网络之一：
| 合作者 | 机构 | 合作内容与意义 |
|---|---|---|
| C.A.R. Hoare（托尼·霍尔） | 牛津大学，1980年图灵奖得主 | 1991年与周巢尘、A.P. Ravn共同提出时段演算（Duration Calculus），发表于实时系统形式化经典文献；这是中国学者与图灵奖得主在程序理论领域最著名的合作之一 |
| A.P. Ravn（Anders P. Ravn） | 丹麦奥尔堡大学 | 时段演算三位共同提出者之一，实时系统形式化设计"ProCoS"项目的核心人物 |
| Michael R. Hansen | 丹麦技术大学 | 与周巢尘合著专著《Duration Calculus: A Formal Approach to Real-Time Systems》（Springer, 2004），是该领域权威参考文献 |
| UNU-IIST国际网络 | 联合国大学（澳门） | 周巢尘任所长期间（1997–2002），UNU-IIST成为面向发展中国家的形式化方法国际培训与合作枢纽，培养了越南、保加利亚、印度、巴基斯坦等数十国的学者 |
时段演算自1991年提出后，带动了国际上二十几个国家的科学家参与研究，衍生出大量扩展（概率时段演算、超稠密时段演算、高阶时段演算等），并被整合进混成系统验证的主流工具链。2018年Springer出版的《Symposium on Real-Time and Hybrid Systems》论文集（由詹乃军、Dang Van Hung、Martin Fränzle等编辑）作为献给周巢尘80岁生日的贺礼，收录了全球实时与混成系统领域顶尖学者的论文，是衡量其国际影响力的标志性事件。
五、业界合作关系深度分析
5.1 安全攸关系统中的形式化方法应用
周巢尘开创的理论经由詹乃军团队在工业界实现了大规模落地：
- 航天领域：基于时段演算思想发展的混成霍尔逻辑与MARS工具链，应用于航天安全攸关嵌入式系统的形式设计与分析；相关方法被纳入面向航天、核电、军工领域的CNCC Tutorial等产业培训体系。
- 国产操作系统认证：詹乃军团队对国产多核实时操作系统微内核完成全流程形式化验证（验证2.5万行系统源码，开发45万行Coq验证代码，排查修正两百余项程序缺陷），助力该系统通过CC EAL5+安全认证——这是形式化方法在中国基础软件工业界最具标志性的应用成果之一。
- 高铁等交通控制系统：时段演算作为实时系统需求规约语言，为列控等安全攸关系统的时序性质描述与验证提供了理论基础，其思想被国内可信软件重大研究计划的相关工作吸收。
5.2 形式化方法在工业界的推广生态
周巢尘学术谱系与工业界的连接主要通过三条渠道实现：
- CCF形式化方法专委会：詹乃军（主任）、吴志林（秘书长）领导的专委会通过CCF中国软件大会（NASAC+FMAC）、CCF@U走进高校/企业等活动，推动形式化验证技术与航天（北京控制工程研究所顾斌团队）、航空计算（西安航空计算技术研究所）等军工单位的对接。
- 标准与认证体系：CC EAL5+等安全认证中的形式化验证要求，直接源于该谱系推动的可信软件理论与工程实践。
- 工具链产业化：MARS工具链（AADL+Simulink/Stateflow建模→HCSP形式模型→混成霍尔逻辑验证→自动代码生成）打通了从工业建模语言到可验证形式模型的完整链条，降低了形式化方法在工业部署的门槛。
5.3 与国家战略的对接
周巢尘晚年倡导的"可信软件"理念通过其学术传人进入国家科技规划：国家自然科学基金委"可信软件基础研究"重大研究计划、973/重点研发计划中的形式化方法课题、以及国产基础软件自主可控战略中，时段演算谱系的形式验证技术均为核心支撑之一。
六、重要奖项与学术兼职
6.1 重要奖项与荣誉
| 年份 | 奖项/荣誉 | 颁发机构 | 说明 |
|---|---|---|---|
| 1993 | 中国科学院院士 | 中国科学院 | 信息技术科学部 |
| 1997–2002 | UNU-IIST所长 | 联合国大学 | 首位担任该职的中国计算机科学家 |
| 2000 | 第三世界科学院院士 | 第三世界科学院（TWAS，现发展中国家科学院） | |
| 2018 | CCF终身成就奖 | 中国计算机学会 | 与何新贵院士同获；该奖每年获奖人不超过两名；同为北大数学院友的获奖者还有杨芙清（2011）、沈绪榜（2016） |
| 2018 | 《Symposium on Real-Time and Hybrid Systems》论文集（Springer） | 国际学界 | 献给周巢尘80岁生日，全球实时/混成系统学者集体致敬 |
| — | CCF会士 | 中国计算机学会 |
6.2 学术兼职
- 联合国大学国际软件技术研究所（UNU-IIST）首席研究员、所长（1992–2002）
- 中国科学院软件研究所研究员、博士生导师
- 长期担任《计算机科学技术学报》（JCST）等国内外学术刊物的工作，推动形式化方法成果的国际发表
- 通过UNU-IIST Fellow计划，实质上承担了联合国框架下发展中国家软件技术人才培养的导师职责
七、Connection圈层总结
周巢尘院士的学术关系网络可从以下圈层进行总结：
第一圈层：学术谱系核心
周巢尘师承数理逻辑学家胡世华院士（中科院计算所研究生时期），形成了"数理逻辑→程序理论"的独特谱系。其上承中国第一代计算机科学家，下启以时段演算为核心的实时系统形式化学派，是连接中国计算机科学"逻辑传统"与当代形式化方法国际前沿的关键节点。
第二圈层：直系学术传承
詹乃军是周巢尘学术遗产的核心继承人：博士论文即高阶时段演算，后将其发展为混成系统形式化设计的完整体系（HCSP、混成霍尔逻辑、MARS工具链），并担任CCF形式化方法专委会主任、国际顶会FM/TACAS程序委员会共同主席，完成了从"院士开创理论"到"杰青引领应用"再到"国际学术组织领导者"的三级跃迁。UNU-IIST时期培养的Dang Van Hung（越南）、Dimitar Guelev（保加利亚）等则将该谱系扩展为跨国学术网络。
第三圈层：软件所团队网络
中科院软件所计算机科学国家重点实验室形成"林惠民（并发理论）+周巢尘（时段演算）"双院士格局，其下由詹乃军、张立军、吴志林、安杰等构成中生代梯队，并经由CCF形式化方法专委会辐射国防科大、华东师大、复旦、南大等全国力量。
第四圈层：国际学术网络
以图灵奖得主Tony Hoare、丹麦奥尔堡大学A.P. Ravn为标志的欧洲合作网络（时段演算三位奠基人）；以UNU-IIST为枢纽的发展中国家学者网络；以及由二十几个国家科学家组成的时段演算研究共同体。
第五圈层：产业转化网络
通过詹乃军团队连接航天（安全攸关嵌入式系统验证）、国产操作系统（CC EAL5+认证）、交通控制等安全攸关产业领域，实现了从理论原创到工业级可信软件的完整闭环。
整体特征
周巢尘的关系网络具有以下显著特征：
- 理论原创的全球辐射力：时段演算是极少数由中国学者原创、并带动全球二十余国科学家跟进的计算机科学理论，其国际影响力以Hoare（图灵奖得主）合作为顶点、以80岁生日Springer贺寿论文集为集中体现。
- 谱系传承的完整性：从胡世华→周巢尘→詹乃军→（吴志林等新一代），跨越三代、延续六十余年，且每一代均有院士/杰青级代表人物，是中国计算机理论界传承最清晰的谱系之一。
- 国际组织领导经验独特：担任UNU-IIST所长五年，是老一辈中国计算机科学家中罕见的执掌国际研究机构者，这段经历为其学术网络注入了跨国培养与多边合作的基因。
- 从纯理论到安全攸关工业的落地路径：时段演算从抽象的区间逻辑出发，最终在航天软件验证、操作系统CC EAL5+认证等国家级工程中发挥作用，体现了"顶天立地"的学术风格。
- 晚年荣誉的顶格认可：CCF终身成就奖（2018）与第三世界科学院院士的双重加冕，标志着国内外学界对其毕生贡献的一致肯定。