面向仿真训练系统的过程模型研究

该文首先说明了过程模型的功能，根据功能需求对相关过程建模方法进行分析，找出了适合于仿真系统中过程模型的描述方法，并重点给出了一种基于有限状态机方法的训练过程模型框架、过程模型实时调度方法和应用实例。该过程模型框架由演示过程、物理行为过程、混合过程、过程转移、转移条件等对象类组成，在仿真训练系统开发中，通过定义和扩展这些对象类，对基于有限状态机的过程模型进行控制与调度，准确而全面地描述和管理仿真训练过程，从而有效地解决了仿真训练系统中的过程模型开发问题。     

一种移动支付协议的模型检验分析

给出了移动支付协议的一种有限状态机建模方法,该方法在传统支付协议的基础上充分考察了移动环境中移动装置和无线网络的特点,所建立的模型具有全面、准确、直观、简洁的特点。以一个典型的移动支付协议KSL为例,对该协议进行有限状态机建模,并通过模型检验工具对其公平性进行了分析验证,指出了其缺陷并进行了改进,从而表明了方法的有效性。该方法具有一定的通用性,以其为基础,可对其他类型的移动电子商务协议进行模型检验分析。     

The Meta-Protocol framework

A communication protocol is a set of rules shared by two or more communicating parties on the sequence of operations and the format of messages to be exchanged. Standardization organizations define protocols in the form of recommendations (e.g., RFC) written in technical English, which requires a manual translation of the specification into the protocol implementation. This human translation is error-prone due in part to the ambiguities of natural language and in part due to the complexity of some protocols. To mitigate these problems, we divided the expression of a protocol specification into two parts. First, we designed an XML-based protocol specification language (XPSL) that allows for the high-level specification of a protocol—expressed as a Finite State Machine (FSM)—using Component-Based Software Engineering (CBSE) principles. Then, the components required by the protocol are specified in any suitable technical language (formal or informal). In addition, we developed the multi-layer Meta-Protocol framework, which allows for on-the-fly protocol discovery and negotiation, distribution of protocol specifications and components, and automatic protocol implementation in any programming language.     

嵌入式系统的Internet接入实现

介绍了嵌入式Internet的概念和嵌入式系统的Internet接入实现方案，讲述了在微控制器（MUU)中实现嵌入式WebServer的方法。在分析嵌入式Web服务器有限状态机基础上，用原始套接字编程的方法实现了thin—TCP／IP协议，并且对嵌入式系统应用层协议进行了设计，简化的协议降低了系统硬件的要求。集成这两种协议的浏览器可访问嵌入式WebServer，并通过提交表格的方式向嵌入式WebServer输入控制信息，在工业自动化和消费电子行业有广泛应用前景。     

基于虚拟多任务机制的OSPF-2的设计与实现

OSPF（Open Shortest Path First Protocol）协议是目前Internet上广泛使用的自治系统内部交换路由信息的动态路由协议。文章介绍了在清华大学研制的国产高性能路由器中分布式路由协议OSPF－2的具体实现。为了实现这一复杂的动态协议,文章提出了基于事件驱动的虚拟多任务机制的设计和实现方法。这种机制能够有效支持复杂系统的分解,在实时性要求不高的前提下提供一种简便有效的并行机制,方便基于状态机的软件实现,提高了软件的可移植性。该方法对于其它的Internet高层协议的设计和实现也有一定的参考价值。     

A new approach for the verification of cache coherence protocols

We introduce a cache protocol verification technique based on a symbolic state expansion procedure. A global Finite State Machine (FSM) model characterizing the protocol behavior is built and protocol verification becomes equivalent to finding whether or not the global FSM may enter erroneous states. In order to reduce the complexity of the state expansion process, all the caches in the same state are grouped into an equivalence class and the number of caches in the class is symbolically represented by a repetition constructor. This symbolic representation is partly justified by the symmetry and homogeneity of cache-based systems. However, the key idea behind the representation is to exploit a unique property of cache coherence protocols: the fact that protocol correctness is not dependent on the exact number of cached copies. Rather, symbolic states only need to keep track of whether the caches have 0, 1, or multiple copies. The resulting symbolic state expansion process only takes a few steps and verifies the protocol for any system size. Therefore, it is more efficient and reliable than current approaches. The verification procedure is first applied to the verification of five existing protocols under the assumption of atomic protocol transitions. A simple snooping protocol on a split-transaction shared bus is also verified to illustrate the extension of our approach to protocols with nonatomic transitions     

Bounded time-stamps

Summary Time-stamps are labels which a system adds to its data items. These labels enable the system to keep track of the temporal precedence relations among its data elements. Many distributed protocols and some applications use the natural numbers as time-stamps. The natural numbers however are not useful for bounded protocols. In this paper we develop a theory ofbounded time-stamps. Time-stamp schemes are defined and the complexity of their implementation is analyzed. This indicates a direction for developing a general tool for converting time-stamp based protocols to bounded protocols. Amos Israeli received his B.Sc. in Mathematics and Physics from Hebrew University in 1976, and his M.Sc. and D.Sc. in Computer Science from the Weizmann Institute in 1980 and the Technion in 1985, respectively. Currently he is a senior lecturer at the Tlectrical Engineering Department at the Technion. Prior to this he was a postdoctoral fellow at the Aiken Computation Laboratory at Harvard. His research interests are in Parallel and Distributed Computing and in Robotics. In particular he has worked on the design and analysis of Wait-Free and Self-Stabilizing distributed protocols. Ming Li received his M.S. and Ph.D. in Computer Science from Wayne State University in 1980 and Cornell University 1985, respectively. Currently he is an associate professor at the Computer Science Department at the University of Waterloo. His research interests are in Theory of Computing, Kolmogorov Complexity, and Machine Learning.Supported in part by the Weizmann fellowship and NSF Grant DCR-86-00379Supported in part by ONR Grant N00014-85-k-0445 and Army Research Office Grant DAAL03-86-K-0171 at Harvard University, by NSF Grant kDCR-86-06366 at Ohio State University, and by NSERC Operating Grant OGP0036747. Most of this work was done when the authors were at Aiken Computation Laboratory at Harvard University. The authors also acknowledge the hospitality of the computer science department at York University, Canada     

A test case generation approach for conformance testing of SDL systems

This paper presents an approach for automatic executable test case and test sequence generation for a protocol modeled by an SDL system. Our methodology uses a unified method which tests an Extended Finite State Machine (EFSM) based system by using control and data flow techniques. To test an SDL system, it extracts an EFSM from each process then the system is tested by incrementally computing a partial product for each EFSM C, taking into account only transitions which influence (or are influenced by) C, and generating test cases for it. This process ends when the coverage achieved by the generated test cases is satisfactory or when the partial products for all EFSMs are tested. Experimental results show that this method can be applied to systems of practical size.     

基于UML状态图的测试技术研究

UML统一建模语言已经广泛应用于软件开发中，基于UML图的测试技术最近成为了一个研究的热点，其中对UML状态图的测试有着广泛应用前景。UML状态图是传统状态图的变体，增加了层次、并发、广播。所以UML状态图的测试方法建立在对传统状态机的测试方法的基础上，对层次、并发、广播的处理或转换。本文介绍了基于UML状态图的测试方法和测试工具的研究进展，最后讨论了未来可以研究的方向。     

Inferring extended finite state machine models from software executions

The ability to reverse-engineer models of software behaviour is valuable for a wide range of software maintenance, validation and verification tasks. Current reverse-engineering techniques focus either on control-specific behaviour (e.g., in the form of Finite State Machines), or data-specific behaviour (e.g., as pre / post-conditions or invariants). However, typical software behaviour is usually a product of the two; models must combine both aspects to fully represent the software’s operation. Extended Finite State Machines (EFSMs) provide such a model. Although attempts have been made to infer EFSMs, these have been problematic. The models inferred by these techniques can be non-deterministic, the inference algorithms can be inflexible, and only applicable to traces with specific characteristics. This paper presents a novel EFSM inference technique that addresses the problems of inflexibility and non-determinism. It also adapts an experimental technique from the field of Machine Learning to evaluate EFSM inference techniques, and applies it to three diverse software systems.     

Verification and conformance test generation of communication protocol for railway signaling systems

Verification and testing are complementary techniques that are used to increase the level of confidence in the correct functioning of communication systems as prescribed by their specifications. This paper presents an experience of model checking for Korean railway signaling protocol specified in LTS (Labeled Transition System). This formal approach checks deadlock, livelock and reachability for the state and action to verify whether properties expressed in modal logic are true on specifications. We also propose a formal method for semi-automated test case generation for Korean railway signaling protocol described in I/O FSM (Input/Output Finite State Machine). This enables the generation of more complete and consistent test sequence for conformance testing. The above functions are implemented by C++ language and included within RSPVTE (Railway Signaling Protocol Verification and Testing Environment) in the MS-windows environment.     

基于CFSM的一致性测试序列生成方法

本文采用通信有限状态机模型描述通信协议,基于通信有限状态机模型提出了协议一致性测试的测试序列生成方法,解决了构件化协议的测试序列生成的问题。本文实现了测试序列的生成算法,通过实例说明了采用测试序列生成算法生成了比传统算法更少的测试序列。同时本算法还可以用于多层协议测试。     

USB2.0协议从控制器设计

文章介绍了USB从控制器所要完成的功能和一种实现方案的模块构成，并且说明了实现USB协议的处理流程。同时也介绍了设计USB从控制器的时候应注意的问题，分析了如何用有限状态机描述实现USB2．0协议。     

基于双数组有限状态机的URL访问控制算法

业务选择网关（SSG）中的访问控制模块从用户请求数据包中解析出URL,并且根据用户的URL访问权限进行访问控制和路由选择。首先提出了改进的有限状态机模型,然后用双数组表示该有限状态机,并提出了优先处理分支结点较多的结点的优化策略。实验证明该算法不仅提高了查询速度,而且占用的存储空间也较少,进一步减少了数据的稀疏。最后将该算法应用在访问控制模块上,实践证明此算法可行、高效。     

基于ORD和FSM的Web应用的建模与测试

Web测试是保证高质量Web应用的一种有效技术.然而,由于其特殊性和复杂性,很难直接将传统的测试理论与方法学运用到Web应用的测试当中来.对Web应用进行了分析与建模,并对其进行测试,提出了一种可行的Web测试模型.首先得到页面流图(PFD,Page Flow Diagram),进而产生对象关系图(ORD,Object Relation Diagram),然后根据提出的算法将ORD转化为形式化的有限状态机(FSM,Finite State Machine)模型.基于FSM模型,提出了一种有效的测试路径自动生成方法,这些测试路径可以转化为XML语法的测试规格说明.测试引擎将测试规格说明作为输入最终产生测试报告.全文以所开发的一个小型的Web应用SWLS(Simple Web Login System)为例进行阐述.     

冷连轧混合系统中离散事件仿真的建模及关键技术

本文以冷连轧过程仿真为例，分析了混合系统中离散事件的特点以及与连续部分的关 系，对系统进行了层次化分解，讨论了在混合系统仿真过程中对于离散事件部分的建模需要 注意的问题，同时给出了用有限状态机方法实现仿真建模的过程，以及实际应用中的关键技 术．     

一种使用动态分析的对象状态机自动提取方法

对象行为协议对于辅助其他开发者理解并正确使用对象所提供的外部行为具有十分重要的意义.然而相关文档却常常缺失或存在不一致,需要通过逆向分析的方法进行恢复.针对这一问题,本文提出了一种基于驱动执行和动态分析的对象状态机(Object State Machine,OSM)提取方法.该方法从源代码中提取包含类属性的条件表达式,以其在运行时刻的取值情况及程序异常信息作为状态标识,并通过驱动执行的方式获取运行时的状态转换信息,然后分析运行时信息逐步构造对象状态机.该方法已实现为相应的原型系统,初步实验结果表明通过该方法可以高效、准确地恢复对象行为协议.     

一种复杂BIU的设计及其CPLD实现

文章分析了可配置成多机系统的嵌入式微处理器中的总线接口单元的结构。文章首先详细分析了这种情况下总线接口单元的控制通路。然后从采用格雷方式FSM编码、FSM有效描述和接口信号的正确描述三个方面讨论该部件的高效实现。     

A systematic approach to integrate common timed security rules within a TEFSM-based system specification

Context

Formal methods are very useful in the software industry and are becoming of paramount importance in practical engineering techniques. They involve the design and modeling of various system aspects expressed usually through different paradigms. These different formalisms make the verification of global developed systems more difficult.

Objective

In this paper, we propose to combine two modeling formalisms, in order to express both functional and security timed requirements of a system to obtain all the requirements expressed in a unique formalism.

Method

First, the system behavior is specified according to its functional requirements using Timed Extended Finite State Machine (TEFSM) formalism. Second, this model is augmented by applying a set of dedicated algorithms to integrate timed security requirements specified in Nomad language. This language is adapted to express security properties such as permissions, prohibitions and obligations with time considerations.

Results

The proposed algorithms produce a global TEFSM specification of the system that includes both its functional and security timed requirements.

Conclusion

It is concluded that it is possible to merge several requirement aspects described with different formalisms into a global specification that can be used for several purposes such as code generation, specification correctness proof, model checking or automatic test generation. In this paper, we applied our approach to a France Telecom Travel service to demonstrate its scalability and feasibility.     

Resource access control for dynamic priority distributed real-time systems

Many of today’s complex computer applications are being modeled and constructed using the principles inherent to real-time distributed object systems. In response to this demand, the Object Management Group’s (OMG) Real-Time Special Interest Group (RT SIG) has worked to extend the Common Object Request Broker Architecture (CORBA) standard to include real-time specifications. This group’s most recent efforts focus on the requirements of dynamic distributed real-time systems. One open problem in this area is resource access synchronization for tasks employing dynamic priority scheduling. This paper presents two resource synchronization protocols that meet the requirements of dynamic distributed real-time systems as specified by Dynamic Scheduling Real-Time CORBA 2.0 (DSRT CORBA). The proposed protocols can be applied to both Earliest Deadline First (EDF) and Least Laxity First (LLF) dynamic scheduling algorithms, allow distributed nested critical sections, and avoid unnecessary runtime overhead. These protocols are based on (i) distributed resource preclaiming that allocates resources in the message-based distributed system for deadlock prevention, (ii) distributed priority inheritance that bounds local and remote priority inversion, and (iii) distributed preemption ceilings that delimit the priority inversion time further. Chen Zhang is an Assistant Professor of Computer Information Systems at Bryant University. He received his M.S. and Ph.D. in Computer Science from the University of Alabama in 2000 and 2002, a B.S. from Tsinghua University, Beijing, China. Dr. Zhang’s primary research interests fall into the areas of distributed systems and telecommunications. He is a member of ACM, IEEE and DSI. David Cordes is a Professor of Computer Science at the University of Alabama; he has also served as Department Head since 1997. He received his Ph.D. in Computer Science from Louisiana State University in 1988, an M.S. in Computer Science from Purdue University in 1984, and a B.S. in Computer Science from the University of Arkansas in 1982. Dr. Cordes’s primary research interests fall into the areas of software engineering and systems. He is a member of ACM and a Senior Member of IEEE.