講座時間：2019年5月7日（周二）14:30-16:00
講座地點：BETVLCTOR伟德官方网站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歐盟科學基金傑出科研獎等重大獎項的獲得者，在推動同步語言國際學術研究方面做出了重要貢獻。
歡迎廣大師生前來聆聽！
