处于时间情景中的推理与形式化

现实的推理是在时空中进行的,推理本身需要花费时间。传统的逻辑理论忽视了这一点,从而导致逻辑全能。为此,给出了相关的案例,表明现实的推理处于时间情景之中 同时,介绍了几个涉及时间的形式化理论,指出它们研究的是关于时间的推理,而非处于时间之中的推理 最后,阐述了一个新的逻辑理论——步进逻辑,认为步进逻辑体现了推理的时间情景,有着良好的应用前景,进而提出了未来的研究设想。     

不可否认协议形式化分析的SVO逻辑方法

使用SVO逻辑对Zhou-Gollmann的公平不可否认协议的一个改进协议进行了形式化分析．在分析该协议的过程中,分析了使用SVO逻辑分析不可否认协议时存在的一些问题,这是分析过程无法发现Zhou-Gollmann不可否认协议的原因．这些问题包括协议目标的确定,协议时限性的描述与分析,协议初始假设集的确定等．分析协议时,不仅需要证明协议的最终目标,还需要证明中间目标．通过对SVO逻辑的语法进行扩展,使其具有显式的时间描述能力,从而能够分析不可否认协议的时限性．     

UML 顺序图的一种形式化描述方法

统一建模语言UML是一种通用的图形化建模语言,在面向对象系统的分析和设计中,它已成为了事实上的工业标准。但UML不是形式化的建模语言,缺乏精确的、形式化的语义,因此阻碍了它的进一步发展。线性时序逻辑是并发或反应式程序动态语义的一种形式化描述语言,它适合用来精确地表示模型的动态语义。本文定义了顺序图的形式化语法,采用线性时序逻辑给出了顺序图的语义描述,并通过实例分析,对模型的某条性质进行了证明,为模型做进一步分析和验证提供了基础。     

关于形式化方法与软件可靠性的研究

形式化方法是一种基于数学的表示方法.它的意义在于它能帮助发现其它方法不容易发现的系统描述的不一致,不明确或不完整,有助于增加软件开发人员对系统的理解,因此形式化表示方法是提高软件系统,特别是Safety-Critical系统的安全性与可靠性的重要手段.     

走出形式化的困境

逻辑的形式化是对自然语言推理的程式化、模式化、符号化，其实质是精确化、抽象化。抽象化到一定界限，它会脱离自然语言实际。实质蕴涵怪论、道义逻辑中的罗斯悖论以及认知逻辑中的厄勒克特拉悖论，都是抽象化、形式化的结果。要消除这些悖论，摆脱形式化的困境，就要由抽象回到具体，回归自然语言，研究自然语言概念、命题及推理的具体用法。     

基于层次时间自动机的移动授权的建模与验证

基于通信的列车运行控制(communication based train control,CBTC)系统以其安全、可靠等性能优点在城市轨道交通的运营中得到广泛关注。它通过其核心功能,即为每一列通信列车提供移动授权(movement authority,MA),来实现列车安全间隔运行。针对功能安全和实时性等方面的不足,首先,建立移动授权的层次时间自动机(hierarchical time automaton,HTA)模型,其中嵌入了列车管理、安全位置、遍历障碍物和列车筛选模块,并对模块间的交互信息进行分析;其次,采用巴科斯范式(Backus-Naur form,BNF)语法对其特性进行描述;最后,利用UPPAAL对各特性验证。结果表明,移动授权模型满足实时性、顽健性、可用性、完整性、安全性5项需求,层次时间自动机理论适用于系统需求规范的验证。     

基于Petri网的安全协议形式化分析与验证

形式化分析方法由于它简洁性成为网络协议的可靠途径。本文提出用Petri网表示网络安全协议的方法描述现在普遍运行的RSA密码体系,并且对Petri的模型进行可达性分析从而验证了RSA的安全性。     

论哲学的逻辑建模

哲学的逻辑建模是与我们的直觉和实在经验相符合,能够对一定范围的哲学问题提供答案的形式理论框架。广义地说,哲学的逻辑建模是建立在逻辑-数学基础上,用于描述和分析哲学概念、哲学论题和哲学推论的形式技术。哲学不仅从逻辑-数学模型获益,而且它本身也提供哲学模型。     

符号的本质及其对人类的意义——对卡西尔《人论》的解读

符号是形式和意义规约的联系。符号的本质在于它的形式化,包括语言、艺术、神话、宗教等的形式化。符号对人类的意义包括两个方面,对文化的开创和对文化的重建。     

浅析中职英语课堂教学

在中职英语课堂教学中渗透多方面教育是当今时代发展的需要,是课程改革的需要,更是中职学生身心发展的需要。本文以新课程改革为背景,结合教学实践,探讨了通过英语课堂教学,提升受教育者对中职英语的兴趣。     

一种面向对象的形式化规范说明技术——VDM＋＋

介绍了一种新的面向对象的形式化规范说明技术ＶＤＭ＋＋它是ＶＤＭ的一种扩充，并且通过一个实例说明如何应用ＶＤＭ＋＋技术对面向对象系统进行形式化规范说明。     

基于LOTOS对象模型的并发形式化研究

面向对象技术和形式化方法结合,在面向对象技术中应用形式化方法,是一种实现软件自动化的有效方法。介绍了形式化描述语言LOTOS的组成、操作语义和规则;根据LOTOS对并发操作描述的优势,应用它的操作语义和规则定义,结合面向对象技术和状态图的理论知识,定义出对象的状态变迁、状态图和对象并发的形式化规则,并运用这些规则对软件系统进行并发形式化;给出了GTP管理子系统形式化的实例说明。     

UML视图的一种形式化模型及其分析

UML是一种得到广泛应用的系统建模语言，但是由于它缺乏形式化语义和严格的推理机制，从而影响了系统建模的准确性和开发效率。TCOZ是一种将Object—Z和TCSP相结合的形式化语言，具有丰富的建模能力。基于TCOZ，本文建立了UML视图的一种形式化模型，对类图和协作图等提出了转换规则，使得TCOZ中的推理可用于分析UML视图。通过某学校信息系统的实例，阐述了UML视图的形式化建模方法和分析技术。     

TOP状态非典型变迁的形式化研究

协议的规格说明主要是以自然语言描述的,对其进行形式化的目的是精确描述协议,减少开发人员对协议规格说明理解的偏差,B方法以数学理论为基础,可产生简明、精确、无歧义且可证明的规格说明,B方法的优点使得它适合对协议进行形式化描述和一致性测试。本文详细介绍了使用B方法对TCP状态非典型变迁进行形式化,并据此生成了测试用例,提高了TCP协议一致性测试的质量和可靠性。     

基于钩子的计算机监控程序的实现

在许多场合下,需要跟踪用户的操作信息,基于此目的,这篇文章阐述了一个基于钩子函数的监控系统。它能够记录用户的键盘输入并且将它保存到文件。同时,它能够把用户操作时当前活动窗口的标题和运行程序的时间记录到文件里。它主要使用了键盘钩子,键盘钩子被放入动态链接库中,属于全局钩子,负责记录键盘信息。     

管理信息系统开发中的形式化需求分析方法研究

需求分析是管理信息系统（MIS）开发中的关键性工作，其质量优劣直接决定MIS的开发成败。以模糊数学为基础，运用神经网络的方法和原理，在深入研究的基础上，提出了一种针对企业信息系统开发中需求分析的形式化方法，它可以大大提高系统需求分析的效率和质量。这一方法已得到初步使用，取得了满意的结果。     

铁路信号域形式化方法研究

铁路信号系统作为安全关键系统。它的失效可能带来灾难性的后果或重大经济损失，因此，安全关键系统的软件开发对可靠性和安全性的要求非常苛刻，而需求分析及描述是软件生命周期的一个重要环节，它所确立的系统逻辑模型是设计和实现目标系统的基础，提出了一种适合于计算机处理的铁路信号域知识的形式化表达方法，希望代替以往继电器接点电路表示的逻辑关系处理方式。     

基于UML需求建模的一种形式化分析方法及其应用

UML是软件开发过程中广泛使用的建模语言,但由于缺乏精确的语义,难以直接对其建立的需求模型进行精化和验证,因而无法进一步提高软件的正确性和可靠性,也不具备实现软件自动化的前提条件.提出了一种基于UML需求建模进行形式化分析的方法.采用Object-Z对UML建立的需求模型进行形式化描述,采用Perfect弥补了Object-Z在精化与验证方面缺少自动化工具支持的不足,最后通过一个实例说明了该方法在实际应用中的可行性.     

Microsoft组件对象模型的形式化描述

基于组件的软件开发(CBD)是一种较为理想的软件开发方法,它根据组件标准,将独立开发的软件组件组合成应用.组件对象模型(COM)是目前最为流行的实现级组件软件协议,它是Microsoft关于如何建立组件和如何根据组件构造应用的一个规范,1995年公布的COM规格说明详细地定义了建立和使用COM组件应遵循的规则.然而该规格说明是非形式化的,这使得它缺乏逻辑的严密性,容易引起歧义.本文根据COM规格说明定义的规则,为其建立一个形式化的组件模型,模型反映了COM组件的本质,但省略了一些具体细节. 模型采用规格说明语言Z进行描述.