In the field of model-based systems engineering, there is an increasing demand for
the application of formal methods. However, this requires expertise in formal methods,
which cannot be expected from systems engineers. While several attempts have been
made to bridge this gap, there are still open questions. (1) With the trend shifting
towards ontological languages, systems are modeled as classes of 4D occurrences, rather
than a 3D system evolving with time, which hinders the application of state-of-the-art
model checking algorithms. (2) Ontological reasoning cannot handle the state space
explosion problem, and can even make it harder for verifiers to operate efficiently.
(3) When operationalizing ontological languages, we need to validate the conformance
of the two semantics, even in the presence of optimizations. (4) On top of all, these
challenges must be solved for every new engineering language, version, or variant.
In this paper, we propose a new approach to address the aforementioned challenges.
To validate its feasibility, we present a prototype tool and evaluate it on a SysML
model.