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

博文

模型检验(5)(100101)

已有 3689 次阅读 2010-1-1 14:23 |个人分类:学术导航|系统分类:科研笔记| 模型检验

模型检验(5)(100101)
闵应骅
    模型检验(model checking)自从1981年提出来以后,受到各种非议。至今28年过去了,才得到了学术界和工业界的广泛关注。这是很正常的。要求一个学术成果马上用于实际,很不现实。中国某些干部就这么急功近利。算法的设计验证包括三步:(1)需求规范;(2)建立可执行的系统模型;(3)开发可扩展的算法,一是去检验需求,二是当需求不能满足时进行诊断。
    需求规范可以用两种方式给定。一种是基于状态的需求,用转换系统指明系统的可观察行为;另一种是基于特性的需求,用说明性的方式。这些需求用一系列的时态逻辑公式表达。IEEE的PSL语言就用了这二者的组合。需求规范的无矛盾性和完全性仍然是一个问题。现在还缺乏某些外部需求的形式化,例如安全性(隐私),可重构性(不相互干扰的构造性),服务质量(抖动度)等。
    可执行的模型要求忠实性,即模型必须与被验证系统保持语义,而且必须是可检验的。这样,你验证的特性才能在实际系统中实现。为了避错和纠错,模型应该能从系统描述自动产生。对于硬件验证,此事从RTL描述出发,比较容易完成。而对于软件,可能只能在抽象级别上进行。扩展UML进行调度和资源管理无法提供严格的定时特性。而扩展硬件描述语言,像SystemC和TLM由于缺乏形式语义只能用于模拟。
    可扩展的验证方法对大系统不好做。一个解决办法是根据特定的语义范畴开发抽象技术,即在特定语义领域求解不动点方程。另一个解决办法是面对复杂性,用分而治之的途径。过去,特性被分成两部分:阶段-结论。现在,我们需要组合验证的理论,把验证组合起来,形成一个大的验证。
    计算机工程于其他自然科学一个巨大的不同就在于保证正确的验证的重要性。其他科学用建造理论来保证正确性和可预见性。我们需要建造复杂系统可靠模型的理论和方法。异构系统可能是同步的或异步的;不同的交互机制,如锁闭、监管、功能调用和消息传达;执行粒度不同,即硬件或软件。我们需要从基于自动机的组合中解放出来,考虑体系结构的组合,像协议、调度和总线。我们需要研究某些特定的特性类,例如无死锁、互操作。而不是去研究一般的安全特性。我们也需要研究特殊体系结构的验证技术。体系结构给定了部件间的交互机制。例如对环形或星形体系结构,对带抢先任务和固定优先级的实时系统,对时间触发的体系结构等。可以像测试定义可测试性一样,定义可验证性。
    总之,模型检验已经在硬件和软件设计验证中得到了应用,但是,还有许多问题有待研究。

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

上一篇:模型检验(4)(091231)
下一篇:模型检验(结束语)(100101)
收藏 IP: .*| 热度|

1 俞立

发表评论 评论 (1 个评论)

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

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

GMT+8, 2024-3-29 06:14

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部