基于算术表达式的MSVL柱面计算方法和系统

摘要

本发明公开了一种基于时序逻辑语言MSVL的柱面计算方法和系统，属计算机系统形式化建模与验证技术领域，本发明定义了多核并行程序语法和语义，描述一个或多个进程并发执行，构造柱面计算模型。将基本时序区间表达式扩展到算术表达式和时序表达式，描述能力增强，对进程控制更加准确；本发明对进程的解释包括对于进程执行体的解释和对于时序区间表达式的解释，进程的时序区间表达式控制进程执行体的执行效果持续的时序区间粒度；利用MSVL并行投影方法参与多个进程的并行解释，控制各个并行程序在各进程一次解释结束状态点上通信。本发明不仅能够描述共享对象，也能够以便捷可控的方式编写多核并行程序，对其进行仿真，建模和验证。