报告一
摘要：
报告人将介绍其最近在基于模型的安全攸关嵌入式系统形式设计方面的工作。报告人提出的方法首先可以使用Simulink/Stateflow和AADL的组合（AADL+S/S）为待开发系统构建图形模型，并进行广泛的仿真；其次，可以将AADL+S/S图形模型自动转换为HCSP形式模型，以便使用混成霍尔逻辑及其定理证明器验证转换后的HCSP形式模型；再次，为了证明转换后的形式模型正确性，使用HUTP（Higher-order Unifying Theories of Programming）定义了AADL+S/S和HCSP的形式语义，因此可以从理论上证明翻译的正确性。另外，报告人提出了HCSP的近似双模拟概念，并定义了一组精化规则，通过这些规则，可以将HCSP过程精化为SystemC代码或ANSI-C代码，这与原始HCSP过程近似双相似。以上所有理论都已经在MARS 工具链实现，并应用于一些真实世界的案例研究。
报告人简介：
詹乃军，男，1971年5月生，北京大学计算机学院博雅特聘教授，国家杰出青年科学基金获得者。之前，为中科院软件所研究员，中科院特聘研究员，中国科学院大学岗位教授，计算机科学国家重点实验室执行主任。分别在南京大学数学系（1989-1993）和南京大学计算机系（1993-1996）获得学士和硕士学位，在中国科学院软件研究所获得博士学位（1997-2000）。研究方向包括：形式化方法，实时、嵌入式、混成系统，程序验证等。任《Journal of Automated Reasoning》、《Formal Aspects of Computing》、《J. of Logical and Algebraic Methods in Programming》、《Research Direction: Cyber-Physical Systems》、《软件学报》、《计算机研究与发展》、《电子学报》、《前瞻科技》等期刊编委，国际会议MEMOCODE和SETTA的指导委员会委员，多个国际会议程序委员会共同主席（如形式化方法旗舰会议FM 2021 和验证领域顶级会议TACAS 2027）和著名国际会议程序委员会委员（如CAV、RTSS、HSCC、ICCPS、EMSOFT等）；在著名国际会议和杂志发表论文150多篇，出版专著2部，编著4部，国际国内著名杂志专刊7辑等。现任CCF形式化方法专委主任。
报告二
摘要：
安全攸关信息物理融合系统的形式验证往往受限于系统庞大的规模、待验证性质的复杂性、AI部件的不可解释性和不确定性，在设计和实现阶段很难对系统的精确模型进行完全的形式验证。目前，运行时验证作为保障系统运行时需求性质的重要方法，是静态验证的重要补充，其问题复杂性较低，更易在工业界使用，正逐渐成为信息物理融合系统领域的研究热点。本报告将重点介绍基于信号时序逻辑的信息物理融合系统运行时监控技术。首先将介绍信号时序逻辑这一广泛用于描述信息物理融合系统需求性质的规约逻辑，及其定性和定量语义；然后介绍当前信号时序逻辑的离线和在线监控算法，并分析基于传统鲁棒语义监控所引起的信息屏蔽这一问题；最后介绍报告人近期提出的信号时序逻辑因果语义及其监控算法，该方法有效解决了信息屏蔽这一难题。
报告人简介：
安杰，中国科学院软件研究所副研究员，博士生导师，CCF形式化方法专委会委员，主持国家高层次海外青年人才项目、入选中国科学院“率先行动” 引才计划（择优）。此前在德国马克斯普朗克软件系统所和日本国立信息学研究所从事研究工作。目前研究方向为形式化方法和人工智能，致力于将相关理论和方法应用于支撑日常生活的智能信息物理融合系统，以确保其功能性，鲁棒性，可靠性，安全性，隐私性等，相关成果在国家深空探测工程中得到应用。在CAV、TACAS、FM、HSCC、EMSOFT、TCAD等形式化方法和嵌入式系统领域重要国际期刊或会议上发表论文三十余篇，曾获FMAC最佳论文，ATVA杰出论文。
