Title: Model-Checking Yampa Programs in a Discrete Runtime Environment using Uppaal
Time： 14:00-15:00, June3 Monday,2019
Location: Room 1002, Science Building B
Lecturer： Prof.Shoji Yuen Nagoya University
Abstract:
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.
Biography:
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.
