报告题目：Model-Checking Yampa Programs in a Discrete Runtime Environment Using Uppaal
报告人：    Prof.Shoji Yuen   Nagoya University
主持人：    李鑫 副研究员
报告时间：2019年6月3日  周一14:00-15:00
报告地点：理科大楼B1002

报告摘要：
We propose a model-checking method of Haskell/Yampa programs in the discrete sampling runtime environment using Uppaal. Yampa is a domain specific language of the Haskell programming language for hybrid systems, where both continuous and discrete behaviour are combined in its behaviour. A Yampa program executes continuous behaviour in a discrete runtime environment by sampling.  If sampling misses a critical point in changing the behaviour, the Yampa program may result in unexpected error although the program is supposed to be correct in the continuous semantics. We focus on such ill behaviour caused by the latency of sampling.   Usually, the sampling rate jitters in the runtime.  Therefore, in order for a Yampa program to behave correctly, we need to code a program so that the latency does not affect the basic behaviour.  We describe the discrete behaviour of Yampa programs triggered by the sampling signal.  We automatically converted a subclass of Yampa programs to a transition system composed by a clock with jitter. We check the behavioural property of the Yampa programs by the Uppaal model checker.  We illustrate erroneous behaviour as the counter example against the expected property in the continuous behaviour in the bouncing-ball program and moving-ball. 

报告人简介：
Shoji Yuen is Professor and Head of Department of information Engineering of Nagoya University, Japan. He received Ph.D. from Nagoya University in 1997. He has been a Professor at the Graduate School of Informatics of Nagoya University since 2007. His research interests are theories and applications of concurrency, especially for communicating software systems. Based on the theoretical framework of communicating processes, he has been working on the additional notion of data, and time to extend the application of the framework.