出访团组名称

张杰等壹人赴澳大利亚一人团组

出访人团组成员

部门

职务

张杰

信息学院

副教授

出访国家或地区

澳大利亚

拟出访日期

2017.10.1-2017.12.10

邀请单位

澳大利亚新南威尔市大学

经费来源及

拟支出金额

经费来源：以国家自然基金项目为主支出

拟支出金额：158265元

出访任务

及日程安排

第1周、2019年10月1日—2019年10月6日(6天)

该段时间开展软件形式化求精方法的研究，该方法是将自动推理和形式化方法相结合而形成的一门新技术，它研究从抽象的形式规格推演出具体的面向计算机的程序代码的全过程。其基本思想是用一个抽象程度低、过程性强的程序去代替一个抽象程度高、过程性弱的程序，并保持它们之间功能的一致。

第2周、2019年10月7日—2019年10月13日（7天）

该段时间内，我们将采用逻辑建模和关键属性分解与综合形式化验证方法对计算机软件进行深入研究。即将研究常规解析型数学模型映射为逻辑型数学模型的过程，具体地说，就是把常规解析型数学模型方程解的存在性、唯一性与稳定性证明映射为逻辑型数学模型方程解的等价性、蕴含性与互斥性证明。

第3周、2019年10月14日—2019年10月20日（7天）

该段时间内我们主要讨论实时ROS的设计，从操作系统方法学层面五大基本指标的优势提出理论上改进的地方。与传统操作系统不同之处在于对外界的反馈，为项目的顺利进行提供坚实的理论基础。

第4周、2019年10月21日—2019年10月27日（7天）

从理论分析的角度提出建立关键数学模型，以及从数学角度证明方案的可行性。开展软件形式化求精方法的研究，该方法是将自动推理和形式化方法相结合而形成的一门新技术，它研究从抽象的形式规格推演出具体的面向计算机的程序代码的全过程。

第5周、2019年10月28日—2019年11月3日（7天）

从数学上建立模型，证明该高可靠实时电子系统的可行性。从理论上求解出能够达到的最好和最差情况的平均响应时间和截止时限。

第6周、2019年11月4日—2019年11月10日（7天）

开展用一个抽象程度低、过程性强的程序去代替一个抽象程度高、过程性弱的程序，并保持它们之间功能的一致性的研究工作。

第7周、2019年11月1日—2019年11月17日（7天）

开展计算机软件系统的出错概率的评估工作。研究计算机软件系统的可靠度是其总体失效率的函数，如何由可靠度折算成系统的平均失效率λ。

第8周、2019年11月18日—2019年11月24日（7天）

该段时间内，我们将采用逻辑建模和关键属性分解与综合形式化验证方法对计算机软件进行深入验证。

第9周、2019年11月25日—2019年12月1日（7天）

进一步在HOL4中建立软件的失效率和可靠度模型，使用逻辑推理方法证明系统的可靠度，并可得符号仿真和数值仿真算法。

第10周、2019年12月2日—2019年12月8日（7天）

总结把常规解析型数学模型方程解的存在性、唯一性与稳定性证明映射为逻辑型数学模型方程解的研究方法，进行组内汇报；同时对应用在恶劣环境下嵌入式软件的验证与分析的现有技术进行讨论，提出改进的方法与方向。

2019年12月9日

讨论确定下一步合作研究计划，尤其是在嵌入式软件可靠性和鲁棒性的形式化验证及项目分析领域。

事后公示

请在回国后1个月内在单位内部公布上述公示内容的实际执行情况和出访报告。

公示期7天，如有异议，请于7月5日下午5:00前请将书面意见反馈至国际交流与合作处，联系电话：010-64448919；邮箱ygcf@mail.buct.edu.cn