报告题目：基于Event-B 语言的时间建模研究
报告人：   朱晨阳 博士
所在单位：University of Southampton，UK
主持人：   李钦 副教授
报告时间：2018年9月10日    上午  10:00-12:00
报告地点：中北校区理科楼B1002
 
报告摘要：

最近几十年，基础性科学研究越来越受到世界范围的高度重视，其中，形式化方法以及证明工程就是一个重要的发展方向。形式化方法主要使用数学方法来进行系统建模，并且通过数学逻辑及定理来验证模型的正确性及可用性，从而提高系统设计的可靠性和鲁棒性。信息物理系统（cyber-physical system）是一个使用计算机系统通过传感器和制动器来和物理世界交互的系统。其主要的应用有精密农业，智能运输以及医疗检测。 实时性和并发性是信息物理系统的两个重要特点 。一些硬实时系统比如起搏器必须要使用一些调度策略来保证所有的任务都能够按时完成，否则会有性命攸关的问题。时间分析在系统设计中非常重要。然而对于时间的抽象在计算机系统里面是缺乏的。时间计算必须被引入系统设计来保证系统的任务能按时完成。在物理系统里同时会有多个任务同时执行，所以一些调度策略可以保证在多个任务执行的过程中保证所有任务可以按时完成。我们的工作是基于Event-B语言的时间建模。基于一个触发-反馈的模式，我们在Even-B模型中加入时间截止，延迟，终止以及间隔等时间约束。在这个基础上我们提出了一些精细化时间模型的模式。为了解决在时间建模中产生的“Zeno”行为，我们从Event-B模型的轨迹语意角度研究并得出额外的证明条件来排除那些“Zeno”行为。为了解决时间建模中的并发性的问题，我们提出了一种基于不确定性队列的调度策略。这种策略可以被用来解决时间建模的并发性问题，同时可以被精细化为不同的调度策略。 我们将会应用所得出的理论用于一些实际的与时间相关的案例研究，比如软件定义网络，心脏起搏器等。
 
报告人简介：
朱晨阳，博士，本科毕业于华中科技大学，研究生毕业于宾夕法尼亚大学，南安普顿大学博士，研究兴趣包括：形式化方法，时间建模，任务调度，机器学习，数据可视化等。