软件体系结构建模研究

提出了软件体系结构工程的概念，建立了软件体系结构的生命周期模型并对软件体系结构进行了分类和建模，介绍了几种典型的软件体系结构语言，提出了一个基于时序逻辑的形式化体系结构语言－ＸＹＺ／ＳＡＥ．该语言可作为系列化时序逻辑语言族ＸＹＺ／Ｅ的子语言，支持对软件体系结构可的构件，连接件和配置的描述，并可在统一的框架下描述软件体系的结构静态行为和动态行为。     

软件过程建模语言研究

本文介绍了软件过程建模的基本概念，提出了对软件过程建模语言的基本要求并简要介绍了几个有代表性的过程建模语言，给出了一个基于时序逻辑的形式化过程建模语言ＸＹＺ／ＰＭＥ，该语言是时序逻辑语言ＸＹＺ／Ｅ的子语言，它支持以角色为中心的逐步求精的过程建模方法，可在统一的形式框架内表示不同抽象级的过程模型．软件过程，软件过程建模，过程建模语言，时序逻辑，程序设计语言．     

UML活动图的时序逻辑语义

UML活动图可以表示不同抽象级的控制流,很适合用于对系统的行为建模．但是缺乏精确的语义使得难以对它所表示的系统行为进行分析．XYZ／E是一可执行线性时序逻辑语言,既可描述系统的动态行为又可表示程序性质,用它对活动图形式化后,就可在统一的逻辑框架下分析活动图的性质．定义了一个有向图结构用以表示UML活动图,再给出其XYZ／E语义,并用一个例子说明活动图到XYZ／E的语义转换,为进一步的分析提供形式化基础．     

基于时序逻辑的UML2.0通信图语义研究

UML2.0通信图可以表示对象之间的交互,很适合用于对系统的交互行为建模,但由于UML缺乏精确语义,使得难以对其所表示的系统行为进行分析和验证.XYZ/E是可执行线性时序逻辑语言,既可描述系统的静态语义和动态语义.在定K.UML2.0通信图的形式化语法的基础上,给出了通信图的XYZ/E时序逻辑语义,为进一步的系统分析和验证提供了形式化基础.     

时序Ada网的语言性质

在Ada网的基础上，利用时序Petri网为Ada任务程序建模，提出了时序Ada网的概念，利用时序Ada网，可以很好地反映Ada程序的公平性和原子性要求及描述程序的需求，规范，对时序Ada网的语言性质进行分析，结论表明时序Ada网所能接受的网语言能完整地刻画程序的动态行为和时序关系，有助于对程序性质的分析和验证。     

基于Petri网的一种时序分析方法

Ｐｅｔｒｉ网由于有强大的建模能力和成熟的理论支持,被广泛应用于各种系统的建模．本文通过把Ｐｅｔｒｉ网转换成转移系统,利用转移系统和Ｋｒｉｐｋｅ结构给出时序逻辑语义的解释,从而建立了一种在Ｐｅｔｒｉ网上进行时序分析的方法．这种方法是根据不动点理论,用模型检查验证公式正确性．通过对Ａｄａ程序会合性质进行模型检查,验证了这种方法的有效性．     

并发程序验证的时序Petri网方法

并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一。Petri网和时序逻辑被认 为是探讨该问题较为有效的两个理论工具,但二者都有局限性。该文引用一种新网子类;时序Petri网,描述了并发程序的时序Petri网建模方法;利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质。     

行为时序逻辑与自反线性时序逻辑的关系

为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中。对行为时序逻辑公式的语义进行形式化定义．从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系．提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念。定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统．以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。     

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

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

支持协商的网构软件体系结构行为建模与验证

针对网构软件行为中的不确定性和不完整性,提出了一种支持协商的网构软件体系结构行为建模与验证方法.在建模中,该方法借鉴了UML时序图元素表示法,并增加了建模元素支持行为的不确定与不完整建模.在验证中,除了集成广泛应用的模型检查工具Spin以提供行为模型的验证能力以外,还引入了基于反例引导的抽象-精化过程思想的协商检查,以解决不确定和不完整建模所带来的正确性验证问题.     

The detection of Udpstorm attacks based on model checking linear temporal logic

The intrusion detection based on model checking temporal logic is effective in detecting the complicated and variable network attacks. However, certain types of attacks remain undetected due to the lack of formal models. To solve this problem, a linear temporal logic is employed to model the variable patterns of Udpstorm attacks. First, an analysis of the principles of Udpstorm attacks is given and the details of these attacks are transformed into atomic actions. The atomic actions are then transformed into action sequence. Finally, this type of attacks is expressed in Linear Temporal Logic (LTL) formulas. With the formula thus obstained used as one input of the model checker and the automaton, which expresses the log, used as the other input of the model checker, the results of intrusion detection can be obtained by conducting the LTL model checking algorithm. The effectiveness and the comparative advantages of the new algorithm are verified by the simulation experiments.     

基于软件体系结构的反射工作流

提出了基于软件体系结构的反射工作流模型．作为元层的抽象软件体系结构和物理软件体系结构概念的分离,使得应用语义和实现技术相分离;映射元对象建立抽象软件体系结构到基层工作流任务结构的因果连接;行为元对象执行工作流实例的活动调度等功能．讨论了工作流活动和过程级别的动态性．     

一种软件体系结构级基本路径覆盖方法

软件体系结构描述系统的高层结构和行为特征,其动态描述常被用来指导软件的分析和测试。基于此,提出一种软件体系结构级的测试路径覆盖方法。利用化学抽象机描述软件体系结构并导出与其对应的DAG图,表达软件体系结构的动态特征。根据基本路径覆盖准则及测试序列生成算法,生成测试路径。以C/S体系结构为例验证该方法的正确性和有效性。     

Foundations for using linear temporal logic in Event-B refinement

In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.     

一种面向普适计算的适应性软件体系结构风格

普适计算软件需要适应用户需求和运行环境的动态变化.这一特点使得软件复杂度空前增加,迫切需要以软件体系结构为代表的架构/设计层面重用手段来支持其高效开发.在以适应性为中心的普适计算空间抽象模型基础上,提出了一种面向普适计算的软件体系结构风格UbiArch,并从概念视图、运行视图和开发视图这3个维度对该软件体系结构风格进行了阐述.UbiArch支持软件实体按需加入应用、主动适应环境的行为模式,实现了软件适应能力的高层次重用,同时与构件等成熟软件技术的紧密结合也保证了其可实践性.支撑该体系结构风格的软件平台原型系统及其上的应用验证了UbiArch的有效性和通用性.     

Temporal logic for process specification and recognition

Acting intelligently in dynamic environments involves anticipating surrounding processes, for example to foresee a dangerous situation by recognizing a process and inferring respective safety zones. Process recognition is thus key to mastering dynamic environments including surveillance tasks. In this paper, we are concerned with a logic-based approach to process specification, recognition, and interpretation. We demonstrate that linear temporal logic (LTL) provides the formal grounds on which processes can be specified. Recognition can then be approached as a model checking problem. The key feature of this logic-based approach is its seamless integration with logic inference which can sensibly supplement the incomplete observations of the robot. Furthermore, logic allows us to query for process occurrences in a flexible manner and it does not rely on training data. We present a case study with a robotic observer in a warehouse logistics scenario. Our experimental evaluation demonstrates that LTL provides an adequate basis for process recognition.     

面向Agent的分析与建模

传统分析方法注重目标软件系统的功能,分析的结果是一个完全,一致和无二义的软件需求规范。     

ARTEMIS-ARC系统协同模型的自省式实现技术研究

基于运行时体系结构的协同模型能够为面向服务的协同应用系统的动态演化提供有效的支持。但是在实现层面上,如何使软件体系结构从抽象的规约转化为运行时实际的对象实体,并成为系统演化行为的直接载体,是一个较为困难的技术挑战。针对这个问题,本文提出一种基于计算自省的实现途径,主要包括基于面向对象程序设计语言构造的体系结构层面的元表示和元协议、基于体系结构上下文中对象引用重解释构建的因果互连机制,以及基于该因果互连机制的应用系统的动态重配置。以上实现方式在自行开发的服务协同系统ARTEMIS-ARC时得以实施。     

Practical synthesis of reactive systems from LTL specifications via parity games

Acta Informatica - The synthesis of reactive systems from linear temporal logic (LTL) specifications is an important aspect in the design of reliable software and hardware. We present our adaption...     

Distributed Software System Design Representation Using Modified Petri Nets

A model for representing and analyzing the design of a distributed software system is presented. The model is based on a modified form of Petri net, and enables one to represent both the structure and the behavior of a distributed software system at a desired level of design. Behavioral properties of the design representation can be verified by translating the modified Petri net into an equivalent ordinary Petri net and then analyzing that resulting Petri net. The model emphasizes the unified representation of control and data flows, partially ordered software components, hierarchical component structure, abstract data types, data objects, local control, and distributed system state. At any design level, the distributed software system is viewed as a collection of software components. Software components are externally described in terms of their input and output control states, abstract data types, data objects, and a set of control and data transfer specifications. They are interconnected through the shared control states and through the shared data objects. A system component can be viewed internally as a collection of subcomponents, local control states, local abstract data types, and local data objects.