标签:
形式化方法的基本概念:
一阶线性时态逻辑:
计算树逻辑
模型检测
Z语言概述:
Z语言为系统建立基于状态的模型。模型的三个主要组成部分是输入、输出和状态,它们均有相应的数学概念来描述。
Z语言表示:
Petri网定义:
任何事物都可抽象为两类元素:状态和事件。在某种状态下,相应的事件便可发生。然后状态发生变化,于是又有一些新的事件可以发生。如此反复不已。
(1) Petri网结构
(2) 前集合后集
(3) 顺序关系
(4) 并发关系
(5) 冲突关系
(6) 混惑关系
标签:
原文地址:http://www.cnblogs.com/apak/p/4261963.html