Keywords

The semantic heterogeneity in the formal development of complex systems has many different, yet related forms, e.g.:

  • Abstraction — as our models move from the abstract to the concrete — from the what to the how — there is usually a need for a mix of non-operational and operational semantics [1].

  • Composition — systems are composed with other systems, and such compositions cannot reasonably be expected to be done within a single homogeneous semantic framework. As the number of possible ways in which we may wish to compose different types of systems is increasing, so too increases the importance of being able to model and manage the heterogeneity [2].

  • Separation of concerns — complex systems involve many different aspects (data, behavior, safety, performance, security, etc.) which are usually handled in a separated timely manner to provide scalability according to their size and complexity. This leads to heterogeneous models where some parts are explicit and other implicit according the related concern. This can be related to composition where each model does not correspond to a part of the system but to a concern in the system development.

  • Reasoning — the language in which one models a system is not usually the same language in which one reasons about the relationship between models, and the correctness of one model with respect to another [3].

  • Implicit versus explicit — in every model, the semantics of the language used to establish the meaning of the model are implicit. In order to understand the meaning of any model one must implicitly understand the semantics of the language in which it is expressed. Similarly, in order to validate the model one needs to establish a relationship between the model and the implicit semantics of the real-world domain in which the model has relevance. Each of these 2 implicit semantics must be made explicit and combined in order to achieve a coherent integration. However, each of these implicit semantics has a very different nature. This type of heterogeneity is a major challenge [4].

A previous thematic track — addressing the same issues — introduced some of the first research results concerned with techniques that can be used to manage the heterogeneous nature of formal modeling [5]. In Modeling and Verifying an Evolving Distributed Control System Using an Event-based Approach [6] the techniques were concerned with component-based system engineering where it is necessary to be able to compose components whose behavior was expressed using different modeling languages. In Requirements driven Data Warehouse Design: We can go further [7] the techniques were based on the use of ontological reasoning mechanisms can used to automatically construct a set of requirements that are coherent and non-conflictual, even when expressed in a variety of modeling languages. Finally, the paper On Implicit and Explicit Semantics: Integration issues in proof-based development of systems [8], the techniques were founded on the principle that re-usable domain knowledge should be modelled explicitly using formal ontologies.

In this year’s thematic track, we emphasis the heterogeneous nature of complex systems engineering and the need for automated tool support for supporting the techniques that manage the heterogeneity in a formal way. We note that the accepted papers are concerned with theoretical advances, together with pragmatic application of these advances in real-world industrial case studies.

In On the Use of Domain and System Knowledge Modeling in Goal-Based Event-B Specifications [9], we see an example of semantic heterogeneity due to the application of several different formalisms in a single system development. The paper combines Goal Oriented Requirement Engineering [10] and the refinement-based Event-B formal method [11] in order to improve the handling of requirements in a formal development. The authors rely on an ontology in order to model part of the requirements usually expressed in natural language [12]. Then the content of the ontology is translated to Event B contexts. The proposal is illustrated with the Landing Gear case study proposed in the ABZ 2014 conference [13].

In Strengthening MDE and Formal Design Models by references to Domain Ontologies. A Model Annotation Based Approach [14], we see how we can enrich design models involved in critical systems development in order to integrate heterogeneous domain constraints. The paper proposes to integrate these domain constraints by enhancing design models with references to domain knowledge. The domain knowledge is modelled by means of ontologies and references are built by annotation mechanism linking design models to domains constraints. The key to the technique is the methodological combination of an MDE approach [15] using Eclipse together with a refinement and proof formal process using Event-B [11].

In Towards Functional Requirements Analytics [16], the authors present the design of warehouses for Functional Requirements [17]. The authors advocate the use of a pivot model as there can be a huge heterogeneity between the Functional Requirements stakeholders. Then, they apply the usual warehouse methods based on ETL (Extract, Transform, Load) [18]. The proposal relies on the implementation of a proof of concept based on the Oracle RDBMS using SparQL and the QB4OLAP W3C proposal. This proof of concept is based upon the common Course Management System example provided by the Van Der Bilt university.

In Heterogeneous Semantics and Unifying Theories [19], the paper illustrates the use of the Unifying Theory of Programming [20] to combine heterogeneous semantics. The paper reports on two core use cases: the introduction of references in the action part of Hoare logic based on separation logic [21]; and the introduction of the theory of design in CSP [22].