Return to Documents

2012 Activities

2011-2012 Activities and Visits

  • Nov. 8th 2011: Kickoff Workshop at ECNU Shanghai, with scientific presentations from Pr. Y. Chen, C. Peng, D. Du, M. Zhang, H. Sun (ECNU), E. Madelaine, R. de Simone (INRIA), and V. Joloboff (LIAMA)
  • Dec. 15 2011 – Sep. 30 2012: Yanwen CHEN, PhD, visit to OASIS team in Sophia-Antipolis (first period of a co-tutelle PhD between ECNU and UNS)
  • Sep. 15 2011 – Sep. 15 2012: Ying LIN, visit to AOSTE team in Sophia-Antipolis
  • Mar. 26 2012 – Mar. 29 2012: Visit of Pr. Yixiang CHEN in Sophia-Antipolis; first year DAESD Workshop.
  • Sep. 3 2012: Trustworthy CPS workshop, Newcastle, UK: presentation by Yanwen CHEN.
  • Sep. 17 2012 – Oct. 7 2012: Robert DE SIMONE, visited to ECNU Shanghai and gave an invited seminar
  • Sep. 15 2012 – Dec. 5 2012: Min ZHANG, Ass. Prof, ECNU, visit to OASIS team in Sophia-Antipolis
  • July & Nov. 2012: Yu FENG visited twice ECNU, to arrange cooperation and to discuss future plans, in particular for the Spring School and for the LIAMA project proposal.

Research

Coherent models for synchronous and asynchronous systems:

– Start of work on the formal properties (expressivity, bisimulation theories) of the pNet formalism, during Pr. Min ZHANG visit in Sophia-Antipolis: The subject here is to find a way to define ordering or equivalence relations for the pNets model, and prove under which properties these relations can have good congruence properties with respect to the parallel composition of pNets. Such results could have very important benefits for using pNets for defining the operational semantics of distributed applications, and for using model-checking approaches to prove the behavioural properties of very large systems. This work will be continued in 2013.

– Extension of the pNet model to a(first version of) timed-pNets: this topic is on the extension of the pNets model from Oasis by some notion of time adapted to heterogeneous synchronous/asynchronous systems. This work began with a significant bibliographic study on DAESD systems, and especially so-called GALS (Globally Asynchronous, Locally Synchronous) systems, and of the notion of logical clocks developed by the Aoste team. This visit yield a preliminary definition of “timed pNets” extending pNets by logical clocks, and this definition was published in [TCPS’12].
As a side-effect of this work we managed to set-up a cotutelle convention for the PhD of Yanwen Chen, between ECNU and University of Nice Sophia-Antipolis (UNS). As a consequence, she will spend alternate periods of her PhD at INRIA Sophia-Antipolis and at ECNU Shanghai.

Formal model for temporal & spatial consistency:
We propose a spatial- temporal consistence language for real-time systems (Shortly, STeC). The consistence requires that agents do their tasks at required locations and times. In the paper, we build the denotational semantics of STeC, and investigate the equivalence between denotations and operational semantics of STeC.

Semantics of the Clocks Constraint Language:
Ling Yin spent a year at INRIA Aoste (second year of her PhD) on a funding by the China Scholarship Council (CSC). This visit was prompted by earlier collaborations between Jing Liu (her PhD supervisor at ECNU), and Frédéric Mallet (Associate Professor with the University of Nice/Sophia-Antipolis, member of Aoste). She studied in depth the structural operational semantics design of CCSL construct (CCSL stands for Clock Constraint Specification Language). This resulted into a full compositional translation/interpretation into transition-Generalized Büchi Automata (tGBAs). This translation sets a definite link between schedulability theory and automatic verification (model-checking), as schedulability amounts to non-emptyness checking of the resulting tGBA. More powerful side results can be extracted from the translation, as a new original algorithm has been designed to check this emptiness problem. This resulted into a research report currently submitted for publication to TACAS 2013.

The use and extension of CCSL and the Time Model of MARTE as introduced inside Aoste has been investigated at ECNU to cope with hybrid systems and continuous (logical) time. This resulted into a publication at the APSEC conference. This promising direction of work should be extended in several directions in the future, but in its own sake and in connection with existing efforts in the theoretical foundations of hybrid models for simulation and verification.

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.

International Conferences and Workshops

  • Yixiang Chen, STeC: A Location-Triggered Specification Language For Real-Time Systems, 2012 IEEE 15th International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops, pp. 1-6, 2012. DOI 10.1109/ISORCW.2012.11
  • Yanwen Chen, Yixiang Chen, Eric Madelaine, “Timed-pNets: A formal communication behavior model for real-time CPS system”, in Trustworthy Cyber-Physical Systems (Newcastle, UK., Sep. 2012)[Paper]
  • Haiyu Pan, Min Zhang , Yixiang Chen. “Bisimilarity for Fuzzy Doubly Labeled Transition Systems” 2012 International Conference on Quantitative Logic and Soft Computing (QL&SC’12), pp. 207-214. doi: 10.1142/9789814401531_0030
  • Haiyu Pan, Min Zhang, Yixiang Chen. “Lattice-Valued Kripke Structures Based on Complete Residuated Lattice”. In the proceeding of 2012 IEEE Sixth International Conference on Software Security and Reliability Companion (SERE’12), pp 137-143. 2012. DOI 10.1109/SERE-C.2012.29
  • Haiyu Pan, Min Zhang, Yixiang Chen. “Bisimulation for Lattice-valued Transition Systems”. In Proceeding of the 6th IEEE International Conference on Theoretical Aspects of Software Engineering (TASE’12), pp.279-282, 2012
  • Ziwei Liu, Jing Liu, Jifeng He, Frédéric Mallet, Miaomiao Zhang: “Formal Specification of Hybrid MARTE Statecharts”. 6th IEEE International Conference on Theoretical Aspects of Software Engineering (TASE’12), pp 59-66, 2012
  • Xiaohong Chen, Jing Liu, Frédéric Mallet, Zhi Jin: “Modeling Timing Requirements in Problem Frames Using CCSL”. In 18th Asia Pacific Software Engineering Conference (APSEC’11): 381-388, Ho Chi Minh City (Vietnam), dec. 2011.

Others

  • Rabéa Ameur-Boulifa, Ludovic Henrio, Eric Madelaine, Alexandra Savu, “Behavioural Semantics for Asynchronous Components”, INRIA RR8167, Dec. 2012, [RR8167]
  • Ling Yin, Julien DeAntoni, Frédéeric Mallet, Robert de Simone, Jing Liu: “Schedulability analysis by exhaustive state space construction: translating CCSL to transition-based Generalized Büchi Automata”, INRIA Research Report 8102, Oct. 2012. [RR8102]