计算机支持的协同工作系统的时序逻辑模型

为了使群体能够协同完成任务,CSCW(computer supported cooperative work)系统不仅要解决各种分布性、处理应用领域的特殊性,而且要提供面向用户的协作支持,从而使其行为异常复杂.然而对系统行为进行形式化的描述是构造软件系统的必经阶段.为了清晰地描述CSCW系统的行为,使其特定性质的验证成为可能,本文在时序逻辑的基础上,建立了CSCW系统行为的抽象描述模型.在此模型中,CSCW系统由分布运行实体和信息对象组成,系统的主要行为表现为用时序逻辑语言XYZ/E描述的实体间的交互.此模型可较好地对系统的分析和构造进行指导.     

分布式软件系统交互行为建模、验证与测试

为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用UML2．0序列图对模块之间交互行为进行描述．采用基于命题投影时序逻辑的模型检测技术,将对象状态机图转换为 Promela 模型,系统交互性质转换为命题投影时序逻辑公式,通过模型检测器验证交互模型是否满足于系统的性质,若不满足于该性质,则能够获得反例执行的路径．给出了一个分布式软件系统测试框架,在验证后的序列图模型基础上,使用基于模型的测试用例自动生成方法得到测试用例集合,该集合能够实现对交互行为的有效测试．实例结果表明,该方法可以提高分布式软件系统中模块交互行为的有效性和可靠性．     

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

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

基于线性时序逻辑的多Agent协商推理模型

在多智能体系统中,协商是Agent交互的主要形式.用形式化方法构建了基于线性时序逻辑的协商推理模型,该模型用线性时序逻辑描述在协商过程中Agent所处环境,自身能力、权力、知识、思维等随时间的变化,以及在系统运行时Agent采取异步行为.进一步完善了多Agent系统中自主的协商机制.     

基于线性时序逻辑的对象文件系统形式化描述

基于线性时序逻辑,给出了对象文件系统特性的形式化描述.对象文件系统时序逻辑(OFSTL)是线性时序逻辑在描述对象文件系统应用中的一个推广.用OFSTL描述对象文件系统的性质,用模型化的状态迁移系统表示对象文件系统的访问行为.试图解决目前对象文件系统研究存在的问题: ①关注提升对象文件系统性能和功能,但是以增加对象文件系统复杂性为代价; ②很少针对对象文件系统精确描述,缺乏形式化的辅助,妨碍从细节上考查对象文件系统的正确性.     

UML2.0顺序图的时序描述逻辑语义

针对UML2.0顺序图用于对象间交互行为建模时存在动态语义缺乏精确形式化描述的问题,提出一种基于时序描述逻辑的UML2.0顺序图形式化方法。对描述逻辑进行时序扩展,得到可表示动态和时序语义的形式化规范——时序描述逻辑,根据UML2.0新增的交互操作符将UML2.0顺序图分成一个或多个最大顺序片段,通过形式化最大顺序片段和交互操作符得到UML2.0顺序图的时序描述逻辑语义。实例检验结果表明,该方法具有可行性。     

混合投影时序逻辑与混合系统的形式化验证

为了描述混合系统的性质和行为，10多年来，各种时序逻辑，如Hybrid Temporal Logic等相继出现。这些时序逻辑适用于刻画混合系统的性质和规范，但不适宜表示描述系统的实现模型。本文定义了一个混合投影时序逻辑（Hybrid Projection Temporal Logic，简称HPTL），既能刻画混合系统的性质，又能表示混合系统的实现。这样，混合系统的验证就可以很方便地在统一的数学模型框架下进行。同时，给出了HPTL的基本的逻辑等价式系统和一个用HPTL进行混合系统验证的实例。     

一种基于Web Service的CSCW应用——MATLAB协同计算系统

Web Service是当前支持CSCW的一种主流的分布式技术,本文对CSCW和Web Service的核心概念、体系结构和关键技术进行了探讨,并对当前MATLAB的的网络扩展功能进行了研究.提出了一种基于Web Service的CSCW应用模型--MATLAB协同计算系统,对该模型的工作原理和主体构架进行了详细的论述,并以UML时序图的方式,说明了系统中各模块间的交互模式.最后给出了一个实现实例.     

RGPS过程层元模型正确性验证

利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系统实例证明该验证方法的正确性和有效性。     

基于交互规则建模的信息系统实时状态监测技术研究

基于信息系统协同关联交互规则,利用XML(可扩展标记语言)技术,对信息系统中分系统、设备的相关属性、交互信息等进行分层建模描述,建立系统的实时状态监测模型;通过多线程并行处理技术,实时采集数据并匹配系统状态监测模型,实现对信息系统的交互状态、时序逻辑、工作状态、数据内容的合规性、完整性、正确性等方面的实时监测,并给出异常告警和提示;同时,结合系统的故障模式、影响及危害性分析,对当前系统故障的影响给出初步的分析,分析结果提供指挥员用于辅助决策参考.     

用高阶逻辑表达时态逻辑及其应用

硬件设计的形式化验证技术开辟了对复杂的超大规模集成电路设计进行验证的新途径。高阶逻辑和时态逻辑在形式化验证技术中均得到成功的应用。本文介绍用高阶逻辑表达线性时态逻辑和区间时态逻辑的方法，并以几个简单实例说明它在硬件设计验证中的应用。这种方法的优点是既利用高阶逻辑系统ＨＯＬ的机械化定理证明手段，又发挥了时态逻辑的表达硬件的动态性质的能力。     

一种基于同步网的工作流管理系统

作为一类典型的CSCW系统,工作流管理系统主要提供异步、结构化的协同支持。本文从模型入手,介绍了一种基于Petri网的工作流模型——同步网。它采用分层视图描述了过程逻辑、语义及管理,过程模型和管理模型的互动关系用来指导工作流引擎的构造。本文基于同步网开发了工作流管理系统,支持工作流的定义、执行和管理。为了满足CSCW的需要,工作流管理系统中增加了同步协作机制。     

一种基于Büchi自动机的LTL程序模型检测方法

时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。基于自动机的理论,用标签转移系统（S）表示程序的行为,用时序逻辑公式（F）描述程序的性质,构建相应的Büchi自动机,从而证明形式化公式SF是否可满足。     

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

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

A predicate spatial logic for mobile processes

A modal logic for describing temporal as well as spatial properties of mobileprocesses, expressed in the asynchronous π-calculus, is presented. The logic has recur-sive constructs built upon predicate-variables. The semantics of the logic is establishedand shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm isdeveloped to automatically check if a mobile process has properties described as formulasin the logic. The correctness of the algorithm is proved.     

基于规则的安全策略定义语言

基于任务－角色访问控制机制,提出类似一阶谓词逻辑的安全策略定义语言,并且有一定的时序表达功能。用户使用这种高层描述语言可在不同的系统中定义各种特定应用的安全策略。还给出了基于扩展的稳定模型的语义描述,定义了安全策略正确性的条件以及验证方法,并进一步讨论实现安全策略的有关问题。     

基于CSCW的复杂产品协同工艺设计

专家系统在CAPP中的应用，使工艺设计系统变得日趋复杂。通过分析工艺设计过程中存在的问题，提出了一种基于CSCW的协同工艺设计与管理模式，使工艺设计由串行转为并行，有效提高了设计效率和系统柔性。     

First-Order Temporal Verification in Practice

First-order temporal logic, the extension of first-order logic with operators dealing with time, is a powerful and expressive formalism with many potential applications. This expressive logic can be viewed as a framework in which to investigate problems specified in other logics. The monodic fragment of first-order temporal logic is a useful fragment that possesses good computational properties such as completeness and sometimes even decidability. Temporal logics of knowledge are useful for dealing with situations where the knowledge of agents in a system is involved. In this paper we present a translation from temporal logics of knowledge into the monodic fragment of first-order temporal logic. We can then use a theorem prover for monodic first-order temporal logic to prove properties of the translated formulas. This allows problems specified in temporal logics of knowledge to be verified automatically without needing a specialized theorem prover for temporal logics of knowledge. We present the translation, its correctness, and examples of its use. Partially supported by EPSRC project: Analysis and Mechanisation of Decidable First-Order Temporal Logics (GR/R45376/01).     

应用于CSCW协同控制机制的分析与设计

基于因特网环境的CSCW中协同控制的研究,提出一个协同控制机制的概念模式,依此模式发展一个协同控制协议,实际应用于CSCW环境,使得在一个多用户信息共享环境中的群体合作能顺利进行,并增进了CSCW系统的协同程度和确保数据的一致性,发展成为一个可以应用于CSCW环境的协同控制协议.通过对该协同控制模式的研究结果,建立有实际应用目标的CSCW环境,推广到远程协作学习、协同设计、协同会诊、协同创作、群体决策等应用领域.     

发动机CAD协同设计的集成环境方案研究

在对 CSCW系统的协同模式进行分析的基础上 ,提出了一种基于 J2 EE和工程数据库的 CSCW系统实现的体系结构 ,其中工程数据库管理系统采用 Servlet/ Jsp/ Bean技术 ,实现了分布式异步协同模式。采用 Ap-plet遵循 CORBA协议实现同 I- DEAS的通讯 ,实现了分布式同步协同模式