From Transpilers to Semantic Libraries: Formal Verification With Pluggable Semantics
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.
Mon 23 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | |||
14:00 30mTalk | Experimenting low code with SDL and BPMN SAM Conference Emmanuel Gaudin PragmaDev | ||
14:30 30mTalk | A Multi-Platform Specification Language and Dataset for the Analysis of DevOps Pipelines SAM Conference | ||
15:00 30mTalk | From Transpilers to Semantic Libraries: Formal Verification With Pluggable Semantics SAM Conference Ármin Zavada Budapest University of Technology and Economics, Kristóf Marussy Budapest University of Technology and Economics, Vince Molnár Budapest University of Technology and Economics DOI |