Section: New Results

Behavioral semantics and equivalence notions for Open Systems

Participants : Eric Madelaine, Tengfei Li, Zechen Hou.

Model-Based Design naturally implies model transformations. To be proven correct, they require equivalence of “Open” terms, in which some individual component models may be omitted. Such models take into account various kind of data parameters, including, but not limited to, time. The middle term goal is to build a formal framework, but also an effective tool set, for the compositional analysis of such programs. Following last year results we have published an experience paper [23] showing the applicability of this approach to show properties of a piece of the control software of a nano-satellite, specified using BIP architectures. Our work now turns on designing specific symbolic algorithms for model checking and equivalence checking (bisimulation) of such open systems, and also, as a specific application domain, to formalize the encoding of BIP architecture, extended with data constraints, into open pNets, aiming at a full approach for compositional verification of such systems. This work is done in collaboration with researchers from ENS Lyon and Inria Lille, and from ECNU Shanghai [23].