亲爱的MBA智库百科用户:


过去的17年,百科频道一直以免费公益的形式为大家提供知识服务,这是我们团队的荣幸和骄傲。 然而,在目前越来越严峻的经营挑战下,单纯依靠不断增加广告位来维持网站运营支出,必然会越来越影响您的使用体验,这也与我们的初衷背道而驰。 因此,经过审慎地考虑,我们决定推出VIP会员收费制度,以便为您提供更好的服务和更优质的内容。


MBA智库百科VIP会员,您的权益将包括: 1、无广告阅读; 2、免验证复制。


当然,更重要的是长期以来您对百科频道的支持。诚邀您加入MBA智库百科VIP会员,共渡难关,共同见证彼此的成长和进步!



MBA智库百科项目组
2023年8月10日
百科VIP
未登录
无广告阅读
免验证复制
1年VIP
¥ 9.9
支付方式:
微信支付
支付宝
PayPal
购买数量:
1
应付金额:
9.9
汇率换算:
9.9
美元(USD)

按当月汇率换算,

包含手续费

打开手机微信 扫一扫继续付款
立即开通
PayPal支付后,可能会遇到VIP权益未及时开通的情况,请您耐心等待,或者联系百科微信客服:mbalib888。
温馨提示:当无法进去支付页面时,可刷新后重试或更换浏览器
开通百科会员即视为同意《MBA智库·百科会员服务规则》

支付成功

全球专业中文经管百科,由121,994位网友共同编写而成,共计436,064个条目

软件形式化方法

用手机看条目

出自 MBA智库百科(https://wiki.mbalib.com/)

软件形式化方法(The formal method)

目录

[隐藏]

什么是软件形式化方法

  软件形式化方法是指建立在严格数学基础上的软件开发方法。形式化方法模型的主要活动是生成计算机软件形式化的数学规格说明。形式化方法使软件开发人员可以应用严格的数学符号来说明、开发和验证基于计算机系统

软件形式化方法的起源

  软件形式化方法最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究,即J.Backus提出BNF描述Algol60语言的语法,出现了各 种语法分析程序自动生成器以及语法制导的编译方法,使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法

  形式化方法的研究高潮始于20世纪60年代后期,针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类:一是采用工程方法来组织管理软件的开发过程;二是深入探讨程 序和程序开发过程的规律,建立严密的理论,以其用来指导软件开发实践。前者导致“软件工程”的出现和发展,后者则推动了形式化方法的深入研究。经过30多 年的研究和应用,如今人们在形式化方法这一领域取得了大量、重要的成果,从早期最简单的形式化方法一阶谓词演算方法到现在的应用于不同领域、不同阶段的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法。形式化方法的发展趋势逐渐融入软件开发过程的各个阶段,从需求分析、功能描述(规约)、(体系结构/算法)设计、编程、测试直至维护。

软件形式化方法的内容

  形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。不同的形式化方法的数学基础是不同的,有的以集合论和一阶谓词演算为基础(如Z和VDM),有的则以时态逻辑为基础。形式化方法需要形式化规约说明语言的支持。

  这样的形式化方法提供了一个框架,可以在框架中以系统的而不是特别的方式刻划、开发和验证系统。如果一个方法有良好的数学基础,那么它就是形式化的,典型地以形式化规约语言给出。这个基础提供一系列精确定义的概念,如:一致性和完整性,以及定义规范的实现和正确性。形式化方法模型的主要活动是生成计算机软件形式化的数学规格说明。形式化方法使软件开发人员可以应用严格的数学符号来说明、开发和验证基于计算机的系统。这种方法的一个变型是净室软件工程(cleanroom software engineering),这一软件工程方法目前已应用于一些软件开发机构。

软件形式化方法的分类

  1、根据说明目标软件系统的方式,形式化方法可以分为两类:

  1. 面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为
  2. 面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。

  2、根据表达能力,形式化方法可以分为五类:

  1)基于模型的方法:通过明确定义状态和操作来建立一个系统模型(使系统从一个状态转换到另一个状态)。用这种方法虽可以表示非功能性需求(诸如时间需求),但不能很好地表示并发性。如:Z语言,VDM,B方法等。

  2)基于逻辑的方法:用逻辑描述系统预期的性能,包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构 造扩充逻辑从而得到一种广谱形式化方法,通过保持正确性的细化步骤集来开发系统。如:ITL(区间时序逻辑),区段演算(DC),hoare 逻辑,WP演算,模态逻辑,时序逻辑,TAM(时序代理模型),RTTL(实时时序逻辑)等。

  3)代数方法:通过将未定义状态下不同的操作行为相联系,给出操作的显式定义。与基于模型的方法相同的是,没有给出并发的显式表示。如:OBJ, Larch族代数规约语言等;

  4)过程代数方法:通过限制所有容许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。如:通信顺序过程(CSP),通信系统演算 (CCS),通信过程代数(ACP),时序排序规约语言(LOTOS),计时CSP(TCSP),通信系统计时可能性演算(TPCCS)等。

  5)基于网络的方法:由于图形化表示法易于理解,而且非专业人员能够使用,因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言,为系统开发和再工程带来特殊的好处。如 Petri图,计时Petri图,状态图等。

相关条目

本条目对我有帮助3
MBA智库APP

扫一扫,下载MBA智库APP

分享到:
  如果您认为本条目还有待完善,需要补充新内容或修改错误内容,请编辑条目投诉举报

本条目由以下用户参与贡献

寒曦,Tracy,Mis铭,苏青荇.

评论(共0条)

提示:评论内容为网友针对条目"软件形式化方法"展开的讨论,与本站观点立场无关。

发表评论请文明上网,理性发言并遵守有关规定。

打开APP

以上内容根据网友推荐自动排序生成

官方社群
下载APP
告MBA智库百科用户的一封信
亲爱的MBA智库百科用户: 过去的17年,百科频道一直以免费公益的形式为大家提供知识服务,这是我们团队的荣幸和骄傲。 然而,在目前越来越严峻的经营挑战下,单纯依靠不断增加广告位来维持网站运营支出,必然会越来越影响您的使用体验,这也与我们的初衷背道而驰。 因此,经过审慎地考虑,我们决定推出VIP会员收费制度,以便为您提供更好的服务和更优质的内容。 MBA智库百科VIP会员(9.9元 / 年,点击开通),您的权益将包括: 1、无广告阅读; 2、免验证复制。 当然,更重要的是长期以来您对百科频道的支持。诚邀您加入MBA智库百科VIP会员,共渡难关,共同见证彼此的成长和进步!
MBA智库百科项目组
2023年8月10日

闽公网安备 35020302032707号

添加收藏

    新建收藏夹

    编辑收藏夹

    20