Return to Documents

2013 Activities

VISITS and EXCHANGES:

Visits in Sophia-Antipolis:

  • Yanwen CHEN (PhD student, cotutelle between ECNU Shanghai, and University of Nice Sophia Antipolis): 2013 Jan 1st – July 15th
  • Ass. Pr. Min ZHANG: 2013 Sept. 12th-16th
  • Pr. Yixiang CHEN: 2013 Oct. 14th-17th
  • Yanwen CHEN: 2013 Oct. 14th-15th
  • Dongqian Liu (Master student, ECNU Shanghai): 2013 Oct. 5th – Dec. 31st.
  • Yanwen CHEN: 2013 Nov. 27th-29th
  • additionally, as an indirect consequence of the DAESD spring school at ECNU, Yuanrui ZHANG, student from ECNU is now following the Ubinet international master track (M2) at University of Nice (Sep. 2013-Aug. 2014)

Visits in China:

  • Ludovic HENRIO, Eric MADELAINE, Frédéric MALLET, Robert de SIMONE: 2013 April 26th -Mai 3rd
  • Eric MADELAINE: 2013 Oct. 25th – Nov 5th.

EVENTS:

  • LIAMA Open day and opening ceremony, and DAESD workshop: Shanghai, April 28th. See the program here.

RESEARCH:

  • Timed models for heterogeneous systems. Yanwen Chen, Yixiang Chen, Eric Madelaine. 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. Since the systems have no common physical clock, when investigating its real-time properties, it brings the challenges of correctly describing system behavior in terms of time constraints. How to build a formal timed model, flexible enough to describe its constrained time-related system behavior, and that can express well the asynchronous communication behavior, is a big challenge. We build this work on top of the pNets model, that provides us with a hierarchical and untimed semantic framework well-suited for compositional semantics. Among the new results obtained this year, we have introduced a system of logical clocks with durations, and shown that the resulting timed-pNets model is adaptive enough to fit well the modeling of the clock-independent distributed systems and asynchronous communications. We have expressed a formal defi nition of the model, and illustrated the approach with a simple use-case from the area of intelligent transportation systems.
  • Semantics and Equivalences for parameterized networks of synchronized automata (pNets). Ludovic Henrio, Eric Madelaine, Min Zhang. We have developped a theory of Parameterised Networks of synchronized Automata (called pNets) for specifying parameterised networks of processes. To illustrate the expressiveness of pNets we have developped a large set of classical synchronisation patterns that we express using pNets. In particular, we show that we can exhibit a pNet model for several classical constructs of process calculi, but also that we can simply express more complex interaction patterns used in distributed component frameworks. We have started to investigate further this similarity, developping a bisimulation theory tailored to such parameterized models, going beyond the existing theories of value-passing process algebras. As a fi rst step towards this goal, we are developping a barbed simulation and a barbed congruence relation for pNets.
  • Schedulability analysis with CCSL: CCSL as a specification language allows to describe both asynchronous (before/after) and synchronous (at the same time) relations betweens ticks/events of distinct logical clocks. The partial order/true concurrent style of specification is natural and avoids over-specification at design/modeling time, enforcing modularity and reusability of formerly independent components linked by new constraints. But solving this set of constraints requires to map (in a non-unique way) all these logical clocks onto a single, totally ordered, discrete main base clock. Because of the nature of the constraints, this may be feasible or not, which is amenable to schadulability analysis (on a new language, with its original expressivity). We tackled this issue form diferent angles, one by simulation that seeks to be optimal in a certain way, resulting in the corresponding publication mentioned below.  The other approach consists in expanding all potential behavior in an interleaved semantic fashion (using the “diamond expansion theorem” to go from true concurrency partal orders to interleaved multiple choice semantics). The second result should be covered as part of Yin Ling forthcoming PhD thesis.
  • MARTE UML profile and metamodeling: when designing the Time Model of the UML MARTE profile we had two goals in mind. Th efirst one was that it had to be able to cover existing design approaches with discrete logical time, discrete clocks, and prominent Models of Computation as found in general Concurrency Theory. This other goal was that it should not be devoted only to this type of design, and accomodate also other more classical approaches, based on pseudo-physical (“real”) time and global timing, often described as continuous rather than discrete (as found in Timed Automata and the UppAal analysis environment for instance). While the Time Model definition itself makes large provision for classical continuous global “chronometric” time, it had not received much attention so far. The publication on Hybrid MARTE refered below is one of the first attempts to base design methods on such a representation, including both syntactic (expressivity) and semantic (executability, decidability) issues.
  • Tools for the specification and verification of distributed component-based systems. Ludovic Henrio, Oleksandra Kulhankina, Dongqian Liu, Eric Madelaine. The Grid Component Model (GCM) provides all the means to define reconfigurable component-based applications. We develop the VerCors platform as a specification and verification toolset, including a set of graphical diagram editors for the early specification of the architecture and behavior of GCM components, and tools to check the behavioral properties of such system using model-checking engines. The challenges here are both on the capacity of the tools (abstraction, compositionnal, distributed MC methods) in order to master the inherent state-space explosion of behavioral models;and on providing tools that can be accessible to non-expert users, hiding the complexity of the underlying formalisms. This year, we experimented the formal specification and verification of a reconfigurable GCM application in an industrial case study context. The results were published in the FACS conference. And we have started to port the VerCors graphical editors to a new Eclipse-based platform named Obeo, that will allow us a much better support of the editors for non-expert users, and in particular the coexistence of UML-based diagrams with dedicated formalisms.

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.

  • Yanfang Ma, Min Zhang: “The Infinite Evolution Mechanism of ε-bisimilarity(Extention Version)”; Journal of Computer Science and Technology(JCST). 2013, 28(6): 1097-1105.
  • Nuno Gaspard, Ludovic Henrio, Eric Madelaine; “Formally Reasonning on a Reconfigurable Component-based System – A Case Study for the Industrial World”; 10th Int. Symposium on Formal Aspects of Component Systems (FACS’13), Nanchang, China, Oct. 2013
  • Yanwen Chen, Yixiang Chen, Eric Madelaine;  “A Timed-pNets semantic model for Cyber Physical Systems”; Under submission.
  • Ling Yin, Jing Liu, Zuohua Ding, Frederic Mallet, Robert de Simone; “Schedulabilty analysis with CCSL specifications”; APSEC 2013, Dec. 2-5, Bangkok.
  • Jing Liu, Ziwei Liu, Jifeng He, Frederic Mallet, Zuohua Ding, “Hybrid MARTE statecharts”; Frontiers of computer science 7(1): 95-108; 2013