一种面向嵌入式软件体系结构的形式化建模方法

为了解决MARTE（Modeling and Analysis of Real Time and Embedded systems）在建立嵌入式软件模型时不够精确的问题,结合Object-Z和PTA（Probabilistic Timed Automation）的优点,本文提出了一种集成的形式化建模方法--PTA-OZ.该方法不仅能够对嵌入式软件模型的静态语义和动态语义进行精确描述,而且通过模型转换规则,能够将MARTE模型转换为PTA-OZ模型.并对模型转换的语义一致性进行了验证,证明本文方法在转换过程能够保持结构语义和行为语义的一致性.最后通过实例模型描述从嵌入式软件建模到属性检验的过程.     

数据库集成系统中数据语义和属性不一致问题的解决方法

介绍了数据库集成时所需要的主要知识，提出了利用模糊集合理论解决数据库集成系统中数据语义和数据值不一致的方法，最后结合例子描述了数据库集成环境中的查询处理方法，该方法能适用于各种应用环境。     

Wright语言的实时扩展

Wright是一种适合于对具有并发特性的系统进行仿真建模的著名体系结构描述语言。文章针对Wright语言对实时性描述支持的不足，利用TCSP对其进行了行为语义的扩展，增强其对具有实时并发特性的系统进行建模的能力。利用扩展后的Wright语言。在系统开发的早期即可对系统的活性、安全性等时间相关的特性进行模型检验。     

用本体实现智能交通系统的语义集成

智能交通系统整体效益的发挥，很大程度上取决于各个分系统的协调和整合，而集成是提高ITS系统性能的有效手段。面向中国智能交通系统的语义集成问题，建立了基本本体、领域本体、应用本体的三层本体体系结构，根据中国智能交通系统体系框架(National Intelligent Transport System Architecture)给出了本体系统的本体分类。研究了本体的表示方法，并提出了基于本体的语义集成框架。     

面向工作流的组织记忆描述模型与实现

为在知识密集型工作流中捕获组织中的知识或信息并嵌入到流程中，提出了一种面向工作流的组织记忆描述模型，设计了基于本体的组织记忆描述模型到面向对象模型的映射器，在此基础上给出了面向工作流组织记忆的实现框架。它根据工作流上下文获取支持信息，支持对语义Web内容的集成，并提供了易于被现有工作流开发人员使用和掌握的工具包，因此提高了上下文感知能力、集成性和可用性。     

浅析TD—SCDMA系统特点对无线定位的影响

本文介绍了无线定位的基本方法，结合TD—SCDMA系统特点，分析了其对无线定位的影响，重点描述了智能天线在无线定位中的应用。     

在多数据库集成环境中的属性集成方法的研究

描述了一种基于模糊集合理论的属性集成方法，它可显示地表示数据库集成系统中数据属性值的不一致程度。介绍了语义更为丰富的扩充的结构化查询语言。最后结合例子描述了在多数据库集成环境中一种属笥集成方法，该方法能适用于各种应用环境。     

领域化业务构件的数据模型可执行语义研究和实现

从企业应用角度出发,为实现快速构建企业信息系统以及提高系统可重用性,提出了一种领域化业务构件描述思路。同时为使开发的信息系统实现企业知识的重用和和共享,方便企业数据交换和集成,将可执行语义建模方法应用到业务构件的业务数据模型中,具体实现参考了语义Web的描述框架。     

一种基于学分制排课系统的Z规格说明

运用形式化方法建模在软件开发过程中可提高目标系统的正确性和可靠性,在此提出了一种利用Z语言进行语义分析的方法。该方法在序列图Z规范的基础上,用属性集表示对象状态,并将序列图的上下文表示为Z形式约束,通过检查上下文约束与对象状态间的一致性对序列图进行语义分析。在此以一个基于学分制的排课系统为例,使用面向对象的形式规格说明语言Z,描述了一个精确、完整的高校排课系统的形式化数学模型。过程显示,该方法具有精确的描述性和很强的抽象性,能为软件系统的开发和验证提供科学的框架。     

关于LOTOS并发操作符行为特性的探讨

LOTOS是ISO制定的描述并发通信系统的标准化形式语言。并发组合操作符行为特征复杂，虽然给出了语义，但在编写及分析LOTOS规格说明文件时，仍然容易混淆。本人对并发操作符的可结合，可交换，多路同步，隐藏等机制进行分析和探讨。有助于LOTOS的学习者理解并发行为的本质，提高编写和分析LOTOS规格说明文档的能力。     

Formal Specification and Model-Checking of CSMA/CA Using Finite Precision Timed Automata

1 Introduction Ani mportant activity within the engineering of com-munication andreal-ti me protocolsisto validate whethera given protocol functions as expected.Formal methodscan support this activity to a large extent . During thelast few years ,the formal specification and verificationof networking or telecommunication systems using for-mal tools[1 ~2]has attracted muchinterest fromacademiccommunity and industrial developers . In fact , therehave been some publications to discuss the specifi…     

Real-time information flow analysis

In previous work, we studied some noninterference properties for information flow analysis in computer systems on classic (possibilistic) labeled transition systems. In this paper, some of these properties, notably bisimulation-based nondeducibility on compositions (BNDC), are reformulated in a real-time setting. This is done by first enhancing the security process algebra proposed by two of the authors with some extra constructs to model real-time systems (in a discrete time setting), and then by studying the natural extension of these properties in this enriched setting. We prove essentially the same results known for the untimed case: ordering relation among properties, compositionality aspects, partial model checking techniques. Finally, we illustrate the approach through two case studies, where in both cases the untimed specification is secure, while the timed specification may show up interesting timing covert channels.     

The Z specification dependence graph

The lack of existing solutions makes it really hard to understand formal specification languages since the application domain for representations is useful for the purpose of carrying out certain software engineering operations such as slicing and the computation of program metrics.A Z specification dependence graph is presented in this letter. It draws on the strengths of a range of earlier works and adapts them, if necessary, to the Z language.     

安全协议的一种CSP开发框架

论文基于系统的API平台提出安全协议的一种CSP开发框架,将形式化方法与高级语言有机结合起来,实现了协议由形式化说明转换为可执行代码处理过程的自动化,有利于快捷准确地将已完成CSP验证的安全协议翻译为可执行代码,避免了在将CSP描述转换为可执行代码预处理过程中引入安全隐患的可能性。     

Specifying and proving properties of timed I/O automata using Tempo

Timed I/O automata (TIOA) is a mathematical framework for modeling and verification of distributed systems that involve discrete and continuous dynamics. TIOA can be used for example, to model a real-time software component controlling a physical process. The TIOA model is sufficiently general to subsume other models in use for timed systems. The Tempo Toolset, currently under development, is aimed at supporting system development based on TIOA specifications. The Tempo Toolset is an extension of the IOA toolkit, which provides a specification simulator, a code generator, and both model checking and theorem proving support for analyzing specifications. This paper focuses on the modeling of timed systems and their properties with TIOA and on the use of TAME4TIOA, the TAME (Timed Automata Modeling Environment) based theorem proving support provided in Tempo, for proving system properties, including timing properties. Several examples are provided by way of illustration.     

一种软硬件协同设计工具原型及其设计描述方法

软硬件协同设计工具不但需具有软硬件功能划分的能力,而且应可实现系统级设计到软硬件基本结构的综合。提出一种利用进程代数为高层设计语义基础,可重用现有软硬件设计工具资源的软硬件协同设计工具的实现方案框架,重点讨论其中的设计描述问题。采用这种基于语言变换的软硬件协同设计工具方案有利于对系统的活性、安全性、接口一致性等性质进行高层仿真与形式验证,具有可用性、易扩展好等优点。     

基于INAP的智能业务形式化描述和冲突检测

基于业务自然语言定义的业务形式化描述具有模糊性,不能精确地检测出业务冲突的问题,本文提出了一种新的基于智能网应用协议INAP的业务形式化描述和冲突检测方法。