Oct 23

Presentation of the Associated-Team

1.     Abstract of the scientific program 

Cyber-Physical Systems (CPS) and the connected Internet of Things (IoT) are inherently heterogeneous systems, with (“cyber”) computer digital parts interacting with their physical sensible environment. Thus, design of such systems as a whole requires a diversity of models, and the behavior orchestration between such models must be carefully defined and analyzed. FM4CPS will address several facets of Formal Model-Driven Engineering for Cyber-Physical Systems (and their relevance in Internet of Things). The design of such large heterogeneous systems calls for hybrid modeling, combining  formal Models of Computation, drawn from Concurrency Theory for the “cyber” discrete processors, timed extension and continuous behaviors for physical environments, requirement models and user constraints extended to non-functional aspects, new challenges for designing and analyzing large and highly dynamic communicating software entities.

Orchestration and comparison of models, with their expressive power vs. their decidable aspects, shall be considered with the point of view of hybrid/heterogeneous modeling here. Main aspects are the various timing or quantitative structure extensions relying for instance on a hybrid logical clock model for the orchestration of underlying components. The associated team aims at various level of research, from formal models, semantics, or complexity, to experimental tools development. This will start for example on one side with building a formal orchestration model for CPSs, based on an hybrid clock model that combine discrete and physical time, synchronous and asynchronous computations or communications. Another goal will be the study of expressiveness and decidability for CPS, based on dedicated sub-families of well-structured push-down systems, addressing both unbounded communication and time-sensitive models. Formal and compositional reasoning on Internet of Things (IoT) connected objects, which bear strong connection with CPS, will complete our research areas.

Beyond their own expertise in this field, the partners will build on the results of previous cooperation in the context of the Liama projects Hades and Tempo, and the associated team DAESD. The current proposal widely broadens the domain of collaboration, and with the inclusion, for the first time, of Jiao Tong University. We expect this is the first step towards the extension of LIAMA in Shanghai with the strengthening of the involvement of E.C.N.U., and the contribution of new top notch universities such as Jiaotong University in Shanghai.

2.     Annual report 2015

     2.1.     Scientific progress – 2015

We have proposed a new language (BCool) for the orchestration of heterogeneous Models of Computation. Individual models are abstracted away by its behavioral language interface, i.e., a set of logical clocks that serve both as observation points and activation. The CCSL formalism was used to describe causalities and synchronizations between these logical clocks, specifying the desired orchestration. BCool decides which CCSL constraint should then be applied, and when. This work was presented at the international conference MoDELS 2015 [1]. The tool development aspects have also been presented in a separate demo session.

To better address the aspects of physical uncertainties in CPS, we have proposed an extension of CCSL with stochastic constructs [2]. Having a stochastic characterization is a way to help specify non-deterministic constraints from the environment in a quantitative way.

The OMG UML profile MARTE can use CCSL constraints to specify the orchestration of distinct UML models: UML State Machines, UML Activities, MARTE Time model of logical clocks. The relevance of MARTE (with and beyond CCSL) to model CyberPhysical Systems has been addressed in an article, included as chapter of a book [3] put up by partners of the International Lab led by ECNU.

We published a journal article that summarizes the different forms of correctness issues that may arise with CCSL, given its expressiveness, and how they can be dealt with [4]. Links to Petri Nets, Buchi automata and Esterel specifications were also expressed (as part of an on-going work). An encoding of a CCSL fragment in MAUDE, discussing decidability issues for schedule periodicity, is under completion [5].

The Chinese partners have used CCSL and the MARTE Time model to specify a realistic Interactive Telemedicine System [10]. Work was also conducted on the denotational semantics of SystemC and related formalisms, using UTP as interpretation domain, and the algebraic axiomatization of the corresponding program equivalence; this work considers in particular the two-dimensional shape of time in this language, with instantaneous causality needed for event-driven simulation encoded as delta-cycles [11].

Vania Joloboff, Frederic Mallet and an ECNU student, Daian Yue have started to work on a new run time verification approach. Simulators generate traces that can be used to verify that the required properties of the system are not violated. There exist assertion languages like PSL that may be used to verify required properties during the simulation session. This requires however that the properties to verify are known at compile time of the simulator. It is the case for a number of properties, but it is also the case that many properties are actually unknown when the simulator models are coded! In most cases, during system design the simulation fails: the engineers then investigate the cause of the failure. A widely used technique for that consists in storing all of the trace data of simulation sessions into trace files, which are analyzed later with specialized trace analyzer tools. An issue then is that the trace files become huge, possibly hundreds of Gigabytes as all data are stored into the trace files. The engineers after iterative refinement steps, which are very time consuming, eventually identify the cause(s) of the failures, most often some unforeseen causality chain of events and state transitions  that lead to a failure state. Then a new required property is identified, it can be expressed and the simulator recompiled to check the new property.

We have been investigating a technique for trace analysis with a language and a compiler based on CCSL for discovering properties without recompiling the simulator although we expect the trace files size to be an order of magnitude smaller. The idea is that a new tool is being designed as a domain specific language (using the Eclipse Modeling Framework). The tool should allow users to define a mapping model from the local simulation events to a logical clock format as well as a user friendly property specification language.  The property specification language is translated into CCSL formulas, which in turn generate automata. The mapping library is dynamically loaded by the simulator and generates input for the automata. The verification of the properties can be dynamically, with a true runtime verification, or statically by analyzing the (much smaller) trace files.

This year we have designed the architecture described above and carried some experimental work, but the implementation still remains to be done. There also remain some theoretical issues with regards to which properties can be effectively verified.

With Pr Mingsong Chen from ECNU, we have started to investigate parallel SystemC simulation for simulation of many-cores platforms. The idea is to run in parallel the simulation of each individual core, although the peripherals and the main model remain in the SystemC sequential scheduling. We have reached some results, but there are still pending issues to resolve regarding clock synchronization of the individual cores…

With Pr Min Zhang from ECNU, we have done some theoretical developments on the properties of the low level behavioral model called “parameterized networks of synchronized automata (pNets)”, and published these at PDP’2015. This work shows how pNets can be used for encoding many concepts of distributed systems, both synchronous or asynchronous, and how the properties of a specific bisimulation equivalence justifies the usage of pNets as a compositional approach in our verification platform. With Pr Huibiao Zhu, and with Siqi Li, we also started studying a UTP-based denotational semantics for pNets.

With Pr Min Zhang, we started to work on a direct and symbolic semantics for “open pNets”, aiming at a behavioral semantics and a proof methodology for open systems, like process expressions, or program skeletons. Preliminary results were presented in a workshop in Shanghai in July, and a master internship is ongoing on this subject.

     2.2.     Next year’s work program

Most of the topics described in the proposal technical annex, and partially addressed during the first year, are still ongoing activities. They concern mostly the issues of formal modeling of CPS using the relevant specification formalisms, so that stringent features can be considered, sound semantic interpretations defined, leading to effective and efficient verification with existing or new tools. Several short-time research directions can be mentioned here:

  • Extension of the CCSL formalism with priority and preemption notions; in a possibly asynchronous (or multiform time) environment, this may require to introduce a dual clock feature (clock_enabled, clock_disabled) to specify mathematically their relation with the actual clock_event.
  • Extension of CCSL with probabilistic features; one of the weak points of stochastic models is that they require statistical event occurrences to follow precise probabilistic laws, while the synchronization and causality imposed in the system by clock/event constraints such as specified in CCSL actually disrespect these regular laws. As in the case of “schedulability by model-checking”, similarities and dissimilarities with Stochastic Timed Automa should be considered here (where they name “clocks” what we would call stopwatches).
  • The PhD thesis of Vincent Zhao should start in January 2016. This PhD is related to the activity with Esterel Technologies. The goal of the PhD is to make a bridge between system models, i.e., a set of components whose interaction semantics is usually informal, and the actual (heterogeneous) components that satisfy some known properties. By leveraging some of properties obtained on the component level, we hope to be able to conduct some execution, validation and verification activities at the system level. We also want to offer mechanisms to help the integration: verify that components satisfy system requirements, allow substitution of components and exploration of alternative costs with regards both of their functional or non-functional properties.
  • Deeper connections between CCSL and UTP, as both are used to provide deeper and more precise semantic meaning to CPS timed formalisms.
  • The study of new symbolic models based on open parameterized networks of synchronized automata (open pNets) will continue, using several directions: on one side, we want to extend our current work on behavioral equivalences, studying fundamental properties of various species of bisimulation, but also relating these with denotational and algebraic semantics, using a UTP approach. On the other side, we aim at experimental validation of the approach, and this requires the implementation of tools handling the model generation and the bisimulation; this will be used on non-trivial use-cases taken from existing bibliography. These activities will be strengthened by researcher visits on both sides, by Eric Madelaine at ECNU in July, and by Min Zhang and/or Huibiao Zhu in Sophia-Antipolis. Several internship subjects will also be proposed, and may lead to a PhD proposal later in the year.

In addition to these topics, new research directions were put up at the Rennes Workshop meeting, where a number of permanent staff from both sides were gathered in the same place and time. Some are linked to the extraction, execution and analysis of traces, considered as abstract behaviors at model level, and then leading to test suite for verification analysis at code level; in particular the joint use of symbolic execution and model-checking for the proper extraction of traces and tests was proposed as new direction topic

 

3.     Annual report 2016

     3.1.     Scientific progress – 2016

We continued our work on studying our Clock Constraint Specification Language (CCSL), both on the theoretical side, and on practical aspects. In the first direction we established its universal Turing-complete expressivity, by encoding Petri Nets with inhibitor arcs in its dynamics; this result is not so surprising as CCSL also allows the modeling of some kind of counter machines, and synchronized products. Still, we defined interesting subclasses with regularity and decidable complexity. We also study the use of proof assistant, rather than fully automatic solvers, to deal with the general case. On the more practical side we started some activities on the definition of a stochastic version of those constraints, mainly to deal with cyber-physical systems in a setting where environmental events and responses may be uncertain in time. We also started to consider links with security aspects (and more specifically the connections with real-time constraints). These two topics (stochastic CPS extensions and links in metamodeling between Real-Time and Security aspects) are respectively linked to the PhD thesis of two Chinese students (AN Dongdong and ZHAO Hui) currently studying at Inria Sophia-Antipolis under the supervision of Frédéric Mallet and Robert de Simone.
With the end of O. Kulankhina PhD work [Fase’16], we reached a milestone in our Formal MDE development for  component base synchronous/asynchronous specification and verification software. An important application of this approach to the GCM distributed component model is under revision for a journal. Several students from ECNU have contributed to this work, including Siqi Li and Yuanmin Zhu in 2016. This direction of research is now turning to more symbolic methods for the semantic definition and verification algorithms, aiming at a new approach, both formal and pragmatic, for analyzing the properties of the composition of concurrent processes [ScienceChina’16]. Preliminary results have been published using both a denotational semantic approach [PDP’16, UTP’16], and a behavioral (symbolic) semantics [FORTE’16]. Work on the implementation of the behavioral semantics is ongoing, with the  internship of QIN Xudong.

     3.2.Next year’s work program

In the context of An Dongdong PhD thesis (in its first year) we will consider extension to CCSL expressiveness including stochastic and probabilistic aspects. Currently, the logical clock constraints involve either asynchronous (timing inequalities) or synchronous (timing inclusion) between system activities represented as “pure events”. The way constraint solving works in practice, timing requirements on the system behavior shall constraint primary input
(event) clocks to occur into well-behaved time frames, thereby enforcing strict scheduling on them. In the context of Cyber-Physical Systems it is not so obvious to constraint external events (even when discretized through sensor sampling) the way one may control a digital cyber-task to start execution in the digital world. Therefore it becomes mandatory to specify and represent some amount of probabilistic uncertainty. This type of extensions has been
considered in most existing modeling contexts (from automata to Markov chains and processes, from Ordinary to Stochastic Differential Equations, and closer to our goals from Timed Automata to Stochastic Timed Automata.
Because our CCSL formalism holds well-understood connections to them (mostly Timed Automata) in the
“un-probabilistic” case, we can investigate whether the same extension patterns can be fruitful, and if not why (and how it can lead to other solutions). Prelimiary attempts in that direction have just been presented in a joint paper (ref.
6 below).
In the context of Hui Zhao PhD thesis (in its second year) we will consider the connections between modeling and metamodeling aspects (SysML/ MARTE and Araadia/ Capella, a formalism being currently deployed on a
large scale inside Thales operational divisions) regarding the combination of Real-Time and Security/dependability points of view. There is certainly a strong feedback from each on the other (if only to mention that they may conflict
as security adds latency to processing). Notions of mixed-criticality, and the timely variations of trust zones according to changing system states, are other examples of this. We want to put here the emphasis on proper and insightful modeling of these aspects, as a preamble to analysis and verification of joint temporal and security/safety conditions.
We want to illustrate these issus based on potential use cases in a subway intelligent system connecting several
subsystems (signaling and traffic regulation and collision avoidance and public information on train arrival delays…)
with secured wireless communications. This applicative domain was chosen because of former expertise of the PhD student.
Our joint work (between Eric Madelaine and Ludovic Henrio from France, professors Zhang Min, Zhu Huibiao and students from ECNU) on symbolic approaches to the composition of concurrent processes will continue both on the fundamental theory, looking for properties and for more effective algorithms for our open bisimulations (strong or weak); and on the implementation of these algorithms, with validation on non-trivial case-studies, typically on
analyzing the properties of existing generic distributed algorithms, or parallel skeletons. The middle term goal is to build a formal framework, but also an effective tool set, for the compositional analysis of such programs.

 

4.Annual report 2017

     4.1.Scientific progress – 2017

We continued our work on studying our Clock Constraint Specification Language (CCSL), both on the theoretical side, and on practical aspects. We took further two main directions:

a) Analysis and Verification: expressively, CCSL goes beyond the range of automatic verification techniques. Still, the existing interpretation in terms of communicating counter automata shows that combination of simple integer arithmetic and Boolean equations are most often sufficient to solve practical problems. This raised the question of connection with SMT solvers (which combine Boolean satisfiability with equational theories) is thus a natural one, and is the subject of progressive evaluation: defining proper subsets of CCSL, matching theories, etc. This line of research is mainly conducted by Frédéric Mallet and Min Zhang, on both sides of the team association. The topic was further debated during the specific FM4CPS workshop held prior to TASE 2017.

b) extension to stochastic and probabilistic frameworks: CCSL is modtsly concerned originally with deterministic discrete logical clocks, althoug many of its basic definitions could be applied more broadly. The extension to stochastic and probabilistic models can be considered in two ways: first, making the ocurrences of clock ticks subject to uncertainty; second, handle stochastic continuous (Markov chain) processes, and try to extract the logical clocks that may integrate these probabilities of tick occurrences to a discrete logical clock with explicit significance (like Worst-Case Reacton Time). We mainly followed the first direction, in joint work between Dehui Du and Frédéric Mallet. In the course of the long-term visit by Dongdong AN to Inria Sophia as part of a Chinese PhD exchange program, we are considering the second direction and their interactions.

Links in metamodeling between Real-Time and Security aspects [Vincent, Fred, Robert] (to be completed)
[Daian Yue, Vania Joloboff, Frederic Mallet]: Trace Runtime Analysis Platform for CPS (j’ai un resume en 2 pages, je vais raccourcir (;-)

Our joint work (between Eric Madelaine and Ludovic Henrio from France, professors Zhang Min, Deng Yuxin and students from ECNU) on symbolic approaches to the composition of concurrent processes has progressed mainly on the pratical side, with an implementation of a prototype algorithm computing the symbolic semantics (called Open Automata) of open systems, and validating the approach for encoding constructs of various formalisms. A paper has been submitted for publication.
As a particular set of use-cases, we have started using pNets to encode the
behavior of “Architecture Templates” of the BIP language, with the aim of proving generic properties of these constructs, and building full systems by combining such architectures, with proven guarantees.
As an asset for the continuation of this collaboration, Xudong Qin has been enrolled as a PhD student at ECNU, and we are in the process of setting a Cotutelle convention with UCA for him.
[Final FM4CPS workshop] We organized on Oct. 12th the final FM4CPS workshop, in Sophia-Antipolis. 5 of our chinese colleagues were participating, and 12 french researchers from INRIA and our local partners. 7 presentations have been given, the full program is available HERE.
[TASE’17 Co-organisation]
Last but not least, we have co-organised in Sophia-Antipolis the “Eleventh International Symposium on Theoretical Aspects of Software Engineering” (TASE’2017: http://tase2017.unice.fr/). Min ZHANG and Frederic Mallet were co-chairs, Eric Madelaine general chair. 19 papers were accepted (selection rates of full papers ~34%), together wth 3 highly reputable keynote speakers; exchanges have been very rich and interesting.
Formal achievements:
To enhance our collaboration, and give us more tools to make it successfaul in the upcoming years, we have been actively discussing formal links between our institutions.
In 2015 we signed a MoU between E.C.N.U.Software of Engineering institute and University of Nice.
In 2015 also, we became partner of the Ministery of education International Joint Lab on Trustworthy Software (IJLTS).
In 2016, we had the pleasure to have another MoU signed, between ECNU and INRIA.
More concretely, this partenership opens opportunities to bilateral projects between INRIA and IJLTS. We have applied to
one of these for the next year. It also sets up a framework for students exchanges:
– at master level:
In july 2017, we signed an agrement for a double master degree between ECNU and University of Nice, and in september 2017, 5 students from ECNU applied and were accepted in the Ubinet international master in Nice.
– at PhD level: we have one new co-advised PhD student, Xudong Qin, starting his PhD at ECNU on sept. 2017.
– at post-doc level: ECNU is offering post-docs positions with very attractive conditions to our PhD students.
Perspectives:
With the end of this associated team, we are now working on new collaboration artifacts.
– on INRIA side, we will both apply for the status of “International partner”, and search for enhancing our involvment
within the LIAMA.
– we have several project already submitted with IJLTS, with CNRS, ANR, and NSFC.