报告题目：CCSL: A Formal Time Constraint Language for sound engineering of embedded Cyber-Physical Systems
报告人：Robert de Simone 教授
主持人： 陈仪香 教授
报告时间：2016年4月19日周二 13：30—15：00
报告地点：中北校区数学馆201
报告人简介:
Prof. Robert de Simone is the Research Director at INRIA, scientific leader of the Aoste research team. From 2009 to 2013 he has been awarded a CNRS research grant in LIAMA and at Tsinghua University. His main research interests are Semantics and implementation of Synchronous Reactive formalisms, Verification tool design, associated algorithmic methods and Concurrency Theory。
报告摘要：
We shall describe a formalism named CCSL (Clock Constraint Specification Language), designed to captured the specific timing constraints occuring in real-time, embedded and cyber-physical systems, and supposed to be applied at formal precise time specification language on top of model-based system description (such as UML behaviorlal diagrams for instance) .
We describe the syntax, practical expressiveness, semantics and theoretical expressiveness of CCSL. We establish it is universal (Turing-complete), but lends itself to easy definition of useful language restrictions that allow subclasses that can be efficiently checked for schedulability (i.e., existence of a solution to the set of constraints) using state-of-the-art automatic solvers.
If time allows we shall illustrate our approach on a use case of big.LITTLE architecture such as found in many nowadays smartphone processors。