登入帳戶　 |　訂單查詢　 |　購物車/收銀台(0)　|　在線留言板　 |　付款方式　 |　聯絡我們　 |　運費計算　 |　幫助中心　|　 加入書簽
	全部範圍 - 圖書 - 　- 中文簡體書(大陸書) - 　- 英文書（原版） - - 音碟 - 　- 音樂 - 　- 影視 - - 雜誌 - 全文 精確	會員登入   新用戶註冊

HOME新書上架暢銷書架好書推介特價區會員書架精選月讀2023年度TOP分類閱讀雜誌

香港／國際用戶

最新/最熱/最齊全的簡體書網

品種：超過100萬種書，正品正价，放心網購，悭钱省心

送貨：速遞 / 物流，時效：出貨後2-4日

新書推薦： 《 根源、制度和秩序：从老子到黄老学（王中江著作系列） 》 售價：NT$ 550.0 《 索恩丛书·北宋政治与保守主义：司马光的从政与思想（1019~1086） 》 售價：NT$ 345.0 《 掌故家的心事 》 售價：NT$ 390.0 《 农为邦本——农业历史与传统中国 》 售價：NT$ 340.0 《 小麦文明：“黄金石油”争夺战 》 售價：NT$ 445.0 《 悬壶杂记全集：老中医多年临证经验总结（套装3册） 中医医案诊疗思路和处方药应用 》 售價：NT$ 614.0 《 无法忍受谎言的人：一个调查记者的三十年 》 售價：NT$ 290.0 《 战争社会学专论 》 售價：NT$ 540.0

編輯推薦： *全面介绍模型检测原理与与实践方法。 *对模型检测领域的核心问题进行了清晰的阐述。 內容簡介： 模型检测是一种用于自动验证有限状态并发系统的技术，与基于模拟、测试和演绎推理的传统技术相比，具有许多方面的优势。本书共分18章，涵盖的主要内容包括模型检测的基本知识、模态逻辑、符号化技术、SATSolver、限界模型检测、自动机上的模型检测、抽象解释、程序分析、实时系统验证，同时介绍NuSMV和UPPAAL两个流行的模型检测器。 關於作者： Edmund M.Clarke教授，美国卡内基 ? 梅隆大学计算机科学系教授，并且是ACM和IEEE会士。他在软硬件验证、自动定理证明、形式方法等方面享有崇高的国际声誉，2007年获得ACM图灵奖。 吴尽昭，广西大学副校长，长期从事高效能高可信计算与推理理论与工具的研究和开发，研究领域涉及符号计算、自动推理、形式化方法及其交叉、融合与应用；在国内外学术刊物和国际会议论文集上发表研究论文107篇，出版专著3部，获得软件著作权6项，申请专利3项；近年来承担国家自然科学基金、863、973子课题等国家、省部级科研项目10余项。 目錄： 目录 第1章绪论1 1.1形式化方法的需求1 1.2硬件与软件验证1 1.3模型检测的流程3 1.4时序逻辑与模型检测3 1.5符号算法4 1.6偏序约简6 1.7缓解状态爆炸问题的其他方法7 第2章系统建模8 2.1并发系统建模8 2.2并发系统11 2.3程序翻译的实例16 第3章时序逻辑18 3.1计算树逻辑CTL*18 3.2CTL和LTL逻辑20 3.3公正性22 第4章模型检测24 4.1CTL模型检测24 4.2基于tableau结构的LTL模型检测29 4.3CTL*模型检测33 第5章二叉判定图36 5.1布尔公式的表示方法36 5.2Kripke结构的表示方法40 第6章符号模型检测42 6.1不动点表示42 6.2CTL符号模型检测45 6.3符号模型检测中的公正性48 6.4反例和诊断信息50 6.5一个ALU的例子52 6.6关系积的计算54 6.7符号化的LTL模型检测61 第7章基于? 演算的模型检测68 7.1简介68 7.2命题? 演算68 7.3求不动点公式的值71 7.4用OBDD表示? 演算公式74 7.5将CTL公式转化为? 演算75 7.6复杂度问题76 第8章实践中的模型检测77 8.1SMV模型检测器77 8.2一个实际的例子80 第9章模型检测和自动机理论85 9.1有限字与无限字上的自动机85 9.2使用自动机进行模型检测86 9.3检查Bchi自动机接受的语言是否为空90 9.4LTL公式转化为自动机93 9.5采用On-the-Fly技术的模型检测97 9.6检测语言包含的符号方法98 第10章偏序约简100 10.1异步系统中的并发101 10.2独立性与不可见性102 10.3LTL?X的偏序约简104 10.4一个例子107 10.5计算充足集ample集合109 10.6算法的正确性114 10.7SPIN系统中的偏序约简117 第11章结构间的等价性和拟序122 11.1等价和拟序算法128 11.2构建tableau结构129 第12章组合推理133 12.1多个结构的组合134 12.2判断假设保证证明方法的正确性136 12.3CPU控制器的验证136 第13章抽象139 13.1影响锥化简139 13.2数值抽象141 第14章对称性154 14.1群和对称性154 14.2商模型156 14.3对称性和模型检测159 14.4复杂度问题160 14.5实验结果164 第15章有限状态系统的无限簇166 15.1无限簇上的时序逻辑166 15.2不变量167 15.3再次分析Futurebus 169 15.4图和网络文法171 15.5令牌环簇的不确定性结果179 第16章离散实时系统和定量时序分析183 16.1实时系统和单调变化率调度183 16.2实时系统的模型检测184 16.3RTCTL模型检测185 16.4量化时序的分析：最小或最大延迟185 16.5飞行控制器187 第17章连续实时系统192 17.1时间约束自动机192 17.2并行组合194 17.3使用时间约束自动机进行建模195 17.4时钟域198 17.5时钟区203 17.6边界可区分矩阵208 17.7复杂度问题211 第18章结论213 参考文献215 內容試閱： 序 言 目前，大家广泛认为有某种原因阻碍了实践帮助计算机就会帮助人类更多的理念，这使得我们更易于将复杂、敏感的系统丢给其他人去实现。这既不是机器的计算速度引起的，也不是计算能力造成的，而是工程师普遍缺乏设计并实现在所有环境中都会正确运行的复杂系统的自信。 这种设计有效性，即尽可能早地保证设计的正确性，是任何系统开发过程中都会遇到的挑战；而且关于这一问题的解决过程，在整个开发周期的成本和时间预算中所占的比例不断增加。 目前，保证设计有效性的方法依旧是持续了多年的模拟和测试技术。工程师已经在这两种技术领域积累了丰富的经验。在调试的早期阶段，这两种技术非常有效，但是经过它们检测后，系统设计仍然可能包含大量错误。随着系统设计越来越精确，这两种方法的工作效率急剧降低，每发现一个小错误都需要花费大量时间。此外，这两种方法还会导致一系列的问题：没有人知道这种技术的查错极限，更没有人能预测出经检测后设计中还剩余多少错误。随着设计复杂度的急剧增加，比如从大约五十万门的芯片设计提高到五百万门的芯片设计，一些有远见的项目经理已经预见到这些传统方法将要崩溃，并且它们将无力再扩展或提升。 形式化验证技术是一个非常具有吸引力的验证方法，可以用于替代模拟与测试，这种方法是本书的主旨。模拟与测试能够检测系统的部分可能行为与情况，但是不能确定系统是否还含有致命错误，而形式化验证却能对系统的全部行为进行彻底的检测。因此当系统设计被形式化验证方法证明为正确时，就蕴含了所有的行为已被检测通过，并且再也不用考虑是否达到足够的覆盖率或者是否含有行为缺失这样的问题。 这些年已经提出了多种形式化验证技术。本书集中介绍的模型检测方法，通过对给定反应系统模型中所有可达状态与行为进行显式的或隐式的彻底的检测，来验证系统规约的行为特性。 与其他方法相比较，模型检测方法有两个显著的优势： ? 自动进行，并且不要求使用者具有专业的数学知识如定理证明和经验。对于任何具有模拟检测经验的人，完全能够使用模型检测进行验证。同当前的验证方法相比，模型检测可以被视为一个更高级的模拟工具。 ? 如果模型检测得出设计未能满足某些期望的性质，那么将产生一个反例来说明系统违反性质的具体行为。这种缺陷轨迹有助于理解检测失败的真实原因，同时也提供了修复此问题的重要线索。 这两个重要的优势，再加上可以对天文数字般的状态进行彻底的隐式枚举的符号模型检测方法，引起了形式化验证领域的根本变革，将模型检测技术从一个纯理论的学科转变为实际可行的技术。模型检测技术可以融入许多工业开发流程中，已经成为一种确保设计有效性的有价值的方法。 工业界普遍认同模型检测具有巨大的实力和潜力，大量的研究人员也在致力于模型检测技术的开发，所开发的产品已经应用于大型先进半导体电路和处理器公司的研发过程中。 非常幸运能够出现这本关于模型检测的原理与方法的权威性著作，这本书的作者从模型检测思想着手，全面介绍了模型检测中各种令人惊讶的技术，并最终构建出一个成功的技术体系。 我对这本出色的参考书非常有信心。这本书将有助于读者包括学生与从业人员理解形式化验证特别是模型检测技术的原理与实现。 Amir Pnueli 前 言 计算机科学中的多个领域都涉及有限状态并发系统，特别是数字电路与通信协议与这种系统关系紧密。这些系统研发过程中出现的逻辑错误对于电路设计者和程序员而言，都是一个非常棘手的问题，可能会推迟新产品的上市时间，也可能导致一些投入使用的重要设备发生故障。目前广泛使用的验证技术是测试和模拟，但当电路或协议的状态规模巨大时，这些技术无疑会遗漏重要的错误。虽然定理证明器、项重写系统和证明检测器都经过了长期和大量的研究，但是这些技术不但耗时，还常常需要许多人工干预。在20世纪80年代，一个被称为时序逻辑模型检测的验证技术由美国的Clarke与Emerson[61]以及法国的Quielle与Sifakis[219]分别独立提出。这种方法使用命题时序逻辑来表示性质规约，电路与协议被建模为状态变迁系统，并且提出一个用于确定规约是否在变迁系统上为真的高效查找过程，即检测变迁系统是否是性质规约的模型。 同机械化的定理证明或证明检测相比，模型检测在验证电路与通信协议方面有着多个重要的优势，其中最重要的优势是检测过程的全自动化，使用者只需提供被检测的模型与性质规约的高阶描述。模型检测算法要么以结果为真终止，此时模型满足规约；要么给出一个反例指出性质违反规约的原因。在复杂变迁系统中，这种反例非常有益于发现和修正细微错误。模型检测过程相当快，通常大约几秒钟产生一个结果。在检测过程中，由于可以部分地检测规约，所以在获得有用信息之前不必构建完整的系统模型。当性质规约不能满足时，可以通过精心构建与当前规约不同的公式，来检测并定位错误的源头。除此之外，描述性质规约的逻辑能直接表示许多并发系统推理所需的性质。 模型检测的主要缺点是状态爆炸，这种情况发生在由许多系统组件并发演化构成的系统中。在这种情况下，整个系统状态的数目将按组件数量呈指数级增长。由于这个问题，许多形式验证的研究者预言模型检测对于大型系统绝对是不实用的。但是，在20世纪80年代后期，模型检测技术所能检测的变迁系统的规模显著地增大了。 这种增长归因于高效表示布尔函数的二叉判定图结构的应用，它不但简洁地表示了变迁系统，也提升了布尔运算的速度。符号模型检测方法对同步电路特别有用。在验证异步协议时，可通过偏序约简技术来减少状态空间的规模。偏序约简的基础是，不同顺序事件对应的计算无法被性质规约区分，可以认为是等价的，因此只需为等价类保留一个典型的计算，检测这种约简空间即可。 基于以上这些技术，以及稍后在本书中介绍的其他一些技术，现在模型检测已经作为一种实用的验证技术在工业界中得到了广泛使用。实际上，几家公司正开始把模型检测工具推向市场。 我们认为这本书既可作为模型检测的简介，也可作为研究者的参考。我们试图包含尽可能多的内容而使其完整，但是这个领域的研究进展如此之快，以至于勉强跟上令人兴奋的新研究成果都不可能。这本书的若干部分与其他部分相比更加专业，在第一次阅读时可以跳过它们，这些部分在书中已经标出，它们主要针对从业者与研究者。我们真诚地希望这本书能够激励读者在模型检测领域做出更好的研究。 最后，作者要感谢那些帮助创作这本书的人。首先想要对David Long表示我们的谢意，他的努力使这本书顺利出版。我们也想要感谢那些审阅初稿的人们，他们是：Eric Allen、Ilan Beer、Armin Biere、Sergey Berezin、Sergio Campos、Ching-Tsun Chou、Allen Emerson、Kousha Etessami、Nissim Francez、Masahiro Fujita、Yair Harel、Wolfgang Heinle、Hiromi Hiraishi、Neil Immerman、Somesh Jha、Irit Katriel、Shmuel Katz、Bob Kurshan、Kim G. Larsen、Yuan Lu、Jan Maluszynski、Will Marrero、Marius Minea、Bud Mishra、Ulf Nilsson、Wojciech Penczek、Amir Pnueli、Toshio Sekiguchi、Subash Shankar、Zeev Shtadler、Prasad Sistla、Frank Stomp、Wolfgang Thomas、Moshe Vardi、Dong Wang、Pierre Wolper、Bwolen Yang、Husnu Yenign、Yunshan Zhu。如果我们遗漏了对这本书有所帮助的人们，我们在此道歉。Edmund Clarke感谢Michael Shostak在写书的过程中所给予的鼓励。Doron Peled感谢Marta Habermann于1998年在CMU的春季学期中提供了一个舒适安逸的居所。

書城介紹　 |　合作申請　|　索要書目　 |　新手入門　|　聯絡方式　 |　幫助中心　|　找書說明　 |　送貨方式　|　付款方式	台灣用户　|　香港/海外用户
megBook.com.tw
Copyright (C) 2013 - 2024 （香港）大書城有限公司　All Rights Reserved.