采用动作时序逻辑的Web服务组合方法

基于有限状态自动机理论,将Web服务建模成一个有限状态自动机。针对网络服务描述语言(WSDL)在服务行为描述方面的缺陷对其进行扩展,提出了从扩展的WSDL到动作时序逻辑(TLA)语言的转换算法,从而可以用TLA对服务行为进行形式化描述和规范,为描述Web服务提供了一个新的方法。讨论了在动作时序逻辑中,服务组合时各组件服务的有限状态自动机的组合方式,以及伴随着服务组合,单个服务的TLA规范如何组合以形成复合服务的TLA规范的问题,并在此基础上,提出了实现TLA规范正确组合的算法思想。     

基于uppaal的飞机着陆控制系统模型验证

为了避免飞机在着陆过程中出现事故,同时又能充分利用机场的跑道资源,对飞机数量多于跑道的情况进行了研究,采用了模型验证的方法.介绍了时间自动机的相关理论,以及基于该理论的验证工具uppaal,在此基础上使用uppaal工具对飞机着陆过程构造了模型,然后对模型的需求规范进行了验证,验证结果表明该模型不存在死锁问题,最终可以保证飞机安全和及时地着陆.     

元胞自动机交通流模型中的车辆更新方式研究

基于TASEP(Totally Asymmetric Simple Exclusion Process)模型,使用蒙特卡洛方法模拟开放边界条件下不同车辆更新方式对稳态时车辆特性及相变行为的影响,得到不同注入概率α和输出概率β条件下的交通流基本图。结果表明,不同更新方式对系统的稳态特性及相变行为有较大影响,流量和密度随α和β的不同而变化,模拟结果与解析解吻合。随机更新方式下道路车流量的大小由输出概率决定,当输出概率达到一定值时,它的增大无法提高道路上的车流量;顺序更新方式的优点是仅当输入和输出概率都相等时,系统保持畅行相;而局部并行更新方式下得出的相图则与顺序和全局并行更新这两种方式下得到的相图类似且可以更好地反映交通流现实。     

Deciding determinism of caterpillar expressions

Caterpillar expressions have been introduced by Brüggemann-Klein and Wood for applications in markup languages. Caterpillar expressions provide a convenient formalism for specifying the operation of tree-walking automata on unranked trees. Here we give a formal definition of determinism of caterpillar expressions that is based on the language of instruction sequences defined by the expression. We show that determinism of caterpillar expressions can be decided in polynomial time.     

一种节约内存的中文多模式匹配算法

AC及其改进算法基于有限状态自动机,随着中文模式串数目增加,完全Hash表和状态表矩阵存储方式会导致存储空间快速膨胀,状态转移函数计算量大,Cache命中率下降,算法的时空性能急剧下降。提出以邻接链表方式存储有限状态自动机,并将状态"0"的链表转化为线性表,以提高算法的时空效率。在此基础上,设计了一种适合中文的多模式匹配算法,该算法所需存储空间仅为完全Hash表方式的10%,约为状态表矩阵方式的20%。     

一种特征点格驻留元胞自动机人群场景分析方法

为了通过视频场景人群状态分析及预报达到预防公共场所发生安全事故的目的,提出了一种改进的特征点格内驻留CA模型(inner-grid parking CA,IPCA).依据行人行进速度各不相同的特点,将元胞内特征点移动速度的取值范围和方式进行了趋真模拟;在元胞格内引入驻留时间以消除个体行进中的位置误差;采用符合人类视野描述的三角形视场所覆盖的元胞确定前向及内容参数.实验结果表明,改进后的模型不依赖于行人行进时在特定视频帧中反映的运动信息,仿真效果趋近真实视频场景状态,具有更高的准确性.     

基于ASM模型的协议一致性测试研究

针对协议测试中,状态机描述、测试集成环境和被测实现彼此独立带来的问题,提出了在可视化编程环境下利用抽象状态机模型和桩函数结合实现协议一致性测试方法。在分析抽象状态机测试理论的基础上,给出基于抽象状态机和remoting技术的协议分布式测试模型。以抽象状态机语言描述简单文件传输协议为例,采用分布式测试模型,实现了被测协议的远程一致性测试。     

Inclusion dynamics hybrid automata

Hybrid systems are dynamical systems with the ability to describe mixed discrete-continuous evolution of a wide range of systems. Consequently, at first glance, hybrid systems appear powerful but recalcitrant, neither yielding to analysis and reasoning through a purely continuous-time modeling as with systems of differential equations, nor open to inferential processes commonly used for discrete state-transition systems such as finite state automata. A convenient and popular model, called hybrid automata, was introduced to model them and has spurred much interest on its tractability as a tool for inference and model checking in a general setting. Intuitively, a hybrid automaton is simply a “finite-state” automaton with each state augmented by continuous variables, which evolve according to a set of well-defined continuous laws, each specified separately for each state. This article investigates both the notion of hybrid automaton and the model checking problem over such a structure. In particular, it relates first-order theories and analysis results on multivalued maps and reduces the bounded reachability problem for hybrid automata whose continuous laws are expressed by inclusions (x′f(x,t)) to a decidability problem for first-order formulæ over the reals. Furthermore, the paper introduces a class of hybrid automata for which the reachability problem can be decided and shows that the problem of deciding whether a hybrid automaton belongs to this class can be again decided using first-order formulæ over the reals. Despite the fact that the bisimulation quotient for this class of hybrid automata can be infinite, we show that our techniques permit effective model checking for a nontrivial fragment of CTL.     

拟(h,k)存贮有限自动机的可逆性

主要研究拟(h,k)阶存贮有限自动机的延迟k步与k+1步弱可逆性,以及它的弱逆,得到了拟(h,k)阶存贮有限自动机的延迟k步与k+1步弱可逆的充分必要条件,并且通过所得结果可以比较简便地构造出延迟k步与k+1步弱可逆拟(h,k)阶存贮有限自动机的延迟k步与k+1步弱逆.