Benoît Combemale

Gurvan Le Guernic, Benoit Combemale, José A. Galindo

Many project-specific languages, including in particular filtering languages, are defined using non-formal specifications written in natural languages. This leads to ambiguities and errors in the specification of those languages. This paper reports on an industrial experiment on using a tool-supported language specification framework (K) for the formal specification of the syntax and semantics of a filtering language having a complexity similar to those of real-life projects. This experimentation aims at estimating, in a specific industrial setting, the difficulty and benefits of formally specifying a packet filtering language using a tool-supported formal approach.

Benoit Combemale, Julien De Antoni, Robert B. France et al.

The first edition of GEMOC workshop was co-located with the MODELS 2013 conference in Miami, FL, USA. The workshop provided an open forum for sharing experiences, problems and solutions related to the challenges of using of multiple modeling languages in the development of complex software based systems. During the workshop, concrete language composition artifacts, approaches, and mechanisms were presented and discussed, ideas and opinions exchanged, and constructive feedback provided to authors of accepted papers. A major objective was to encourage collaborations and to start building a community that focused on providing solutions that support what we refer to as the globalization of domain-specific modeling languages, that is, support coordinated use of multiple languages throughout the development of complex systems. This report summarizes the presentations and discussions that took place in the first GEMOC 2013 workshop.

Mounira Kezadri Hamiaz, Marc Pantel, Benoît Combemale et al.

Composition technologies improve reuse in the development of large-scale complex systems. Safety critical systems require intensive validation and verification activities. These activities should be compositional in order to reduce the amount of residual verification activities that must be conducted on the composite in addition to the ones conducted on each components. In order to ensure the correctness of compositional verification and assess the minimality of the residual verification, the contribution proposes to use formal specification and verification at the composition operator level. A first experiment was conducted in [15] using proof assistants to formalize the generic composition technology ISC and prove that type checking was compositional. This contribution extends our early work to handle full model conformance and study the mandatory residual verification. It shows that ISC operators are not fully compositional with respect to conformance and provides the minimal preconditions on the operators mandatory to ensure compositional conformance. The appropriate operators from ISC (especially bind) have been implemented in the COQ4MDE framework that provides a full implementation of MOF in the COQ proof assistant. Expected properties, respectively residual verification, are expressed as post, respectfully pre, conditions for the composition operators. The correctness of the compositional verification is proven in COQ.