并发系统中谓词行为图的行为时序逻辑表达

行为时序逻辑(TLA)组合时序逻辑与行为逻辑, 可以对并发系统进行描述与验证, 它引入动作和行为的概念, 使得系统和属性可用它的规约公式表示, 但存在用TLA描述复杂系统时TLA公式复杂且难以理解的不足。类似于状态转移图, 对于并发转移可以用谓词行为图进行图形化表示, 谓词行为图与行为时序逻辑规约具有相同的表达能力。介绍行为时序逻辑的语法、语义及简单推理规则, 用一个简单的实例说明使用谓词行为图去描述并发转移系统的有效性, 并用系统规约的TLA公式对谓词行为图表达能力进行证明, 表明两者具有等价性, 为描述和分析并发转换系统提供了一种可行的方法。     

行为时态逻辑TLA定理系统证明及公平性研究

行为时态逻辑TLA(temporal logic of actions)能够在一种语言中同时表达模型程序与逻辑规则,是目前模型检测技术中一个较新的研究方向.为了理解行为时态逻辑与传统时态逻辑之间的理论联系,研究了时态逻辑的语义和定理系统,并根据行为时态逻辑TLA的自身特征指出了TLA中的行为属于时态逻辑T4系统.在此基础上严格的证明了TIA的定理系统及TLA中强公平性蕴涵弱公平性的重要性质,讨论了强公平性与弱公平性等价的条件.最后以实例说明了如何确定动作的强弱公平性,进而建立系统的TLA模型.     

基于TLA的事件图模型形式化验证方法*

针对目前没有直接对事件图模型进行形式化验证的方法,提出了一种基于行为时态逻辑(temporal logic of action,TLA)的事件图模型形式化验证方法.该方法利用TLA语言能够同时表达模型行为与逻辑规则的特点及其与事件图的相似性,将事件图模型及性质规约用TLA语言进行形式化描述,从而使该模型能够被TLA模型...     

基于TLA的NS安全协议分析及检测

行为时序逻辑是一种组合了时序逻辑与行为逻辑来对并发系统进行描述与验证的逻辑,在描述并发转移系统中,行为时序逻辑通过引入行动和行为的概念,使得系统和属性可用同一种行为时序逻辑来表示。本文首先介绍行为时序逻辑的语法、语义及简单推理规则;然后以典型的NS公开密钥协议为例,对其进行形式化分析,建立了入侵者参加的简化模型。通过对模型进行FSM建模,转化为TLA+描述的规约系统,然后对其进行TLC检测,发现其存在中间人的重放攻击。     

行为时序逻辑中四级公平性下的活性推理规则

公平性是行为时序逻辑用于表达系统活性的形式,直接影响到系统描述的正确性与完整性,对其进行细化与完善能有效提高行为时序逻辑的系统描述能力。然而在对公平性进行细化的同时,却缺乏相应的、运用于性质验证的推理规则。针对这一问题,通过对公平性内涵的分析,给出了四级公平性体系下的活性推理规则,并分别进行了证明。作为示例,运用新的活性推理规则,对一个程序实例进行了推理验证。在建立起相应的活性推理规则后,四级公平性才能够被有效运用到实际的系统描述与验证中。     

一种用描述逻辑刻画多代理系统规约的方法

支持模块化的语言机制和严格性能够很好地推动代理技术向更广泛的、更大规模的应用发展.朱宏等人提出的基于模型的多代理系统开发方法提出了符合面向Agent软件工程思想的语言机制,如Caste和Scenario.以该方法为基础提出了基于描述逻辑的对多代理系统的规约进行形式化刻画和分析证明系统属性的方法.利用描述逻辑的强大的表达力刻画多代理系统的规约,利用其自身的推理机制对系统属性进行推理、证明和验证,可以增强基于代理系统的严格性.     

基于TLA＋的BRP协议规约及验证

BRP协议是为不可靠信道上传送大数据包文件设计的工业协议。该协议的正确性依赖于各部件实时方面的假设。本文主要阐述了使用时序规约语言TLA＋对BRP协议进行规约和验证的过程。首先通过自然语言非形式化地描述BRP协议的基本原理和需求，在此基础上建立了BRP的形式化模型，利用TLA＋先对不考虑实时要求的BRP进行规约，然后添加实时约束获得BRP完整的规约，最后使用模型检验器TLC验证BRP协议的各种性质。     

一种从Z到精化演算的软件开发方法

一、引言形式化方法的研究和应用已有二十多年的历史,源于Dijkstra和Hoare的程序验证以及Scott、stratchey等人的程序语义研究,指为保证复杂系统的可靠性,以数学为基础对其进行精确描述和验证的语言、技术和工具。形式化方法的关键在于形式规约语言。通过语法和语义有严格数学定义的形式规约语言对系统及其各方面性能的描述,产生系统的形式规约,可以帮助开发者获得对所描述系统的深刻理解,并通     

基于系统调用属性的程序行为监控

程序的行为轨迹常采用基于系统调用的程序行为自动机来表示.针对传统的程序行为自动机中控制流和数据流描述的程序行为轨迹准确性较低、获取系统调用上下文时间开销大、无法监控程序运行时相邻系统调用间的程序执行轨迹等问题,提出了基于系统调用属性的程序行为自动机.引入了多个系统调用属性,综合系统调用各属性的偏离程度,对系统调用序列描述的程序行为轨迹进行更准确地监控;提出了基于上下文的系统调用参数策略,检测针对系统调用控制流及数据流的行为轨迹偏离;提出了系统调用时间间距属性,使得通过系统调用及其参数无法监控的相邻系统调用间的程序行为轨迹在一定程度上得到了监控.实验表明基于系统调用属性的程序行为自动机能够更准确地刻画程序行为轨迹,较传统模型有更强的行为偏离检测能力.     

基于场景规约的构件式系统设计分析与验证

使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.     

嵌入式系统定义探讨

对目前国内流行的嵌入式系统定义提出质疑,认为嵌入式系统不是"专用计算机系统",嵌入式系统不只"以计算机技术为基础".从嵌入式系统的发展起源、体系结构、功能特点、知识技术体系等方面进行了分析论证,从而进一步完善了嵌入式系统的定义.     

卡车的TSK模糊控制

针对在保证一定精度的条件下,要求一次性完成卡车的倒车的情况,利用TSK (Takagi-Sugeno-Kang)模糊系统控制卡车,在TSK模糊控制器作用下让卡车从任意的初始位置一次性倒车到指定的位置。在卡车数学模型中,线性部分设计线性状态反馈控制器,非线性部分先求TSK模糊模型,然后设计基于TSK模糊模型的TSK模糊控制器。它是一个非线性控制器,可保证闭环系统的稳定性。仿真实验结果表明,所设计的TSK模糊控制器对卡车的倒车控制是非常有效的。     

营销管理专家系统中的知识问题

知识和概念化是专家系统设计与实现中的核心难题，对于领域开放、任务非受限的复杂应用而言，知识的细致充分性和知识形式的匹配有效性是解决诸如营销管理专家系统设计与实现这样现实应用时必然面临的问题。本文详细定义了这样两个问题是什么，它们是如何产生的，并且讨论了解决问题的方法。     

复杂自组织系统的研究综述

自组织系统是一类复杂系统,它通常驻留在开放的环境中,并且可以根据外部环境和内部状态的变化,通过系统成分之间的自主交互,对系统进行动态调整,从而更好地满足设计目标。近年来,随着计算机技术和Internet的不断发展,越来越多的计算机系统呈现出自组织的特征,有关自组织系统方面的研究变得非常活跃,受到学术界和工业界的广泛关注和重视。本文在深入分析自组织系统概念和特点的基础上,从理论模型、核心机制、关键技术、支撑平台四个方面对自组织系统的研究现状进行了综述和分析,介绍了其应用,讨论了自组织系统研究面临的问题和挑战,并展望了进一步研究方向。     

股票信息系统的组成与应用

对中国股票市场的信息系统做了一个总体概括和介绍。将整个股票信息系统分解为券商信息系统、交易撮合系统、盘后结算系统以及行情分析和信息发布等四个系统,并详细阐述了各信息系统之间的关系,分别给出各个信息系统的基本设计原理和架构。     

数字仿真应用科学

数字仿真应用科学,如同其它学科的应用科学一样,也是包括应用理论和应用技术(工程技术、生产技术等)两部分.数字仿真应用理论,按仿真对象不同,可分为连续系统仿真、离散事件系统仿真、连续一离散混合系统仿真、复杂系统仿真来分别加以阐述,而数字仿真应用技术可按构造仿真、实况仿真、虚拟仿真来分别给以说明.如今数字仿真的应用,日益广泛,正在向普适化迈进.     

Sufficient conditions for the stability of a class of interconnected dynamic systems

Some sufficient conditions are derived which can guarantee the stability of a class of interconnected dynamic systems and applying examples are given.     

独立于操作系统的嵌入式FAT32文件系统设计

在嵌入式领域中需要可移植性、灵活性高的FAT32文件系统,以适用多样的硬件存储设备,因此采用一种满足该要求的文件系统设计实现,整个设计采用层次化设计,全部使用C语言编写,无任何特定操作系统API相关的调用,仅依赖少量几个标准C库函数的调用,使得文件系统本身代码不仅与具体硬件平台相分离,而且独立于任何操作系统,从而可以方便及灵活地移植于有操作系统支持或无操作系统支持的环境中。     

N维系统可分性的充要判据

本文给出了N维Roesser模型和一般二维系统模型可分的充要判据,并将所得结果应用于可分系统的稳定性问题,得到了相应的判据。     

变电站综合自动化系统的安全措施

分析变电站综合自动化系统中测控装置和监控装置分别在出现故障情况下所需要采取的必要的安全措施,以保证综合自动化系统的正常运行。