项重写的图实现

图重写能够有效地实现项重写。文章从项重写的图实现的角度出发，研究了图重写模拟项重写的正确性和完备性：在无环出现的情况下，图重写对一切项重写下正确；在无环出现的条件下，图重写对左线性合流的项重写是完备的。     

项重写系统的并行实现方案

项重写系统的并行归约可以提高归约的效率，在无共享内存的Ｔｒａｎｓｐｕｔｅｒ网络上实现时要考虑任务的分配，项的拼装，归约任务的控制等问题，其中怎么样减少机间的机内进程的通信慢提高系统效果的关键。本文从控制方式角度讨论在不同拓扑结构的Ｔｒａｎｓｐｕｔｅｒ网络上实现项重写系统的方案，重点介绍基于树形结构下的控制方法，进程安排和通讯形式。     

依赖项重写系统及其在程序设计语言中的应用

面重写系统是一种简洁通用的计算模型，在许多领域中有着重要的应用。     

项重写系统等价性的归纳证明

尽管学者们在计算机软件理论及相关数学理论方面做出了不懈的努力,但伴随着计算机硬件的高速发展而来的软件危机却日益严峻,其原因复杂多样。其中,主要原因之一是缺乏程序验证的方法和工具。程序设计的主要步骤有:描述问题、设计程序、实现程序及测试程序。需要注意的是,这里是测试程序的正确性而非证明程序的正确性,这样程序的正确性就不能从根     

重写系统的模块分解

Ｍｉｄｄｅｌｄｏｒｐ和Ｔｏｙａｍａ证明，强加构造原则到项重写系统可获得完备概念的模块性，并且系统分解成的各部分间可共亨函数符号和重量写规则。本文推广他们的结论，当构造性的项重写系统引用定义在其它系统中的函数符号时，完备概念的模块性仍保持。该结论对代数规范和基于项重写的编程语言等方面是很有意义的。     

项重写系统弱基终止性的归纳证明

1.引言项重写系统是一种受到广泛研究和应用的形式计算模型。一个项重写系统由一组称为重写规则的定向等式组成。例如,下面的R是一个由五个重写规则组成的、定义用({0,s})表示的自然数集N上的两倍函数d(x)=2×n:N→N的项重写系统:     

基于项重写的动态可重构系统建模与仿真框架

可重构系统建模与仿真是一项复杂的任务.本文从可重构计算模式的基本特征出发,建立计算与通讯并重的生产者-消费者系统架构,并提取其数据、计算、通讯基本元素,解决运行时的调度和加载问题,形成基于项重写理论的动态可重构计算系统建模框架.最后指出基于本框架进行系统规范描述、系统设计和仿真验证的方法与步骤.并以实例说明了不同的调度策略产生满足不同规范的应用系统,显示了本框架的通用性.     

基于梯形逻辑的联锁系统形式化验证方法

铁路联锁系统设计通常采用梯形逻辑进行建模。为了实现对铁路联锁系统进行形式化验证的目的,根据梯形逻辑的状态变迁语义,将梯形逻辑表示的联锁系统模型转换成模型检测工具NuSMV的语言,并将铁路联锁系统的安全需求表示为计算树逻辑(CTL),最后实现基于NuSMV的铁路联锁系统设计模型的形式化验证。     

高效率重写型程序的设计

本文考虑如何设计高效率(即重写步数较少的)重写型程序。文中以计算Fibonacci数列的程序为例．比较具有相同功能的重写型程序,展示编写高效率重写型程序的可能性。介绍利用动态项重写计算编写高效率重写型程序的直观、简洁的方法。其中．动态项重写计算是项重写系统的元计算模型,其计算同样基于项重写。     

基于重写逻辑的UML模型一致性检查方法

在模型驱动开发的场景下,保证UML模型的一致性具有重要意义,但目前大多数UML／MDA工具仪提供了有限支持。该文提出了一种基于代数重写逻辑的UML模型一致性检查的方法。首先定义了基于两级代数规范的实施构架以分别检查UML模型的没讣时和运行时语义一致性,其次定义了检查包括类图、状态机图和顺序图在内的多图一致性的重写规则。该方法为保持面向可执行的UML模型的一致性提供了有效支持。     

Symbolic chemical system based on abstract rewriting system and its behavior pattern

We develop an abstract computational model, the abstract rewriting system on multisets, called ARMS, to deal with systems with a large number of degree of freedom, like liquids, and to confirm that they can simulate the emergence of the complex behavior of cycles, such as autocatalytic cycles, with their period-doubling and fusion of cycles, which are often found in the emergence of life. Furthermore, we clarify the conditions in which ARMS generates cycles through the theoretical investigation of ARMS.     

The undecidability of self-embedding for term rewriting systems

The self-embedding property of term rewriting systems is closely related to the uniform termination property, since a nonself-embedding term rewriting system is uniform terminating. The self-embedding property is shown to be undecidable and partially decidable. It follows that the nonself-embedding property is not partially decidable. This is true even for globally finite term rewriting systems. The same construction gives an easy alternate proof that uniform termination is undecidable in general and also for globally finite term rewriting systems. Also, the looping property is shown to be undecidable in the same way.     

Formal Semantics and Analysis of Component Connectors in Reo

We present an operational semantics for a component composition language called Reo. Reo connectors exogenously compose and coordinate the interactions among individual components that comprise a complex system, into a coherent collaboration. The formal semantics we present here paves the way for a rigorous study of the behavior of component composition mechanisms. To demonstrate the feasibility of such a rigorous approach, we give a faithful translation of Reo semantics into the Maude term rewriting language. This translation allows us to exploit the rewriting engine and the model-checking module in the Maude tool-set to symbolically run and model-check the behavior of Reo connectors.     

基于RTLinux/Linux的计算机联锁系统可靠性分析

针对计算机联锁系统故障诊断多基于维修人员实际经验,无法实现快速、精准定位故障,基于贝叶斯网络在表达不确定性知识上的优势,提出了一套完善的计算机联锁系统故障的诊断方法和实现流程.首先,运用贝叶斯算法的理论知识,搭建了基于贝叶斯算法的计算机联锁系统故障诊断模型;然后对计算机联锁系统的整体架构和硬件、软件组成进行搭建.最后,...     

基于系统理论过程分析的软件安全性需求分析与验证方法

针对传统系统理论过程分析（STPA）方法缺乏自动化实现手段、自然语言结果分析存在歧义性的问题,提出一种基于STPA的软件安全性需求分析与验证方法。首先,提取软件安全性需求,并利用算法将其转化为形式化表达式;其次,建立状态图模型来描述软件安全控制行为逻辑,并将其转化为程序可读的形式化语言;最后,采用模型检验技术进行形式化验证。结合某武器发射控制系统案例验证了方法的有效性,结果表明,该方法能够实现安全需求分析的自动化生成与形式化验证,解决了传统方法对于人工干预的依赖问题及自然语言描述问题。     

A class of confluent term rewriting systems and unification

The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof.     

基于CPN的进路式联锁调度建模及其分析

提出一种基于有色Petri网(CPN)的进路式联锁调度算法模型,其中包括对联锁调度过程中机车的任务内正常行驶、进路联锁运算、机车驶离任务路线、闯入未开放进路、故障处理恢复等情况建立了清晰的模型。并利用CPN Tools对模型进行仿真验证与分析,结果表明该联锁调度CPN模型正确模拟了井底机车运输调度,对于机车调度是安全可靠的。     

Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications

In this paper, we propose the notion of reducibility of symbols in term rewriting systems (TRSs). For a given algebraic specification, operation symbols can be classified on the basis of their denotations: the operation symbols for functions and those for constructors. In a model, each term constructed by using only constructors should denote an element, and functions are defined on sets formed by these elements. A term rewriting system provides operational semantics to an algebraic specification. Given a TRS, a term is called reducible if some rewrite rule can be applied to it. An irreducible term can be regarded as an answer in a sense. In this paper, we define the reducibility of operation symbols as follows: an operation symbol is reducible if any term containing the operation symbol is reducible. Non-trivial properties of context-sensitive rewriting, which is a simple restriction of rewriting, can be obtained by restricting the terms on the basis of variable occurrences, its sort, etc. We confirm the usefulness of the reducibility of operation symbols by applying them to behavioral specifications for proving the behavioral coherence property.     

Extending model checkers for hybrid system verification: the case study of SPIN

A hybrid system is a system that evolves following a continuous dynamic, which may instantaneously change when certain internal or external events occur. Because of this combination of discrete and continuous dynamics, the behaviour of a hybrid system is, in general, difficult to model and analyse. Model checking techniques have been proven to be an excellent approach to analyse critical properties of complex systems. This paper presents a new methodology to extend explicit model checkers for hybrid systems analysis. The explicit model checker is integrated, in a non‐intrusive way, with some external structures and existing abstraction libraries, which store and manipulate the abstraction of the continuous behaviour irrespective of the underlying model checker. The methodology is applied to SPIN using Parma Polyhedra Library. In addition, the authors are currently working on the extension of other model checkers. Copyright © 2013 John Wiley & Sons, Ltd.