基于混合自动机的随机噪声电路动态特性分析

在集成电路非线性随机噪声的分析中应用Petri网技术,需要对原有的Petri网从定义和变迁发射规则方面等进行统计特性与连续特性的拓展研究和补充.并且基于噪声的随机非线性特性分析目的需求,拓展了传统的Petri网,提出了混合随机Petri网(Hybrid Statistical Petri Net,HSPN)模型分析方法.通过分析非线性电路的混合自动机模型,增加Petri网随机参数变迁描述能力,针对电路噪声特点,确定适合HSPN的随机动态特性分析模型.通过实例电路说明验证HSPN的建模方法,并与SPICE仿真软件进行比较,验证了该方法的精度和可行性.     

基于事务断言验证及SDH芯片验证平台

提出了基于事务断言验证技术,用属性说明语言(Property Specification Language,PSL)描述系统的属性,用事务进行系统的验证,通过编程语言接口机理和工具控制语言来控制验证中PSL断言的状态,使得基于PSL的断言验证可以事务的形式灵活地应用。采用该技术建立了同步数字体系(Synchronous Digitial Hierarchy,SDH)验证平台,验证了超过100万门交换芯片的功能,实践表明,该方法极大的提高了验证覆盖率和验证效率。     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

PSL构造双向交换自动机及非确定自动机的方法

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

混合信号电路可测性结构研究

在深入研究IEEE1149.1及IEEE1149.4标准的基础上,对基于边界扫描的混合信号电路的可测性结构进行了探索;对所设计混合信号电路可测性结构用可编程逻辑器件及外部模拟电路进行硬件的具体实现,构建了验证模块DOT4MBST;同时以DOT4MBST与IEEE1149.4工作组提供的标准验证芯片为核心对同结构的混合信号电路构建了验证电路;最后对验证模块DOT4MBST及验证电路进行了测试验证,测试结果表明,所设计的混合信号电路可测性结构是可行的,并可以应用到混合信号电路中提高电路的可测试性。     

基于广义特征分析与边界扫描技术的混合信号测试系统

分析了用于模数混合电路的边界扫描测试技术的工作机制对测试主控系统的功能需求,提出了一种基于微机的符合IEEE1149.4标准的混合信号边界扫描测试主控系统。所采用的广义特征分析法利用库函数映射的思想,将传统的各种故障字典进行统一描述。实践证明,该方法对模数混合电路的测试是行之有效的。     

混合信息的多属性决策研究

针对实数型、区间型、三角模糊数和不确定性语言组成的混合多属性决策问题,首先分析了混合属性信息的度量关系,并结合混合属性特点讨论了各属性之间的转化关系,将混合属性统一到区间属性信息框架下,实现了混合属性之间的不确定性度量。其次基于灰色关联的区间多属性决策方法,计算决策方案的贴近度,根据贴近度对混合多属性信息转化后的区间信息进行决策。最后结合武器威胁程度决策判定,验证了所提出的混合多属性决策方法的实用性。     

基于自动机的构件实时交互行为的形式化模型

采用形式化方法对复杂实时构件系统交互行为进行描述和验证,对于提高系统的正确性、可靠性等可信性质具有重要意义.分析了基于进程代数和自动机的构件交互行为形式化建模方法各自的优缺点,在此基础上提出了基于时间构件交互自动机的建模方法,给出了时间构件交互自动机的相关定义、组合和验证算法.时间构件交互自动机引入了时间限制、时间代价、时间代价计算半环、构件组合层次等概念,既能够描述构件交互情况,又能够清楚地表示出构件系统的体系结构信息和实时信息,便于对系统进行描述和验证.最后,结合具体应用给出了应用示例.     

基于混合自动机的J2ME代码自动生成技术

在概述混合自动机理论的基础上,给出了它的一种基于xml语言的形式描述,并利用这种描述规范提出了一种基于混合自动机的模型驱动的开发方式,结合一个具体的应用实例进行开发,给出了根据模型描述文件生成可以编译运行的J2ME代码的原理以及关键步骤,以及需要注意的问题。     

基于EEMD与矩阵分形的自动机故障诊断方法

针对自动机振动响应信号非线性、瞬态和冲击特性,提出基于聚合经验模态分解(EEMD)和矩阵分形相结合的自动机故障诊断方法。首先对采集到的自动机各种工况信号采用EEMD分解的方法对其进行分解,通过对分解得到的固有模态函数(IMF)分量信号进行广义维数计算,得到每个工况广义维数分形矩阵,发现不同工况下的分形矩阵有较大差别。通过计算待检测信号与样本信号之间的的相关系数,采用折线图进行直观比较,确定待检测信号的故障类别。验证了该方法能有效地应用在自动机故障诊断中。     

Time Domain Verification of Oscillator Circuit Properties

The application of formal methods to analog and mixed signal circuits requires efficient methods for constructing abstractions of circuit behaviors. This paper concerns the verification of properties of oscillator circuits. Generic monitor automata are proposed to facilitate the application of hybrid system reachability computations to characterize time domain features of oscillatory behavior, such as bounds on the signal amplitude and jitter. The approach is illustrated for a nonlinear tunnel-diode circuit model using PHAVer, a hybrid system analysis tool that provides sound verification results based on linear hybrid automata approximations and infinite precision computations.     

Computational techniques for hybrid system verification

This paper concerns computational methods for verifying properties of polyhedral invariant hybrid automata (PIHA), which are hybrid automata with discrete transitions governed by polyhedral guards. To verify properties of the state trajectories for PIHA, the planar switching surfaces are partitioned to define a finite set of discrete states in an approximate quotient transition system (AQTS). State transitions in the AQTS are determined by the reachable states, or flow pipes, emitting from the switching surfaces according to the continuous dynamics. This paper presents a method for computing polyhedral approximations to flow pipes. It is shown that the flow-pipe approximation error can be made arbitrarily small for general nonlinear dynamics and that the computations can be made more efficient for affine systems. The paper also describes CheckMate, a MATLAB-based tool for modeling, simulating and verifying properties of hybrid systems based on the computational methods previously described.     

构件式实时系统建模与验证研究

在复杂的实时系统开发中使用构件式设计方法已成为目前软件开发领域中的研究热点,如何有效地验证实时软件的设计是否满足给定的时间需求并降低验证过程的复杂度,是实时计算领域中的主要挑战之一.文中对构件接口模型进行时间扩展,提出了时间接口模型,并将其用于构件接口交互行为的形式化建模.在接口自动机理论的的基础上进一步提出了时间接口自动机模型用于描述时间接口交互下构件的行为及组合方法,通过消除错误状态产生组合模型来约减构件时间接口自动机模型的积,并在约减的模型上进行性质检验,降低了分析复杂度,有效地应对状态空间爆炸问题.为了说明论文建议的方法,详细讨论了一个简单的、贯穿整篇论文的示例系统.     

Symbolic model checking APSL

Property specification language (PSL) is a specification language which has been accepted as an industrial standard. In PSL, SEREs are used as additional formula constructs. In this paper, we present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. Then, we extend the LTL symbolic model checking algorithm to that of APSL, and then present a tableau based APSL verification technique, which can be easily implemented via the BDD based symbolic approach. Moreover, we implement an extension of NuSMV, and this adapted version supports symbolic model checking of APSL. Experimental results show that this variant of PSL can be efficiently verified. Henceforth, symbolic model checking PSL can be carried out by a transformation from PSL to APSL and symbolic model checking APSL.     

Symbolic model checking APSL

Property specification language (PSL) is a specification language which has been accepted as an industrial standard. In PSL, SEREs are used as additional formula constructs. In this paper, we present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. Then, we extend the LTL symbolic model checking algorithm to that of APSL, and then present a tableau based APSL verification technique, which can be easily implemented via the BDD based symbolic approach. Moreover, we implement an extension of NuSMV, and this adapted version supports symbolic model checking of APSL. Experimental results show that this variant of PSL can be efficiently verified. Henceforth, symbolic model checking PSL can be carried out by a transformation from PSL to APSL and symbolic model checking APSL.     

On simulation-based probabilistic model checking of mixed-analog circuits

In this paper, we consider verifying properties of mixed-signal circuits, i.e., circuits for which there is an interaction between analog (continuous) and digital (discrete) values. We use a simulation-based approach that consists of evaluating the property on a representative subset of behaviors and answering the question of whether the circuit satisfies the property with a probability greater than or equal to some threshold. We propose a logic adapted to the specification of properties of mixed-signal circuits in the temporal domain as well as in the frequency domain. We also demonstrate the applicability of the method on different models of Δ–Σ modulators for which previous formal verification attempts were too conservative and required excessive computation time.