P-GRADE环境下形式验证与调试方法的集成

### P-GRADE环境下形式验证与调试方法的集成 #### 1. P-GRADE与DIWIDE简介 P-GRADE是一个用于在各种平台上开发和执行并行程序的集成编程环境，它由多个软件工具组成，可辅助软件开发的不同阶段，用于创建、执行、测试和调整并行应用程序。在P-GRADE中，可以使用GRED图形编辑器根据GRAPNEL语言的语法和语义来构建并行程序。GRAPNEL是一种混合编程语言，它使用图形和文本表示来描述整个并行应用程序。 在P-GRADE环境中，DIWIDE调试器应用了宏步（macrostep）技术，允许用户在各种定时条件下测试应用程序。宏步的思想基于集体断点的概念，集体断点放置在每个GRAPNEL进程的进程间通信原语上。两个连续集体断点之间执行的代码区域集合称为一个宏步。假设通信指令之间的顺序程序部分已经过测试，我们可以将每个顺序代码区域视为一个原子操作。这样，并行程序的系统调试就需要通过纯宏步来调试并行程序。 并行程序的宏步执行模式定义如下：在每个宏步中，程序运行直到命中一个集体断点，因此宏步的边界由一系列全局断点集定义，并行程序的连续一致全局状态会自动生成。在重放时，任务的进度由存储的集体断点控制，程序会像执行阶段一样再次自动按宏步执行。 执行路径是一个图，其节点表示宏步的结束（即一致全局状态），有向弧表示可能的宏步（即连续全局状态之间的可能状态转换）。执行树是执行路径的推广，假设当前程序的不确定性源于通配符消息传递通信，它可以包含并行程序的所有可能执行路径。 顺序程序的行为可以用时间逻辑（TL）语言表达的运行时断言来描述，这是提高代码可靠性以及开发者对程序正确行为信心的有效方法。在扩展P-GRADE的调试能力时，除了使用时间逻辑断言，我们的主要目标是支持以下机制： - 用户使用时间逻辑规范指定GRAPNEL应用程序的正确性属性（即预期的程序行为），并且该应用程序成功编译后，GRP2cPN工具会生成程序的有色Petri网模型。 - DIWIDE分布式调试器与TLC引擎合作，逐宏步将规范与观察到的程序行为进行比较，同时GRSIM模拟器将状态空间的遍历导向可疑情况。 - 如果检测到错误情况，用户可以通过GUI检查应用程序的全局状态或各个进程的状态。 - 根据情况，用户可以使用GRED编辑器修复编程错误，或者重放整个应用程序以更接近检测到的错误情况的根源。 通过这种方式，两个独立的子系统在宏步模式下支持检测错误。一方面，TLC引擎及其相关模块能够处理程序实际执行期间的过去和当前程序状态；另一方面，基于有色Petri网的建模和仿真可以展望未来，自动将实际执行导向检测到的错误情况，而无需用户交互。 #### 2. 有色Petri网与发生图 有色Petri网（CPN）允许系统设计师和分析师将直接处理实际系统的困难任务转移到更易于处理且成本较低的计算机化建模、仿真和分析中。CP网提供了一种有效的动态建模范式和一种带有相关计算机语言语句的图形结构。CP网的主要组件包括数据实体、位置、标记、转换、弧和保护，但有效的CPN建模需要能够将网络分布在多个分层页面上。 我们的实验GRSIM系统的核心是Design/CPN工具集，它配备了多种功能，如仿真和分析能力，以及一种类似C的标准化元语言（CPN/ML），用于定义转换的保护、复合令牌等。它提供了两种用于互连不同页面上的网络结构的机制：替换转换和融合位置。为了在不失去整体视图的情况下为模型添加细节，一个（替换）转换可以关联一个单独的CP网结构页面，称为子页面。包含该转换的页面称为超级页面。连接到子页面上替换转换的位置称为端口，它将在超级页面上显示为插座。这两个位置组成一个功能实体。 给定CPN模型的发生图（OCC图）是一个有向图，其中每个节点表示一种可能的令牌分布（即标记），每个弧表示两个连续令牌分布之间的可能状态转换。 #### 3. 从GRAPNEL到CPN的转换步骤 P-GRADE中采用的编程模型基于消息传递范式。程序员可以定义独立并行执行计算的进程，这些进程仅通过相互发送和接收消息进行交互。通信操作总是通过属于进程并由通道连接的通信端口进行。 在GRAPNEL程序中，有三个不同的分层设计级别： - 应用程序级别：用于定义进程、端口和确保进程间通信的通道。 - 进程级别：应用类似控制流图的技术来定义进程的内部结构，包括输入、输出和替代输入等通信操作。 - 文本级别：为进程内的顺序元素、条件或循环表达式或端口协议定义C代码。 在自动生成与GRAPNEL应用程序等效的Petri网模型时，主要挑战之一是将网络以分层模式放置在页面上并将这些组件连接在一起。GRP2cPN在生成过程中保留了GRAPNEL的逻辑层次结构，应用程序级别在最高级别的超级页面（主页面）上描述，其中每个进程由一个与“ReadyToRun”（在此处放置一个令牌允许进程执行）和“Terminated”（如果此处出现一个令牌，则进程执行完成）融合位置相连的替换转换表示。因此，一个进程在一个子页面上表示，该子页面包含上述两个融合位置。 在应用程序级别，GRAPNEL输入类型同步端口转换为三个融合位置： - “SenderReady”（SR）：此位置上的一个令牌表示伙伴进程已准备好进行通信。 - “ReceiverReady”（RR）：执行在通信输入操作上挂起，等待伙伴。 - “Data”（D）：数据到达的位置。 GRAPNEL输出类型端口转换为CPN的另外三个融合位置： - “SenderReady”（SR