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

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

香港／國際用戶

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

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

送貨：速遞 / EMS，時效：出貨後2-3日

新書推薦： 《 生活在低处 》 售價：NT$ 291.0 《 长颈鹿与少年（全球销量超过50万册。基于真实历史事件创作） 》 售價：NT$ 260.0 《 近代早期海洋文化史 》 售價：NT$ 510.0 《 怪诞行为学2：非理性的积极力量 》 售價：NT$ 354.0 《 锦衣玉令 》 售價：NT$ 510.0 《 米沃什与布罗茨基：诗人的友谊 》 售價：NT$ 406.0 《 法国小史 》 售價：NT$ 499.0 《 五凉王国的七张面孔 》 售價：NT$ 359.0

建議一齊購買： + NT$ 247 《 医学免疫学与病原生物学实训教材 》 + NT$ 338 《 金融经济学二十五讲（21世纪经济学系列教材） 》 + NT$ 234 《 大学生素质教育概论（第四版） 》 + NT$ 265 《 管理学：原理与方法（第七版）习题与案例指南（博学·大学管理类丛书） 》 + NT$ 458 《 兽医药理学 》 + NT$ 249 《 内部控制与风险管理（第3版）（MPAcc精品系列） 》 內容簡介： 形式化方法是指有严格数学基础的软件和系统开发方法，支持软件与系统的规约、设计、验证与演化等活动。随着软件可信需求的不断增长，形式化方法的重要性和关注度日益提高。全书共12章，章概述形式化方法，第2章介绍形式化方法发展早期的经典内容，其余部分共分3篇：上篇（第3～5章）为系统建模篇，着重介绍迁移系统、有穷自动机、Petri网等基本计算模型；中篇（第6和第7章）为形式规约篇，着重讨论时序逻辑及其在并发系统属性描述的应用；下篇（第8～12章）为形式验证篇，除介绍演绎证明方法外，着重介绍验证并发、实时及混成系统的各种模型检测方法及相关验证工具。全书提供了大量应用实例，每章后均附有习题。本书适合作为高等院校计算机、软件工程、网络工程、信息安全、自动化等专业高年级本科生、研究生的教材，同时可供相关领域的研究人员和技术开发人员参考。 目錄： 章绪论 1.1形式化方法的发展历程 1.2形式化方法的基本内容 1.2.1系统建模 1.2.2形式规约 1.2.3形式验证 1.3本章小结 习题1 第2章程序正确性证明 2.1前后断言法 2.1.1基本概念 2.1.2证明方法 2.1.3应用举例 2.2公理化方法 2.2.1基本概念 2.2.2证明方法 2.2.3应用举例 2.3 弱前置条件方法 2.3.1基本概念 2.3.2证明方法 2.3.3应用举例 2.4本章小结 习题2 上篇系统建模 第3章迁移系统 3.1基本概念 3.1.1形式定义 3.1.2迁移图 3.1.3计算 3.2应用举例 3.2.1时序电路 3.2.2数据依赖系统 3.2.3并发和交错 3.3本章小结 习题3 第4章自动机 4.1有穷自动机 4.1.1有穷状态系统 4.1.2形式定义 4.1.3判定算法 4.2Buchi自动机 4.2.1ω—有穷自动机简介 4.2.2Buchi自动机 4.2.3应用举例 4.3本章小结 习题4 第5章Petri网 5.1库所／变迁Petri网 5.1.1基本概念 5.1.2基本性质 5.1.3分析方法 5.1.4应用举例 5.2谓词／变迁Petri网 5.2.1基本概念 5.2.2应用举例 5.3着色Petri网 5.3.1基本概念 5.3.2应用举例 5.4本章小结 习题5 中篇形式规约 第6章时序逻辑 6.1线性时序逻辑 6.1.1LTL语法 6.1.2LTL语义 6.1.3应用举例 6.2分支时序逻辑 6.2.1CTL语法 6.2.2CTL语义 6.2.3应用举例 6.3区间时序逻辑简介 6.4本章小结 习题6 第7章并发系统属性 7.1基本概念 7.2安全性 7.2.1形式定义 7.2.2形式描述 7.2.3应用举例 7.3活性 7.3.1形式定义 7.3.2形式描述 7.3.3应用举例 7.4本章小结 习题7 下篇形式验证 第8章演绎证明 8.1演绎证明方法 8.1.1PLTL逻辑系统 8.1.2Manna—Pnueli演绎规则方法 8.1.3验证图方法 8.1.4应用举例 8.2验证工具STeP 8.2.1STeP简介 8.2.2STeP使用 8.3STeP应用举例 8.3.1建模 8.3.2验证 8.4本章小结 习题8 第9章模型检测 9.1基本概念 9.2模型检测算法 9.2.1CTL模型检测算法 9.2.2LTL模型检测算法 9.3模型检测工具及应用 9.3.1验证工具SPIN 9.3.2应用举例 9.4本章小结 习题9 0章符号模型检测 10.1二叉决策图 10.1.1基本概念 10.1.2约简方法 10.1.3Apply操作及应用 10.2CTL符号模型检测 10.2.1基本方法 10.2.2验证工具SMV 10.2.3应用举例 10.3LTL符号模型检测简介 10.4本章小结 习题10 1章概率模型检测 11.1概率模型 11.1.1离散时间马尔可夫链 11.1.2马尔可夫决策过程 11.1.3连续时间马尔可夫链 11.2概率时序逻辑 11.2.1概率计算树逻辑 11.2.2连续逻辑 11.3概率模型检测工具及应用 11.3.1验证工具PRISM 11.3.2应用举例 11.4本章小结 习题11 2章实时与混成系统验证 12.1时间自动机 12.1.1语法 12.1.2语义 12.2实时逻辑 12.2.1时间计算树逻辑 12.2.2度量区间时序逻辑 12.3实时系统模型检测 12.3.1基本方法 12.3.2验证工具UPPAAL 12.3.3应用举例 12.4混成系统验证简介 12.4.1混成自动机 12.4.2微分动态逻辑 12.4.3混成系统模型检测 12.5本章小结 习题12 参考文献

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