Return to Documents

2014 Activities

VISITS and EXCHANGES:

Visits in Sophia-Antipolis:

  • Yanwen CHEN (PhD student, cotutelle between ECNU Shanghai, and University of Nice Sophia Antipolis): 2014 Feb. 15th – Aug.15th
  • Pr. Yixiang CHEN: 2014 May. 17th, LIAMA workshop in Paris.
  • Yuanrui ZHANG, M2 internship with Robert de Simone and Frédéric Mallet: Apr. 2014-Aug. 2014
  • Pr. Min ZHANG: 2014 Sept. 17th – Nov. 9th.
  • Siqi LI, internship with E. Madelaine, 2014 Oct. 15th – Dec. 15th.

Visits in China:

  • Eric MADELAINE, Frédéric MALLET, Julien DeAntoni: 2014 July 7-11
  • Robert de Simone, 2014 Mar. 24-28
  • Pr. Frédéric Mallet, Long visit in ECNU, 2014 Aug. 15th — June 2015
  • Eric MADELAINE, Ludovic HENRIO, Oleksandra KULANKHNIA, 2014 Nov. 30 – Dec. 5

EVENTS:

  • LIAMA Open day and workshop: Shanghai, July 7th. Program.
  • LIAMA/DAESD Summer School, ECNU Shanghai, July 8-11, Program.
  • Yanwen CHEN PhD defense, ECNU, Nov. 30 2014
  • DAESD final workshop, ECNU Shanghai, Dec. 3, 2014, Program.

RESEARCH:

  • Timed models for heterogeneous systems.  This work is an attempt to build a behavioral semantic model for the cyber part of Cyber Physical Systems (CPSs), which are distributed systems consisting of locally synchronous components among which communications are asynchronous. This work has been developped this year towards a fully compositional method for building hierarchical heterogeneous systems, with: (1) algorithms for the synthesis of time specifications (TS) from timed transition systems, and from compositin of systems expressed as timed-pNets; (2) a compatiblity predicate on TS allowing the composition os systems; (3) algorithm for computing a timed transition system from a TS. This has been accpeted for publication in the FCS journal. The PhD thesis of Y. Chen, in the end of the year, will also contain the application of these methods on a case-study from Intelligent Transportation Systems area.
  • Quantitative Analysis and verification on complex systems.  We focus on formal modeling and formal verification in Internet of Things, especially in the embedded systems and more complex systems. Because of the closer interaction of information network and physical system in these complex systems, variability, uncertainty and ambiguity of the physical world leads inevitably to the difference between physical and digital expression in the modelling. How to control effectively this different effects has become the key issues to improve the modeling of complex systems. The results of our study mainly aims in the environment with incomplete modeling information, how to quantitative analyze and verify the software and hardware systems.  We use a kind of mathematical structure— lattice structure to describe many uncertain information and incomplete information in the complex network system, and establish a series of quantitative formal models. On the other hand, based on the above quantitative models, we propose the theory of quantitative bisimulation and quantitative model checking method, which provides a new method for network authentication technology
  • Schedulability analysis with CCSL:
  • MARTE UML profile and metamodeling: .
  • Tools for the specification and verification of distributed component-based systems. This year we have finished the port of de Vercors Component Editors (VCE) on the Obeo platform, and incorporated in VCE a set of UML diagram editors for the specification of interfaces and behaviors of GCM components. This version is now distributed, and has been used during the DAESD/LIAMA summer school at ECNU. We also have done a full formalisation of structural correctness for GCM component systems, including specific constraints on the separation of concerns netween functional and non-functional aspects of applications. This has been published in Foclasa’14, and implemented in VCE. Then, as Obeo has recently published an open-source Eclipse-based release known as Sirius, we have now started a port on this new platform, that will solve the distribution problems we had with the commercial Obeo platform. Last, we have started implementing the behavioral semantics published last year, that will allow to use model-checking directly from VCE specification, including UML state machines, with as little as possible user help. This should be distributed, within the Sirius version, by the end of the year.

PUBLICATIONS:

All papers here are direct results of the associated team research. Those that are explicitely co-signed by researchers from the two partners are marked in bold face.

  • Ludovic Henrio, Oleksandra Kulankhina, Eric Madelaine, Dongqian Liu; “Verifying the correct composition of distributed components: Formalisation and Tool”; 13th Int. Workshop on Foundations of Coordination Languages and Self-Adaptive Systems (FOCLASA’14), Roma, Italy, Sep. 2014
  • Yanwen Chen, Yixiang Chen, Eric Madelaine: “A Timed-pNets semantic model for Cyber Physical Systems”; Frontiers of Computer Science, Vol. ??, N ??, 2014.
  • Haiyu Pan, Min Zhang, Hengyang Wu, Yixiang Chen: “Quantitative Analysis of Lattice-valued Kripke Structures”; Fundamenta Informaticae, 2014.
  • Haiyu Pan, Yongzhi Cao, Yongming Li, Min Zhang: “Multi-valued model checking with nondeterminism”; Science China, 2014.
  • Haiyu Pan, Yongzhi Cao, Min Zhang， Yixiang Chen: “Simulation for Lattice-valued Doubly Labeled Transition Systems”; International Journal of Approximation Reasoning, 55(2014) 791-811.
  • J. Liu, Z. Liu, J. He, F. Mallet and Z. Ding: “Hybrid MARTE Statecharts”; Frontiers of Computer Science, 7(1):95-108, 2013, Springer.
  • Yuanrui Zhang, Frédéric Mallet, Yixiang Chen: “Transformation of Spatio-Temporal Consistence Language to Timed Automata”; TASE 2014, to Appear