闵应骅的博客分享 http://blog.sciencenet.cn/u/ymin 一位IEEE终身Fellow对信息科学及其发展的看法

博文

模型检验(2)(091231)

已有 5304 次阅读 2009-12-30 17:17 |个人分类:学术导航|系统分类:科研笔记| 时态逻辑

模型检验(2)(091231)
闵应骅
    程序正确性的形式验证依靠数学逻辑的使用。程序是一个很好定义了的、可能很复杂、直观上不好理解的行为。而数学逻辑能精确地描述这些行为。过去,人们倾向于正确性的形式证明。而模型检验回避了这种证明。在上世纪60年代,流行的是佛洛伊德-霍尔式的演绎验证。这种办法像手动证明一样,使用公理和推论规则,比较困难,而且要求人的独创性。一个很短的程序也许需要很长的一个证明。
    不搞程序正确性证明,可以使用时态逻辑,一种按时间描述逻辑值变化的形式化。如果一个程序可以用时态逻辑来指定,那它就可以用有限自动机来实现。模型检验就是去检验一个有限状态图是否是一个时态逻辑规范的一个模型。
    对于正在运行的并发程序,它们一般是非确定性的,像硬件电路、微处理器、操作系统、银行网络、通信协议、汽车电子及近代医学设备。时态逻辑所用的基本算子是F(有时),G(总是),X(下一次),U(直到)。现在叫线性时间逻辑(LTL)。
    另一种常用的逻辑是计算树逻辑(CTL)。它的基本时态是A(对所有以后的交易),E(对某些以后的交易),跟随着F,G,X,U之一。复合公式是线性时间逻辑子公式的嵌套和组合。例如AFp(以后,p终将成立,因此是必然的。)EFp(以后,p最后可能成立。)如图1所示。
    时态逻辑公式可以在给定的有限状态图上加以解释。所以又称为克里普克(kripke)结构。M包含一个状态集S,一个完全的二进制转换关系R ⊆ S × S,和一个状态标签L,其原子事实为真。用M, s0 |= f 表示“在结构M中,于状态s0,f为真。”或者简写为M |= f.例如,M, s0 |= AFp 当且仅当对在M中的所有通路 x = s0, s1, s2, . . .我们有对任何i >=0, P ∈ L(si).    当我们写规范的时候,我们只写AFp,断言公式p是必然的。一个线性时间逻辑公式h意味着在整个结构皆为真,即Ah。在线性时间逻辑中,
G¬(C1 ∧ C2)表明进程C1和C2总是互相排斥的。而在计算树逻辑中则写成AG¬(C1 ∧ C2)。AG(T1 ⇒ AFC1)意味着只要进程1进入它的尝试区域T1,它总是进入它的关键段C1。AGEFstart表示系统总是可以重新启动的。这在线性时间逻辑中是无法表示的。而CTL*中的EGFsend则表明存在一个公平的行为,使得send条件可以重复出现。
    这些逻辑已经在工业界得到广泛应用,包括基于CTL的IBM Sugar,基于LTL的Intel For-Spec,和IEEE 1850标准所用的PSL用了CTL*。
    还有命题演算,非常一般的TL。它允许时态正确性的不动点递归定义。例如EFp = p ∨ EX(EFp)。时态正确性的不动点特征在模型检验的算法和工具中都很有用。

https://wap.sciencenet.cn/blog-290937-282651.html

上一篇:模型检验(1)(091230)
下一篇:模型检验(3)(091231)
收藏 IP: .*| 热度|

0

发表评论 评论 (0 个评论)

数据加载中...
扫一扫,分享此博文

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-3-29 01:02

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部