新书推介：《语义网技术体系》
作者：瞿裕忠，胡伟，程龚
   XML论坛     W3CHINA.ORG讨论区     计算机科学论坛     SOAChina论坛     Blog     开放翻译计划     新浪微博  
 
  • 首页
  • 登录
  • 注册
  • 软件下载
  • 资料下载
  • 核心成员
  • 帮助
    		•   Add to Google

    >> 软件工程、需求工程、系统工程，UML、MDA、模型驱动开发，面向对象软件工程、面向目标软件成功、面向场景的设计、敏捷
    [返回] 计算机科学论坛 → 计算机技术与应用 → 『 软件工程论坛 』 → 弱弱的问一下，什么是model checking ◇查看新帖 ◇ 用户列表 ◇

      发表一个新主题  发表一个新投票  回复主题  (订阅本版) 您是本帖的第 20403 个阅读者浏览上一篇主题  刷新本主题   树形显示贴子　浏览下一篇主题
     * 贴子主题： 弱弱的问一下，什么是model checking 举报  打印  推荐  IE收藏夹 
       本主题类别:     
     cqyanbo 帅哥哟，离线，有人找我吗？
      
      
      等级：大一新生
      文章：1
      积分：55
      门派：XML.ORG.CN
      注册：2007/12/4

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给cqyanbo发送一个短消息 把cqyanbo加入好友 查看cqyanbo的个人资料 搜索cqyanbo在『 软件工程论坛 』 的所有贴子 引用回复这个贴子 回复这个贴子 查看cqyanbo的博客楼主
    发贴心情 弱弱的问一下，什么是model checking

    有劳各位了！很急啊！

       收藏   分享  
    顶(0)
      




    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2007/12/4 11:22:00
     
     wcdxyl 帅哥哟，离线，有人找我吗？天秤座1980-10-9
      
      
      威望：4
      等级：大四(每天看1小时莱昂氏)(版主)
      文章：158
      积分：1145
      门派：IEEE.ORG.CN
      注册：2006/3/14

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给wcdxyl发送一个短消息 把wcdxyl加入好友 查看wcdxyl的个人资料 搜索wcdxyl在『 软件工程论坛 』 的所有贴子 引用回复这个贴子 回复这个贴子 查看wcdxyl的博客第2楼
    发贴心情 
    模型检验（Model Checking）,　具体做法是采用一种形式语言描述系统的规范说明，构造一种算法来遍历根据系统规格说明设计的实现模型，确认实现模型是否满足系统的规范说明。

    ----------------------------------------------
    主页:http://wcdxyl.blogchina.com
    MSN:wcdxyl@163.com

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2007/12/18 10:15:00
     
     月光 帅哥哟，离线，有人找我吗？金牛座1990-5-11
      
      
      等级：大一新生
      文章：6
      积分：79
      门派：XML.ORG.CN
      注册：2010/10/15

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给月光发送一个短消息 把月光加入好友 查看月光的个人资料 搜索月光在『 软件工程论坛 』 的所有贴子 点击这里发送电邮给月光 引用回复这个贴子 回复这个贴子 查看月光的博客第3楼
    发贴心情 
    解释的听恰当。

    ----------------------------------------------
    互换一个苹果，双方仍各有一个苹果。互换一个想法、心得。双方各有两个想法、心得。如果你们的想法一样，那你更该高兴。这表示英雄所见略同！

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2010/10/18 21:32:00
     
     bailong3301 帅哥哟，离线，有人找我吗？水瓶座1986-2-10
      
      
      等级：大一新生
      文章：1
      积分：54
      门派：W3CHINA.ORG
      注册：2011/8/1

    姓名：(无权查看)
    城市：(无权查看)
    院校：(无权查看)
    给bailong3301发送一个短消息 把bailong3301加入好友 查看bailong3301的个人资料 搜索bailong3301在『 软件工程论坛 』 的所有贴子 点击这里发送电邮给bailong3301  引用回复这个贴子 回复这个贴子 查看bailong3301的博客第4楼
    发贴心情 
    据我所知，模型检验是把待检验的程序建模成一个状态转换系统P，待验证的安全属性建模为有限状态机F，然后检查P能够达到的任何一个状态是否是安全属性F的非~F的接受状态，如果P能到达这样一个状态，则说P违反了安全属性F；否则，说P遵守了安全属性F。

    ----------------------------------------------
    我喜欢这些星星，它们沉默不言，它们就在那儿。

    点击查看用户来源及管理<br>发贴IP：*.*.*.* 2011/8/1 17:08:00
     
     GoogleAdSense水瓶座1986-2-10
      
      
      等级：大一新生
      文章：1
      积分：50
      门派：无门无派
      院校：未填写
      注册：2007-01-01
    给Google AdSense发送一个短消息 把Google AdSense加入好友 查看Google AdSense的个人资料 搜索Google AdSense在『 软件工程论坛 』 的所有贴子 点击这里发送电邮给Google AdSense  访问Google AdSense的主页 引用回复这个贴子 回复这个贴子 查看Google AdSense的博客广告
    2024/5/18 18:14:47

    本主题贴数4，分页： [1]

    管理选项： 修改tag | 锁定 | 解锁 | 提升 | 删除 | 移动 | 固顶 | 总固顶 | 奖励 | 惩罚 | 发布公告
    W3C Contributing Supporter! W 3 C h i n a ( since 2003 ) 旗 下 站 点
    苏ICP备05006046号《全国人大常委会关于维护互联网安全的决定》《计算机信息网络国际联网安全保护管理办法》
    		 3,273.438ms