下载文档原格式
软件工程中的形式化方法研究早期软件系统规模较小,20世纪60年代之前,对软件系统的开发一直通过“手工”方式,具有个人化及技艺化的开发特点。
60年代中期,计算机的容量和速度有了显著提升,软件系统规模越来越大,软件开发生产率不再能满足现状,软件危机开始爆发。
60年代后期,针对“软件危机”提出两类解决办法:一是将工程化应用于软件的开发过程,即“软件工程”的出现和发展;二是建立严格的理论基础,采用形式化方法来指导软件开发过程。
经过近半个世纪的探索和应用,形式化方法这一领域已经取得了大量的研究成果。
1形式化方法1.1形式化方法软件工程中的形式化方法就是通过严格的符号系统和数学模型来描述和验证一个目标软件系统的行为和特性,包括需求规格、设计和实现等。
形式化方法所使用的是严格的数学语言,其语法和语义都是无二义的、精确的。
1.2主要研究内容形式化方法的研究主要集中在形式规约(FormalSpecification)和建立在形式规约基础上的形式验证(FormalVerification)两个方面。
形式规约是指通过具有精确语义的形式语言对程序功能进行描述。
描述结果将作为程序设计和验证的重要依据。
形式验证是对现有的程序系统进行验证,检查其是否符合规约的要求。
传统的验证方式是通过实验对系统进行查错,包括模拟(simulation)和测试(testing)。
1.3形式化方法的分类根据描述方式,可将形式化方法归为两类:(1)模型描述的形式化方法。
通过构造一个数学模型来直接描述系统或程序。
(2)性质描述的形式化方法。
通过对目标软件系统中不同性质的描述来间接描述系统或程序。
根据表达能力,可将形式化方法大概分为五类[Barroca*1992]:(1)模型方法——对系统状态和改变系统状态的动作直接给出抽象定义,并进行显式描述。
该方法的缺陷是不能显式地表示并发。
(2)代数方法——通过定义不同操作的关系,隐式地描述操作。
与模型方法相同,代数方法也不能显式地表示并发。
软件工程形式化方法 z 语言软件工程是一个复杂而庞大的领域，要确保软件系统的正确性和可靠性，需要采用各种形式化方法。
形式化方法是一种严格、精确的描述和分析系统的方法，其中最著名的是Z语言。
1. 什么是形式化方法形式化方法是一种使用数学符号和形式化规范来描述和分析软件系统的方法。
它能够捕捉系统的各个方面，从而确保系统的正确性和可靠性。
形式化方法可以消除歧义和模糊性，提供严格的语法和语义定义，并进行可靠的推理和验证。
2. Z语言的引入和发展Z语言是一种基于数学集合论和一阶谓词逻辑的形式化规范语言。
它于20世纪70年代由牛津大学的J.R.阿兰·特拉弗斯和J.B.斯托拉兹提出，并继续在软件工程领域的学术界和实践中得到广泛应用。
3. Z语言的特点和优势- 精确性：Z语言使用严格的数学符号和形式化规范，可以精确地描述系统的各个方面，避免了自然语言的歧义和模糊性。
- 可读性：尽管Z语言使用了数学符号，但其符号系统和语法规则都经过严格定义，使得Z规范可以被可靠地解释和理解。
- 可验证性：Z语言规范的严格性使得系统的正确性验证变得可行。
通过形式化推理和模型检测等技术，可以对规范进行自动验证和分析。
- 模块化：Z语言支持模块化规范，可以将系统的不同部分进行独立的规范和验证，从而提高开发过程的灵活性和可重用性。
4. Z语言在软件工程中的应用- 需求分析和规约：Z语言可以用于对软件系统的需求进行精确描述和形式化规约，从而帮助开发人员和用户准确理解和交流需求。
- 设计规约和验证：Z语言可以用于对软件系统的设计进行精确描述和形式化规约，并进行验证和验证。
通过验证，可以发现设计冲突和错误，提高系统的可靠性。
- 系统建模和仿真：Z语言可以用于对软件系统进行形式化的建模和仿真。
通过建立形式化模型，可以进行系统行为的精确分析和评估，从而帮助设计和优化系统。
- 代码生成和自动化工具支持：Z语言可以作为设计工具中的一部分，与代码生成和其他自动化工具集成，从而提高开发效率和系统质量。
第六讲软件工程的形式化说明技术软件工程使用的描述技术有三类：非形式化技术、半形式化技术和形式化技术。
所谓非形式化技术的代表方法是用自然语言描述的需求规格说明；所谓半形式化技术的代表方法有数据流图、E-R图和UML等；所谓形式化技术的方法有很多，其中具有代表性的方法包括有：时序逻辑语言、有穷状态机、Petri网系统和Z语言等；所谓形式化规格说明语言的关键思想是把软件开发过程中的需求规格说明阶段和软件设计说明阶段分开,在需求规格说明阶段精确地描述软件“做什么”，而不涉及“怎么做”。
编写规格说明与编写计算机程序的不同之处在于规格说明是对目标软件系统的功能描述，而计算机系统则是实现目标软件系统功能的过程描述。
形式化和非形式化描述方法各有优缺点形式化描述的优点：1．使用形式化方法可以严格准确地描述出系统对象；2．使用形式化方法描述的系统可以向任意具体系统进行映射转换；3．可以对形式化描述的系统进行严格的数学证明分析；形式化描述的缺点：1．形式化描述方法难以使用；2．使用形式化描述一个庞大的实际系统存在许多困难，在实际应用中有许多问题本身就是模糊或非确定的无法使用严格的形式化方法进行描述；3．形式化描述的模型对于那些没有经过专门的训练用户来说很难理解；4．形式化说明的正确性证明费时费力；5．尚未出现支持形式化风格全过程的软件环境；非形式化方法的优点：1．描述的模型直观，容易理解；2．非形式的描述技术比较简单，容易学习；3．许多的应用只能使用非形式化的方法描述；非形式化方法的缺点：1．非形式化的描述可能存在矛盾、二意性和含糊性等问题；2．难以进行严格的证明工作；3．对于高可靠性的系统，使用该方法描述存在潜在的问题；本文介绍三种形式化方法：有穷状态机、Petri网、Z语言有穷状态机：使用一个六元组来准确地描述系统状态的变化的一种形式化方法。
当前状态+事件+谓词=>下一个状态Petri 网：Petri的背景：Petri网的首次提出是由德国科学家Petri于1962年在他的博士论文《用自动机通讯》中提出的使用网状结构模拟通讯系统。
