混合系统(Hybrid System)能够有效地捕获嵌入式系统中离散和连续成分之间的动态交互作用。它架起了计算机科学、控制工程和数学之间的桥梁,为嵌入式系统提供了形式化的分析和合成方法。形式化验证是混合系统的一个重要研究方向。它可以检验混合系统是否在任何环境下都能安全运行,对于保证系统的安全性起着至关重要的作用。可达性分析和可达集的计算是混合系统形式化验证的基础。水平集方法被用于表示可达集和追踪可达集边界的演化。因此,我们采用水平集方法作为合成算法的数值计算方法,而基于SUNDIALS(Suite of Nonlinear and Differential/Algebraic Equation Solvers)的并行水平集内核能够提供更高的精确度和更快的运算速度。基于模型整合计算(Model-Integrated Computing, MIC)的工作平台ReachLab允许用户搭建图形化的算法模型,并通过算法翻译器,自动产生调用数值计算工具的可执行代码。我们为ReachLab设计算法翻译器,根据算法模型产生程序代码,并在多核多核计算平台上实施对动力系统进行可达性分析,并对计算结果进行展示。本文的主要研究内容如下:1.通过对算法模型进行分析,提取有关信息,并创建输入图。模型由不同的组件互连起来的,隐式地用图结构表示。2.引入基于Sundials的并行水平集内核,提高计算速度和精度。3.使用语义映射,对分析得到的输入图重组,并结合并行计算内核,自动生成可运行的并行计算代码。