Semantic heterogeneity in the formal development of complex systems: An introduction

Nowadays, the formal development of complex systems (including hardware and/or software) implies the writing, synthesis and analysis of many kind of models on which properties are expressed and then formally verified. These models first provide separation of concerns, but also the appropriate level of abstraction to ease the formal verification. However, the building of such heterogeneous models can introduce gaps and information loss between the various models as elements that are explicit in the whole integrated models are only explicit in some concerns and implicit in others. The whole correct development should thus only be conducted on the whole integrated model whereas separate development is mandatory for scalability of system development. More precisely, parts of these systems can be defined within contexts, imported and/or instantiated. Such contexts usually represent the implicit elements and associated semantics for these systems. Several relevant properties are defined on these implicit parts according to the formal technique being used. When considering these properties in their context with the associated explicit semantics, these properties may be not provable or even can be satisfiable in the limited explicit semantics whereas they would be unsatisfiable in the whole semantics including the implicit part. Therefore, the development activities need to be revisited in order to facilitate handling of both the explicit and implicit semantics.