公开(公告)号：CN105260295B

公开(公告)日：2018-09-25

申请号：CN201510581206.2

申请日：2015-09-14

Applicant: 桂林电子科技大学

Inventor： 钱俊彦 ,  甘鹏程 ,  郭云川 ,  赵岭忠 ,  古天龙

IPC: G06F11/36 ,  G06F21/57

Abstract: 本发明公开一种时间多栈下推网络的静态转换方法，首先，为了描述实时系统中并发递归机制，以及线程之间的交互，在MPDN的基础上引入时钟，提出TMPDN模型，并给出其语法及操作语义。其次，利用时钟域等价的优化技术，通过静态转换方法，将连续时间的TMPDN模型转换成离散的MPDN模型。本发明能够实现同时实现实时并发系统的实时性和并发性的描述，并能为实时并发程序的形式化验证提供保证。

公开(公告)号：CN105260295A

公开(公告)日：2016-01-20

申请号：CN201510581206.2

申请日：2015-09-14

Applicant: 桂林电子科技大学

Inventor： 钱俊彦 ,  甘鹏程 ,  郭云川 ,  赵岭忠 ,  古天龙

IPC: G06F11/36 ,  G06F21/57

Abstract: 本发明公开一种时间多栈下推网络的静态转换方法，首先，为了描述实时系统中并发递归机制，以及线程之间的交互，在MPDN的基础上引入时钟，提出TMPDN模型，并给出其语法及操作语义。其次，利用时钟域等价的优化技术，通过静态转换方法，将连续时间的TMPDN模型转换成离散的MPDN模型。本发明能够实现同时实现实时并发系统的实时性和并发性的描述，并能为实时并发程序的形式化验证提供保证。

公开(公告)号：CN105260296B

公开(公告)日：2018-08-14

申请号：CN201510581423.1

申请日：2015-09-14

Applicant: 桂林电子科技大学

Inventor： 钱俊彦 ,  甘鹏程 ,  郭云川 ,  赵岭忠 ,  古天龙

IPC: G06F11/36

Abstract: 本发明公开一种时间多栈下推网络的动态转换方法，首先，在MPDN的基础上引入时钟，提出TMPDN模型，并给出其语法及操作语义；其次，利用时钟域等价的优化技术，通过动态转换方法，将连续时间的TMPDN模型转换成离散的多栈下推网络模型。本发明能够实现同时实现实时并发系统的实时性和并发性的描述，并能为实时并发程序的形式化验证提供保证。

公开(公告)号：CN105260296A

公开(公告)日：2016-01-20

申请号：CN201510581423.1

申请日：2015-09-14

Applicant: 桂林电子科技大学

Inventor： 钱俊彦 ,  甘鹏程 ,  郭云川 ,  赵岭忠 ,  古天龙

IPC: G06F11/36

Abstract: 本发明公开一种时间多栈下推网络的动态转换方法，首先，在MPDN的基础上引入时钟，提出TMPDN模型，并给出其语法及操作语义；其次，利用时钟域等价的优化技术，通过动态转换方法，将连续时间的TMPDN模型转换成离散的多栈下推网络模型。本发明能够实现同时实现实时并发系统的实时性和并发性的描述，并能为实时并发程序的形式化验证提供保证。