CCSL: A Formal Time Constraint Language for sound engineering of embedded Cyber-Physical Systems

报告题目：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

报告摘要：

    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.

报告人简介:

    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.