LIAMALOGO

SACCADES: Formal Methods for Embedded Systems (merge of TEMPO and HADES projects)

Updated: 2016/11/8   

TEMPO: Trustworthy EMbeded PlatfrOms

Scientific leaders: Dr. Mingsong CHEN (ECNU); Dr. Frank DE BOER (CWI), Dr. Vania JOLOBOFF (Inria)
LIAMA founding members involved: ECNU (China), Inria (France), CWI (Netherlands)
Host: ECNU
Creation: December 2013

PROJECT OBJECTIVES

The goal of the project is to introduce usage of formal methods techniques within a virtual prototyping framework, in order to build more reliable embedded systems. The project is composed of relatively independent tasks, that must however be integrated together to provide the developers with a convenient tool. One can distinguish two orthogonal research directions:

  • developing fast and powerful simulators that can simulate platforms and offer convenient interface to the users,
  • connected to specific tools, the goal of which is to verify required properties of the system.

The first action is mostly relevant to compiler, operating system and simulation research to accelerate or parallelize the simulation. It will be addressed in the project mostly by collaboration between ECNU and INRIA. The second is strongly related to usage of formal methods, as adjunct tools to the previous one. This research will be carried out mostly by ECNU and CWI.

The following section describes the focus of the research in the two directions. This work is accompanied by a relatively important engineering work. In particular, to maintain and extend the SimSoC
simulators, one need to follow up with the technologies underlying SimSoC such as SystemC, CLANG, LLVM, etc...

HADES: HeterogeneousAsynchronous/Distributed and Embedded/Synchronous system development

Scientific leaders: Dr. Yixiang CHEN (ECNU); Dr. Robert DE SIMONE (Inria)
LIAMA founding members involved: Inria (France), ECNU (China)
Host: ECNU
Creation:  December 2012

PROJECT OBJECTIVES

Modern computing architectures are becoming increasingly parallel, at all levels. Meanwhile, typical applications also display increasing concurrency aspects, specially streaming applications involving data and task parallelism. Cyber physical system interactions also add extra-functional requirements to this high degree of concurrency. The goal of best fitting applications onto architectures becomes a crucial problem, which must be tackled from any possible angle.

Our position in the HADES LIAMA project is to consider modeling of applications using formal models of concurrent computation, and specialized model-driven engineering approaches to embody the design flow for such models (analysis, verification, mapping allocation, representation of non-functional properties and constraints).

We build on various previous domains of expertise: synchronous languages for embedded system design, asynchronous languages for high-performance cloud computing, and real-time specification languages for cyber-physical interaction aspects. The various formalisms currently involved in our design methodologies are reported in the picture.

 

 

On Inria side these formal models and related methods are studied as part of the activities of EPI Aoste and Oasis at Sophia-Antipolis Centre.

A more complete description of the HADES project can be found here. 

ACHIEVEMENTS

  • A dedicated Spring School, again named DAESD (Distributed/Asynchronous, Embedded/Synchronous system Development), was organized at ECNU April 27-30, 2013. It was held in conjunction with the inaugural LIAMA Shanghai Opening Day (April 27th). All French and Chinese permanent project members attended these events, together with the French LIAMA Director Vania Joloboff, the Director of ECNU SEI He Jifeng, and officials from    ECNU Shanghai, the Chinese Ministery (MOST) and the French Consulate in Shanghai.  Lectures were given by the French members to Chinese graduate students, from ECNU as well as other universities.

 

  • Visit exchanges (other than above) :

          - Min Zhang visited Inria Sophia-Antipolis in Spetmber 2013. A resulting publication with the EPC Oasis members is under way.

          - Yixiang Chen visited Inria Sophia-Antipolis in October 2013. A short version for a new ANR/NSFC proposal was finalized on this occasion (with the collaboration of Vania Joloboff, now       hosted at ECNU, and Min Zhang).

          - Eric Madelaine visited ECNU after the FACS conference in Jiangxi Univ., Nanchang, from Nov. 3 to Nov. 6 2013.

  • Students :

          - Yanwen Chen visited Inria again, from Jan. 1st to July 14th, as part of her PhD under the co-supervision of Eric Madelaine and Yixiang Chen (co-tutell PhD between E.C.N.U. and Univ. of Nice Sophia-Antipolis).

          - Dongqian Liu, currently Master Student at ECNUconductedher intership period inside the EPC OASIS, from October 6 to December 31, 2013.

          - Yuanrui Zhang, formerly Master Student at ECNU, enrolled into the International Ubinet branch of the Master2 IFI (Computer Science) at the university of Nice Sophia-Antipolis, from September 2013 to August 2014. He is foreseen to spend his internship inside the EPC Aoste, under the supervision of Frédéric Mallet.

PUBLICATIONS

         - Schedulability analysis with CCSL specificationsLing Yin, Jing Liu, Zuohua Ding, Frédéric Mallet, Robert de Simone. APSEC 2013, Dec. 2-5, Bangkok.

         - Hybird MARTE statecharts. Jing Liu, Ziwei Liu, Jifeng He, Frédéric Mallet, Zuohua Ding. Frontiers of Computer Science 7(1): 95-108 (2013).

         - More under submission: A Timed-pNets semantic model for Cyber Physical Systems, Yanwen Chen, Yixiang Chen, Eric Madelaine; pNets: an Expressive Model for Specifying Parameterised Networks of Processes, Ludovic Henrio, Eric Madelaine and Min Zhang.

 
回首页 回前页 回到页首