Implementations of high-level modeling languages that integrate high-performance verifiers

自然、符号和网络物理系统的建模和验证技术正变得越来越重要。这项研究的目的是证明基于数学概念的高级建模语言的可行性，这些概念的普遍性远远超出了计算机科学的范畴。为了实现这一目标，我们构建了两个公开可用的语言实现，它们集成了运行时系统和验证器。一种是图重写语言LMNtal的实现，现已演化为具有超图重写能力的并行模型检查器；另一种是混合约束语言HydLa的实现，它已演化为具有不确定性的混合系统的非确定性符号执行系统。

Modeling and verification technologies of natural, symbolic and cyber-physical systems are becoming increasingly important. The aim of this research was to demonstrate the viability of high-level modeling languages based on mathematical notions such as graphs, sets, equations and inequations whose generality goes far beyond Computer Science. To achieve this goal, we constructed two publicly available language implementations that integrate runtime systems and verifiers. One of them is an implementation of the graph rewriting language LMNtal, which has now evolved into a parallel model checker with hypergraph rewriting capabilities; the other is an implementation of the hybrid constraint language HydLa, which has evolved into a non-deterministic symbolic execution system for hybrid systems with uncertainties.