报告题目：Acceleration of Real-Time CCSL

  报告时间：10月29日15：00-16：00

  报告地点：理科大楼B1002

  报告人：Frederic Mallet教授

报告人简介：

Frédéric MALLET is director of i3s Laboratory, a French joint research unit between CNRS and INRIA counting around 300 staff members. He is a Distinguished Professor at Université Côte d'Azur and is also a permanent member of the Kairos Team, INRIA/i3s team. His research interests lie in the design of sound formal languages for the modelling and verification of safety critical systems, mainly focusing on timed and temporal models. After his PhD he has spent two years at the University of Edinburgh. From 2006 to 2011, he was in the OMG task force that has defined the UML MARTE Profile and was co-leader of the design of the time sub-profile that gave rise to the Clock Constraint Specification Language (CCSL). In 2014, he was a visiting professor at ECNU in Shanghai.

报告摘要：

The Clock Constraint Specification Language (CCSL) captures the causal and temporal behaviour of a system by specifying constraints on logical clocks. Logical clocks are integer counters that increases, ticks, whenever a given event occur. The ticking marks the advance in time. Chronometric clocks are logical clocks with an external interpretation and an assumption of regularity relative to the time of Physics. However, encoding chronometric clocks as counters may result in verification inefficiencies and hard-to-read specifications. By making explicit those clocks that are chronometric, through a typing system, we allow the use of specific acceleration techniques that benefit from the regularity while still remaining in the logical framework.