Handling Heterogeneity in Formal Developments of Hardware and Software Systems

International audienceNowadays, the formal development of hardware and/or software systems implies the design of several models on which properties are expressed and then formally verified. Moreover, these models may be expressed in different modeling languages~\cite{losl} and semantics. As a consequence, this development process leads to heterogeneous developments. Heterogeneity may appear in two different forms. The first one is related to the large variety of formal development techniques and to the semantics and proof systems carried out by these techniques. Several formal descriptions may be associated to a given system with different semantics. The second type of heterogeneity results from the modeling domain~\cite{dines1,dines2,dines3} chosen for formalizing the described system. Usually, this domain is not explicitly described nor formalized. Most of the knowledge related to this domain is hardly encoded by the formal system description. The last decade has made use of ontologies~\cite{Gruber93} as an explicit formalization of such modeling domains. Expressing, in formal models, references to ontological concepts contribute to reduce such a heterogeneity. It also allows developers to address specific properties related to interoperable, adaptive, reconfigurable and plastic systems