基于实时自动机的连续时段演算的验证

时段演算是描述和推导嵌入式实时系统和混成系统性质的一种区间时态逻辑.扩展线性时段不变式是时段演算的重要子集.针对实时自动机,提出一种连续时间语义下扩展线性时段不变式的有界模型检验方法.该方法将扩展线性时段不变式的有界模型检验问题转化为量词线性算术公式的正确性问题,从而可以采用量词消去技术进行求解.首先,运用符号化的思想,在实时自动机上利用深度优先搜索找到所有满足观测时长约束的符号化路径片段;然后,将每条符号化路径片段转化为一个量词线性算术公式;最后,利用量词消去工具求解.与已有工作相比,基于实时自动机设计了验证算法.另外,降低了验证复杂度,并且加速了验证过程的实际速度.     

具体反例生成与图形化显示系统

模型检测是用来验证系统模型是否满足所期望性质的一种形式化方法,模型检测相对于其它的模型检验方法有两个显著的特点,一个是它对模型进行检测的过程是自动化的,另一个是当系统不满足所验证的性质时,它会给出一条反例路径,这条反例路径可以为系统修正提供帮助．本文研究的重点就是如何使这条反例路径的生成在高效的同时其反例信息又直观易懂,为系统修正带来更方便快捷的帮助．本文中实现了具体反例生成与图形化显示系统（简称CCGS）,它能快速生成离散语义下具体反例并图形化显示时间自动机沿着该具体反例的运行过程．实验结果表明CCGS能够快速生成具体反例路径信息,并且能够图形化显示具体反例信息,为系统修正提供更直观的信息,提高系统的正确性和安全性．     

无穷状态系统可覆盖性分析算法

针对良序结构迁移系统可覆盖性分析计算成本高的问题,提出一种运用有限状态模型检验技术解决无穷状态系统可覆盖性问题的算法.首先将良序结构迁移系统划分为不同权值限定下的一系列有限状态机模型;然后采用最新的模型检验技术增量式地计算不同权值下模型的可达状态空间上逼近,得到可覆盖的反例路径或证明该系统不可覆盖.实验结果表明,该算法在同等计算时间限制下能够解决更多的测试样例;在1 GB内存限制下,可以解决97.2%的测试样例,超过同类算法的2倍.     

基于不完全Kripke结构三值逻辑的模型检验

模型检验技术是形式化验证中比较成熟的技术，但随着设计系统规模的增加，状态爆炸已成为其发展的一个主要问题.为解决此问题，本文提出对系统进行抽象，建立不完全的状态模型，在此状态模型上来验证表示其属性的逻辑公式.这样一个逻辑公式的真值除了真、假外，还出现了第三种情况：未知，即在这个状态模型下无法确定其真值，需要更多的状态信息才能确定.本文还讨论了二值逻辑的模型检验技术，在此基础上给出了基于不完全状态空间的三值逻辑的模型检验算法，此算法与二值逻辑模型检验算法相比，没有带来时间复杂度的增加，最后给出了三值逻辑模型检验算法的应用.     

SMV的观察迁移系统的模型检测分析

模型检验技术是开发高可信系统的重要途径.提出了一种基于定理证明的模型验证方法,并实现了工具验证.它以代数规约语言CafeOBJ描述系统的无限状态并把它转换成有限状态的SMV规约.通过观察迁移系统,证明产生的SMV规约的反例即CafeOBJ规约的反例,来找出开发早期阶段的系统的潜在错误,从而避免时间、金钱的耗费及重复性的劳动.     

基于一阶迁移系统的限界模型检测工具实现

为了简化在限界模型检测过程中模型的建立过程,给出了一种采用基于一阶迁移系统语言的模型建立方法,并在此一阶迁移系统语言中加入了通道的功能,增强了描述能力.然后在此基础上完成了一个以基于插值和k步归纳的限界验证算法为核心的模型检测工具(BMCF),最后利用该工具对常见的互斥协议,简单数据传输协议的性质进行了分析与验证.结果表明,利用该工具对系统进行建模具有方便直观的特点,并借助实现的验证算法能高效的检验性质的正确性,如果性质不成立工具还会给出反例提示.     

一种基于扩展不完全Kripke结构的三值逻辑模型检测方法

多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。     

基于反例确认的CPS不确定性模型校准

信息物理系统被广泛应用于众多关键领域,例如工业控制与智能制造.作为部署在这些关键领域中的系统,其系统质量尤为重要.然而,由于信息物理系统自身的复杂性以及系统中存在的不确定性（例如系统通过传感器感知环境时的偏差）,信息物理系统的质量保障面临巨大挑战.验证是保障系统质量的有效途径之一,基于系统模型与规约它可以证明系统是否满足要求的性质.现有一些信息物理系统的验证工作也取得了显著进展,例如模型检验技术就被已用工作用于验证系统在不确定性影响下的行为是否满足性质规约,并在性质违反的情况给出具体的反例.这些验证工作的一个重要输入就是不确定性模型,它描述了系统中不确定性的具体情况.而实际中要对系统中不确定性精确建模却并非易事,因此验证中使用的不确定性模型很可能与实际不完全相符,这将导致验证结果不准确并与现实偏离.针对这一问题,本文提出了一种基于反例确认的不确定性模型校准方法,来进一步精化验证结果以提高其准确度.首先通过确认反例在系统的执行中能否被触发来判断验证使用的不确定性模型是否精确.对于不精确的模型再利用遗传算法进行校准,并根据反例确认的结果来构造遗传算法的适应度函数以指导搜索,最后结合假设检验来帮助决定是否接受校准后的结果.在代表案例上的实验结果表明了我们提出的不确定性模型校准方法的有效性.     

模态转移系统的三值逻辑模型检验

分析了现有的模型检验技术应用于模态转移系统的三值逻辑公式的模型检验中存在的问题.提出了把模态转移系统转换成Kripke结构的算法以及三值逻辑公式转换成2个二值逻辑的算法,经过转换后可用现有的模型检验技术进行模型检验.用该算法转换后,状态数、转移数和原子命题数目与原模型呈线性关系,没有增加模型检验的复杂度.     

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

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

Semantics and verification of monitors and systems of monitors and processes

In this paper we present a sound and complete semantics for the monitor concept of C.A.R. Hoare. First a method for specification of monitors, introduced by O.-J. Dahl, is reviewed. This method is based on the relation between the historic sequence of monitor procedure calls and the historic sequence of monitor procedure exits. Based on such specifications and our new monitor semantics we present a method by which it is possible to prove that a concrete monitor is an implementation of an abstract one. In the last part of the paper an axiomatic semantics for systems of concurrent processes and monitors is introduced. The method supports verification by separation of concerns: Properties of the communication to and from each process are proven in isolation by a usual Hoare style axiomatic semantics, while abstract monitors are also specified in isolation by the method reviewed in the first part of the paper. These properties of the components of the system are then used in a new proof rule to conclude properties of the complete system. Stein Gjessing received a Ph.D. (actually a Dr. philos.) from the University of Oslo (Norway) in 1985. Presently he is an Associate Professor at the Institute of informatics, University of Oslo, Norway. Dr. Gjessings research interests are in the area of concurrent and distributed programming, operating systems, formal specification and verification and programming languages.     

Models and Complexity of Problems of Design and Reconstruction of Telecommunication and Transport Systems

This article considers network synthesis problems arising in the design and exploitation of telecommunication and transportation systems. A formalization of network synthesis problems on graphs is proposed in which constraints on cut capacities are given and possibilities of failing some network components are taken into account. Approaches to the solution and analysis of the complexity of the considered problems are described.     

Teamcenter与NX集成客户化定制技术研究与实现

PDM产品实施过程中一项重要工作是系统集成与客户化定制。对Teamcenter Engineering(简称Teamcenter)与NX系统集成客户化定制中业务建模、属性映射等相关技术进行了研究,提出了Teamcenter与NX集成客户化定制的技术思路,并以客户化定制NX工程图纸标题栏为例,介绍了Teamcenter与NX集成定制实现的关键步骤及方法。     

椭圆拉伸变形长短轴的计算及应用

在CAD应用软件程序编制中,椭圆的长短轴是很重要的参数。应用相关数学知识推导出6个计算公式,可利用这些公式确定椭圆沿坐标轴拉伸变形后的长短轴大小与位置并在CAD软件中实现与之相关的功能。     

IPSEC与防火墙协同工作设计与实现

IPSEC提供网络层的安全服务，通过对IP报文的加密和验证，保证数据在传输过程中的安全．由于IPSEC封装了报文中一些重要信息，使得IPSEC与防火墙不能同时有效地工作．本文提出一种分层IPSEC(Layered IP Security，L_IPSEC)思想，即将协议头和数据部分分别进行安全处理．并将这种分层思想与分布式处理技术结合，设计与实现一种IPSEC与防火墙协同工作方案．     

智能业务和软交换互通的设计与实现

电信业的快速发展及下一代网络的全面建设促进智能业务与软交换实现互通。文中首先介绍了互通的种类和方案，并重点讲述了智能网和软交换互通过程中模型的重要部分——软交换侧的SSP。在此基础上，提出了智能网和软交换互通的实现方案，并且以智能用的典型业务FPH为例简明分析了方案，对利用业务服务器实现软交换中的智能业务进行了插述和分析。     

Kohonen与Madaline用于解析重叠光谱测定钨和钼

首先应用Kohonen网络对钨、钼的混合吸收光谱进行波长选择，在全光谱中优选最能代表光谱特征的波长，被选波长处吸光度作为Madaline网络的输入，设定输出目标函数为G（λ）＝∑Aiexp[-4(ln20）(λ-t）^2/2]，进行解析重叠光谱，同时测定了钨和钼，该法利用特征光谱代表全谱进行光谱解析，减少了解析光谱中大量的数据。     

智能业务和软交换互通的设计与实现

电信业的快速发展及下一代网络的全面建设促进智能业务与软交换实现互通.文中首先介绍了互通的种类和方案,并重点讲述了智能网和软交换互通过程中模型的重要部分--软交换侧的SSP.在此基础上,提出了智能网和软交换互通的实现方案,并且以智能网的典型业务FPH为例简明分析了方案,对利用业务服务器实现软交换中的智能业务进行了描述和分析.     

Binary perfect and extended perfect codes of lengths 15 and 16 and of ranks 13 and 14

Inaccuracies in computations in the paper of the authors on classification of perfect binary codes of lengths 15 and 16 and of rank 13 are fixed. An explicit construction of all extended perfect codes of length 16 and rank 13 with a given kernel size is presented. Perfect binary codes of length 15 and rank 14 obtained by the general doubling construction are classified.