编辑: | 来源:信息学院 | 发布时间:2019-05-05 | 浏览量：
讲座时间：2019年5月7日（周二）14:30-16:00
讲座地点：信息学院216
讲座主题：物联网形式化验证技术
主讲嘉宾：Jean-Pierre
语言：英文
讲座内容：
The IoT is a network of devices that sense, actuate and change our immediate environment. Against this fundamental role of sensing and actuation, design of edge devices often treats action and event timing to be primarily software implementation issues: programming models for IoT abstract even the most rudimentary information regarding timing, sensing and the effects of actuation. As a result, applications programming interfaces for IoT allow wiring systems fast without any meaningful assertions about correctness, reliability or resilience.
We make the case that the "API glue" must give way to the logical closure of interface types. Interfaces can be governed by a calculus – a refinement type calculus – to enable reasoning on time, sensing and actuation, in a way that provides both deep specification refinement, for mechanized verification of requirements, and multi-layered abstraction, to support compositionality and scalability, from one end of the system to the other.
From small to big, our project will be illustrated by two recent case-studies we participated in, from the correctness proof of specification requirements of a stepper motor controller to the parametric protocol verification for large sensor networks.
嘉宾简介：
Jean-Pierre，法国计算机及自动化研究院高级教授研究员 ，法国国家信息与自动化研究所（INRIA）项目团队ESPRESSO负责人，JITEA2项目OPEES的法国国家信息与自动化研究所（INRIA）方面的科学代表和执行主管，SLAP++研讨会系列指导委员会的委员。同时，教授于2014年和2017年获得中国外国专家局授予的高端外国专家荣誉称号，于2014年获得中国科学院授予的中科院外国专家特聘研究员荣誉称号。
近年来教授在ACM Transactions等国际期刊和IEEE，springer检索的重要会议上发表高水平学术论文百余篇，并获得ACM/IEEE LICS 的20 年杰出论文奖、ACM SIGPLAN的POPL 10年最有影响论文奖，2004年ACM 最佳论文奖，同时又是ANR法国科学基金科研成果奖以及ITEA2欧盟科学基金杰出科研奖等重大奖项的获得者，在推动同步语言国际学术研究方面做出了重要贡献。
欢迎广大师生前来聆听！
