下载风险提示
若需要下载，请务必先预览(下载的文件和预览的文件一致)
质量、数量、时间上的核对，一旦你付费下载，本站将不予退款。
原文件部分截取内容：
形式化方法
董威 教授
wdong@nudt.edu.cn
国防科技大学计算机学院
软件设计与体系结构
形式化方法
传统工程技术往往能在进行产品生产之前,通过建立模型进行演算、测试和验证，从而保证产品生产出来后具有期望的性质。
软件工程的目标：Develop reliable systems
形式化方法：
Mathematical languages, techniques and tools
Used to specify and verify systems
Goal: Help engineers construct more reliable systems
2
形式化方法
形式化规约(Formal Specification)
使用具有严格数学定义语法和语义的语言刻画软件系统及其性质。
形式化验证(Formal Verification)
在形式化规约的基础上验证系统是否满足所期望性质的过程。
Verifier
Property
System
Yes/No
3
(1)形式化规约
对系统的不同方面进行描述
功能行为(Functional behavior)
时序行为(Timing behavior)
性能特征(Performance characteristics)
内部结构(Internal structure)
实时约束(Real-time constraints)
安全策略(Security policies)
体系结构(Architectural design)
……
4
一个简单的例子——求最大公约数
非形式化描述：寻找能够整除两个给定自然数的最大自然数。
形式化描述：a和b是两个自然数，它们的最大公约数是
规约语言
5
各种形式化规约
顺序系统的形式化规约
侧重于对状态空间的描述，利用集合、关系和函数等离散结构表达系统的状态和迁移
Z 、VDM 等
并发系统的形式化规约
侧重于对系统并发特性的描述，用序列、树、偏序等来表达系统的行为
CSP、CCS、状态图、时序逻辑等
6
(2)形式化分析与验证
模型检验
通过搜索待验证软件系统模型的有穷状态空间来检验系统的行为是否具备预期性质的一种自动验证技术。
定理证明
将软件系统和性质都用逻辑方法来规约，通过基于公理和推理规则组成的形式系统，以如同数学中定理证明的方法来证明软件系统是否具备所期望的性质。
静
“3-4-形式化方法.ppt”
百度一下
搜狗搜索
360搜索
相关资源：pmpm:Web的穷人软件包管理器-PMP代码类资源-CSDN文库
声明：本站部分文章及图片源自用户投稿，如本站任何资料有侵权请您尽早请联系jinwei@zod.com.cn进行处理,非常感谢！