形式化方法研究学术会

❶ 形式化方法的发展过程

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

❷ 孙吉贵的学术论文

[1]输入调解法和单元调解法在Horn集上的完备性 ，《软件学报》1993年2月，4（1）。欧阳丹彤，孙吉贵，刘叙华。
[2]Horn集上的有向调解法，《吉林大学自然科学学报》 1992年11月，（4）。欧阳丹彤，孙吉贵，刘叙华。
[3]Completeness of Input Symmetric Paramolation and Unit Symmetric Paramolation on Horn Set,《Chinese Journal of Advanced Software Research》 1994年5月，1（2）。欧阳丹彤，孙吉贵，刘叙华。
[4]广义因果理论上基于模型诊断过程的形式化，《吉林大学自然科学学报》 2000年10月，（4）。欧阳丹彤，孙吉贵。
[5]基于模型诊断的形式化方法，《人工智能进展（第六届中国人工智能联合学术会议论文集）》 2001年2月1日。欧阳丹彤，孙吉贵，姜云飞。
[6]对基于模型诊断过程的形式化，《模式识别与人工智能》 2002年9月，15（3）。欧阳丹彤，孙吉贵。
[7]“离散数学学习指导与习题解答”，高等教育出版社，2003年8月。
[8]约束逻辑的一个新语义研究，广西师范大学学报（自然科学版），Vol.21, No.1, 2003,1-5。第七届中国人工智能联合学术会议论文集CJCAI2002，张永刚，孙吉贵。
[9]一种模型不完备条件下的诊断方法，广西师范大学学报（自然科学版），Vol.21, No.1, 2003, 79-82。第七届中国人工智能联合学术会议论文集， CJCAI2002，林海，孙吉贵。
[10]基于模型诊断的替换测试与问题分解的研究，广西师范大学学报（自然科学版），第七届中国人工智能联合学术会议论文特刊Vol.21, No.1, 2003, 23-26。李占山，王涛，孙吉贵。
[11]受限的proflog语言及其表推演过程语义，广西师范大学学报（自然科学版），第七届中国人工智能联合学术会议论文特刊，Vol.21, No.1, 2003, 27-33。陈荣，孙吉贵，姜云飞。
[12]一种多值规则量词公式的tableau的方法，广西师范大学学报（自然科学版），第七届中国人工智能联合学术会议论文特刊，Vol.21, No.1, 2003,，101-105。刘全，孙吉贵。
[13]Theorem Proving Based on the Extension Rule, Journal of Automated Reasoning 31, 2003, pp11-21.LIN Hai, SUN Jigui, ZHANG Yimin.
[14]非二元约束满足问题求解，计算机学报，Vol.26, No.12, 2003, pp1746-1752.孙吉贵，景沈艳。
[15]The Concept of Approximation Based on Fuzzy Dominance Relation in Decision-Making, Proceedings 9th International Conference, RSFDGrC2003, Chongqing, China, May 2003. In Guoyin Wang, Qing Liu, Yiyu Yao and Andrzej Skowron eds: Rough Sets, Fuzzy Sets, Data Mining, and Granular Computing, Lecture Notes in Artificial Intelligence 2639, Edited by J.G.Carbonell and J.Siekmann, Subseries of Lecture Notes in Computer Science. Springer, pp382-385.。Yunxiang Liu, Jigui Sun, Shengsheng Wang.
[16]量子搜索算法，软件学报，Vol.14, No.3, 2003, pp334-344.。孙吉贵，何雨果。
[17]提高一阶多值逻辑Tableau推理效率的布尔剪枝方法，计算机学报，Vol.26, No.9, 2003, 1165-1170.。刘全，孙吉贵。
[18]一种含等词的分阶段Tableau算法，计算机工程，Vol.29, No.8, 2003, pp44-46.。刘全，孙吉贵，张永刚。
[19]一种多值规则量词公式的Tableau的方法，计算机工程，Vol.29, No.8, 2003, pp128-130.。刘全，孙吉贵，窦全胜。
[20]组合优化调度问题求解方法，计算机科学，Vol.30, No.2, 2003, pp9-16.张居阳，孙吉贵。
[21]基于约束的调度研究与实现，2003中国计算机大会论文集1，北京，2003年12月，清华大学出版社，pp80-85.。张居阳，礼欣，孙吉贵。
[22]适用于决策表的快速属性约简算法，2003中国计算机大会论文集1，北京，2003年12月，清华大学出版社，pp41-46.。何雨果，孙吉贵。
[23]模糊集合的语义，中国人工智能学会全国第10届全国学术年会论文集（下），广州，2003年12月，2003，pp1072-1077。刘云翔，孙吉贵。
[24]基于t-norm算子的模糊逻辑和模糊推理。吉林大学学报（理学版），Vol.41, No.1, 2003.pp64-69。刘云翔，孙吉贵。
[25]模型生成与约束求解，知识科学与计算科学研讨会，乌鲁木齐，2002年9月，见陆汝钤主编“知识科学与计算科学”，清华大学出版社，2003年1月，197-232。孙吉贵，张永刚。
[26]量子并行计算，知识科学与计算科学研讨会，乌鲁木齐，2002年9月，见陆汝钤主编“知识科学与计算科学”，清华大学出版社，2003年1月，236-242。孙吉贵，何雨果。
[27]基于模型的诊断问题分解及其算法，计算机学报，Vol.26, No.9, 2003, 1171-1176.李占山，姜云飞，王涛。
[28]基于模型诊断方法的系统替换修复与重新配置，吉林大学学报（理学版），Vol.41, No.1, 2003, pp45-48.李占山，王涛，孙吉贵。
[29]商业智能技术及行业应用分析，吉林大学学报（信息科学版），第21卷 第1期 2003.2.李泽海，孙吉贵，赵君。
[30]离散数学教学改革中的几点做法和体会，中国教育理论杂志，第42期， 2003.11。张永刚，孙吉贵。
[31]21世纪《离散数学》教材与教学模式的改革现代教学与管理，2003.第8期。李占山 孙吉贵。

❸ 形式化方法的研究内容

形式化方法的一个重要研究内容是形式规约(Formal Specification,也称形式规范或形式化描述),它是对程序“做什么”(what to do)的数学描述,是用具有精确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验证程序是否正确的依据。对形式规约通常要讨论其一 致性(自身无矛盾)和完备性(是否完全、无遗漏地刻画所要描述的对象)等性质。形式规约的方法主要可分为两类:一类是面向模型的方法也称为系统建模,该方 法通过构造系统的计算模型来刻画系统的不同行为特征；另一类是面向性质的方法也称为性质描述,该方法通过定义系统必须满足的一些性质来描述一个系统。不同 的形式规约方法要求不同的形式规约语言,即用于书写形式规约的语言(也称形式化描述语言),如代数语言OBJ、Clear、ASL、ACT One/Two等;进程代数语言CSP、CCS、π演算等；时序逻辑语言PLTL、CTL、XYZ/E、UNITY、TLA等；这些规约语言由于基于不同 的数学理论及规约方法，因而也千差万别，但它们有一个共同的特点,即每种规约语言均由基本成分和构造成分两部分构成。前者用来描述基本(原子)规约,后者 把基本部分组合成大规约。构造成分是形式规约研究和设计的重点，也是衡量规约语言优劣的主要依据。
形式验证形式化方法的另一重要研究内容是形式验证(Formal Verification)。形式验证与形式规约之间具有紧密的联系，形式验证就是验证已有的程序(系统)P，是否满足其规约(φ,ψ)的要求(即P (φ,ψ)),它也是形式化方法所要解决的核心问题。传统的验证方法包括模拟(simulation)和测试(testing)，它们都是通过实验的方法 对系统进行查错。模拟和测试分别在系统抽象模型和实际系统上进行,一般的方法是在系统的某点给予输入，观察在另一点的输出,这些方法花费很大，而且由于实 验所能涵盖的系统行为有限，很难找出所有潜在的错误。基于此，早期的形式验证主要研究如何使用数学方法，严格证明一个程序的正确性(即程序验证)。

❹ 形式化方法的介绍

形式化方法英文的名称是formal methods。在逻辑科学中是指分析、研究思维形式结构的方法。它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包含概念彼此间的联结,推理中则是各个命题之间的联结,抽取出它们共同的形式结构;再引入表达形式结构的符号语言,用符号与符号之间的联系表达命题或推理的形式结构。例如,把全称肯定命题,用符号形式化为“SAP”;把联言命题、假言命题分别形式化为:“p∧q、“p→q”。又例如:一个具体的假言联言推理“如果这种金属是纯铝,那么它的物理性质必与纯铝相同;如果这种金属是纯铝,那么它的化学性质必与纯铝相同;但这种金属的物理性质和化学性质与纯铝不相同;所以,它不是纯铝。”这个推理的形式结构是:“如果p,则q;如果p,则r;非q且非r;所以非p。”可进而形式化为下列公式:((p→q)∧(p→r)∧┐q∧┐r→┐p。

❺ 形式化方法的分类

根据说明目标软件系统的方式，形式化方法可以分为两类：
1）面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。
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图，状态图等。

❻ 形式化方法

你用画的方法是一个过程的解决方式，这个方式是很流行的

❼ 什么是形式化什么是形式模型

形式化方法一般是用一种严格的，精准的方法（一般是数学语言）描述软件，对软件建模。
你可以理解为类似UML建模。只是形式化的方法更难学，你可以理解为离散数学里的各种规约、公式。形式化模型就是你用形式化方法构建出来的模型，可类比UML模型，也可以类比数学建模，甚至可以类比编程代码（编程同样是用编程语言对软件需求的精确描述）

❽ 对软件形式化方法课程学习的认识

把概念、判断、推理转化成特制的形式符号后，对形式符号表达系统进行研究的方法。它可以消除自然语言的歧义性、不通用性，为不同学科提供具有普遍适用性的共同逻辑形式，有利于揭示新联系，导致新发现。