高阶类型化软件体系结构建模和验证及案例

根据权威统计数据，软件测试中发现的70%以上的错误由需求获取或体系结构设计引起.因此，应用软件体系结构在设计阶段的正确性验证非常重要.现有的软件体系结构设计方法不支持需求满足验证，需求满足验证需要其他验证工具的支持.面向主流Web应用软件的体系结构设计及其需求满足验证，提出了一种高阶类型化软件体系结构建模和验证语言（SAML）与软件体系结构建模和验证方法（SAMM）.SAML语言通过定义类型和项的语法及语义，描述软件体系结构中类型和对象的构造，通过定义类型规则及其类型检查算法来判定Γ|-t：T和Γ|-R（T₁，T₂）是否成立.SAMM给出了软件体系结构建模范式，包括构建接口类型M_cls（type interface）、组件M_cmpt（component）、容器M_cont（container）、框M_frm（frame）和框架M_frwk（framework）这5层建模过程，以及生成层内与层间类型之间关系对应的类型规则，同时定义了接口类型方法调用图（G_SA）用以刻画软件体系结构设计要求，定义了类型序列及其正确性用以刻画需求期望的性质，并给出了相应的验证算法.设计实现了基于该方法的原型工具系统SAMVS，其中，模型编辑环境支持应用软件的设计过程，验证环境支持设计满足需求的自动化验证.通过一个实际案例，完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.     

高阶类型化可验证应用系统体系结构建模及案例

随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计无法支持需求满足验证,需求满足验证需要其它验证工具的支持.而应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主动运维.本文面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下,提出了一种高阶类型化模型驱动的可验证应用系统体系结构建模语言（V_ASAML）与可验证应用系统体系结构建模方法（V_ASAMM）.V_ASAML语言通过定义类型和项的语法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定Γ⊦t：T和Γ⊦R（T₁,T₂）是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述组成部分之间的关系和配置.V_ASAMM方法给出了应用系统体系结构建模过程,包括构建M_bd（基本数据类型）、M_bti（基本接口类型）、M_dev（设备类型）和M_frwk（应用系统框架）等四层,以及自动生成层内与层间类型之间关系对应的类型规则,同时定义了设备类型服务调用图（G_DSI）用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统V_ASAMS,其中,建模编辑环境支持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.     

基于余归纳的最小Kripke结构的求解

状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：（1） 对于任意给定的一类Kripke结构（记为K）,在互模拟等价意义下K中最小Kripke结构（记为K₀）的存在唯一性.K₀描述了K中所有Kripke结构的行为而且没有冗余的状态;（2） 对于任意的M∈K（M可能包含无穷多个状态）,在互模拟等价意义下的相对于（M且基于K₀）的最小Kripke结构（记为K_M）的存在唯一性.由此提出一种求解K_M的算法,并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的K_M代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.     

结合可信度的km-means算法

以K-means为代表的聚类算法被广泛地应用在许多领域, 但是K-means不能直接处理不完整数据集. k_m-means是一种处理不完整数据集的聚类算法, 通过调整局部距离计算方式, 减少不完整数据对聚类过程的影响. 然而k_m-means初始化阶段选取的聚类中心存在较大的不可靠性, 容易陷入局部最优解. 针对此问题, 本文引入可信度, 提出了结合可信度的k_m-means聚类算法, 通过可信度调整距离计算, 增大初始化过程中选取聚类中心的可靠性, 提高聚类算法的准确度. 最后, 通过UCI和UCR数据集验证算法的有效性.     

基于距离不等式的K-medoids聚类算法

本文研究加速K-medoids聚类算法,首先以PAM（Partitioning Around Medoids）、TPAM（Triangular Inequality Elimination Criteria PAM）算法为基础,给出两个加速引理,并基于中心点之间距离不等式提出两个新加速定理.同时,以O（n+K²）额外内存空间开销辅助引理、定理的结合而提出加速SPAM（Speed Up PAM）聚类算法,使得K-medoids聚类算法复杂度由O（K（n-K）²）降低至O（（n-K）²）.在实际及人工模拟数据集上的实验结果表明,相对PAM、TPAM、FKMEDOIDS（Fast K-medoids）等参考算法均有改进,运行时间比PAM至少提升0.828倍.     

利用MODIS数据估计中国黄东海区域测深参数

目的 现有关于漫衰减系数的研究大多是在490 nm波段建立反演模型,且未将相关研究与机载激光雷达测深能力建立联系,本文尝试获取测深参数532 nm漫衰减系数K_d(532)和透明度SD(Secchi disk depth),为机载双色激光雷达测深能力的评估和飞行方案的制定提供了重要技术参数。方法 首先分析了测深参数532 nm漫衰减系数K_d(532)和透明度SD对于评估机载双色激光系统测深能力的重要性。利用2003年春季中国黄东海区域的实测光学数据,对现有的漫衰减系数反演模式进行改进,建立了K_d(532)和K_d(490)=的线性关系以及SD和K_d(532)的幂函数关系。结果 根据2003年春季MODIS的490 nm漫衰减系数产品和上述函数关系获取了K_d(532)和SD参数。结论 本文获取测深参数K_d(532)和SD的方法能够用来有效评估该区域机载激光雷达的测深能力,准确性和精度依赖于实测光学数据的精度、分布和数量以及MODIS的K_d(490)产品的准确性。     

基于不相似性度量优化的密度峰值聚类算法

密度峰值聚类（clustering by fast search and find of density peaks,简称DPC）是一种基于局部密度和相对距离属性快速寻找聚类中心的有效算法.DPC通过决策图寻找密度峰值作为聚类中心,不需要提前指定类簇数,并可以得到任意形状的簇聚类.但局部密度和相对距离的计算都只是简单依赖基于距离度量的相似度矩阵,所以在复杂数据上DPC聚类结果不尽如人意,特别是当数据分布不均匀、数据维度较高时.另外,DPC算法中局部密度的计算没有统一的度量,根据不同的数据集需要选择不同的度量方式.第三,截断距离d_c的度量只考虑数据的全局分布,忽略了数据的局部信息,所以d_c的改变会影响聚类的结果,尤其是在小样本数据集上.针对这些弊端,提出一种基于不相似性度量优化的密度峰值聚类算法（optimized density peaks clustering algorithm based on dissimilarity measure,简称DDPC）,引入基于块的不相似性度量方法计算相似度矩阵,并基于新的相似度矩阵计算样本的K近邻信息,然后基于样本的K近邻信息重新定义局部密度的度量方法.经典数据集的实验结果表明,基于不相似性度量优化的密度峰值聚类算法优于DPC的优化算法FKNN-DPC和DPC-KNN,可以在密度不均匀以及维度较高的数据集上得到满意的结果;同时统一了局部密度的度量方式,避免了传统DPC算法中截断距离d_c对聚类结果的影响.     

支持多约束的K-匿名化方法

K-匿名化(K-anonymization)是数据发布环境下保护数据隐私的一种重要方法.目前,K-匿名化方法主要针对单一约束条件进行处理,而实际应用中涉及到大量的多约束条件,使K-匿名化问题更加复杂.如果简单地将单一约束K-匿名化方法应用到多约束情况,会造成大量的信息损失及过低的处理效率.根据多约束之间的关系,通过继承Classfly算法的元组概括过滤思想,提出多约束K-匿名化方法Classfly⁺及相应的3种算法,包括朴素算法、完全IndepCSet算法和部分IndepCSet的Classfly⁺算法.实验结果显示,Classfly⁺能够很好地降低多约束K-匿名化的信息损失,改善匿名化处理的效率.     

基于立体视觉的汽车安全气囊装配精度测评方法

本文提出了一种基于双目立体视觉检测而实现汽车安全气囊装配精度测评的方法,将CCD摄像机提供的待测安全气囊的图像与标准安全气囊的三维数模相结合,建立了汽车安全气囊轮廓检测点的位置公差V_x、V_y、V_z以及点所在轮廓曲线段的形状公差K作为装配精度参数的评价指标,自动完成轮廓尺寸参数的计算,判定待测安全气囊是否合格.实际验证结果表明,所建立的立体视觉安全气囊装配精度测评方法和指标可以快捷精确的评价汽车安全气囊的装配质量.     

RB模型实例集上置信传播算法的收敛性

置信传播算法求解RB（k,n,α,r_c,p）模型实例时非常有效,几乎能够有效求解接近可满足性相变点的难解实例.然而,因子图带有回路的实例,置信传播算法不总有效,常表现为不收敛.对于这种现象,至今缺少系统的理论解释.置信传播算法是最为基础的信息传播算法,对置信传播算法的收敛性分析是其他信息传播算法收敛性分析的重要基础.在RB（k,n,α,r_c,p）模型中,取k=2,α>（1/k）,r_c>0均为常数,且满足ke^{-（α/（r_c））}≥1.证明了如果p∈（0,n^-2α）,则置信传播算法在RB（k,n,α,r_c,p）模型产生的随机实例集上高概率收敛.最后,在RB（k,n,α,r_c,p）模型上选取了几组不同的数据进行数值模拟,实验结果表明该结论有效.当问题规模n增大时,在RB（k,n,α,r_c,p）模型的可满足区域,实验收敛区间趋于一个固定范围,而理论收敛区间逐渐变窄.原因在于,RB（k,n,α,r_c,p）模型是一个具有增长定义域的随机CSP实例产生模型,不协调赋值的数目与参数p及问题规模n有关.     

Lumped model of a non-linear distributed system by finite element method

The finite element method has been used to find an approximate lumped parameter model of a non-linear distributed parameter system. A one dimensional non-linear dispersion system is considered. The space domain is divided into a finite set of k elements. Each element, has n nodes. Within each element the concentration is represented by C(x,t)^(e) = [N][C] ^T where [N] = [n₁(x),n₂(x), [tdot] n_n(x)] and [C] = [C₁(t),C₂(t), [tdot] C_n(t)]. By using Galerkin's criterion a set of (k × n ? n+ 1) first order differential equations are obtained for C_i(t). These equations are solved by an iterative method. The concepts are illustrated by an example taking five three-node elements in the space domain. The results are compared with those obtained by a finite difference method. It is shown that the finite element method can be used effectively in modelling of a distributed system by a lumped system.     

Rupture degree of graphs

We introduce a new graph parameter, the rupture degree. The rupture degree for a complete graph K _n is defined as 1?n, and the rupture degree for an incomplete connected graph G is defined by r(G)=max{ω(G?X)?|X|?m(G?X):X?V(G), ω(G?X)>1}, where ω(G?X) is the number of components of G?X and m(G?X) is the order of a largest component of G?X. It is shown that this parameter can be used to measure the vulnerability of networks. Rupture degrees of several specific classes of graphs are determined. Formulas for the rupture degree of join graphs and some bounds of the rupture degree are given. We also obtain some Nordhaus–Gaddum type results for the rupture degree.     

Controller reduction via stable factorization and balancing

A controller reduction procedure based on a representation of a controller as a matrix function defined using stable proper transfer functions and employing a balancing technique is studied in this paper. For a certain right coprime factorization of an LQG designed controller K(s) = N(s)D^-1(s), we approximate using a balancing technique the pair [D(s), N(s)]^T by a low-order pair [D₁(s), N₁(s)]^T defining a factorization of the reduced-order controller K ₁(s) = N₁(s)D₁ ^-1(s). We show that reducing the controller order in this way is motivated in a natural way, which leads to the expectation of both good stability properties and good accuracy of approximation of closed-loop behaviour. This is also demonstrated in some examples.     

Existence and efficient construction of fast Fourier transforms on supersolvable groups

The linear complexityL _K(A) of a matrixA over a fieldK is defined as the minimal number of additions, subtractions and scalar multiplications sufficient to evaluateA at a generic input vector. IfG is a finite group andK a field containing a primitive exp(G)-th root of unity,L _K(G):= min{L _K(A)|A a Fourier transform forKG} is called theK-linear complexity ofG. We show that every supersolvable groupG has amonomial Fourier Transform adapted to a chief series ofG. The proof is constructive and gives rise to an efficient algorithm with running timeO(|G|²log|G|). Moreover, we prove that these Fourier transforms are efficient to evaluate:L _K(G)8.5|G|log|G| for any supersolvable groupG andL _K(G)1.5|G|log|G| for any 2-groupG.     

Inducing Constructor Systems from Example-Terms by Detecting Syntactical Regularities

We present a technique for inducing functional programs from few, well chosen input/output-examples (I/O-examples). Potential applications for automatic program or algorithm induction are to enable end users to create their own simple programs, to assist professional programmers, or to automatically invent completely new and efficient algorithms. In our approach, functional programs are represented as constructor term rewriting systems (CSs) containing recursive rules. I/O-examples for a target function to be implemented are a set of pairs of terms (F(i_i),o_i) meaning that F(i_i)—denoting application of function F to input i_i—is rewritten to o_i by a CS implementing the function F. Induction is based on detecting syntactic regularities between example terms. In this paper we present theoretical results and describe an algorithm for inducing CSs over arbitrary signatures/data types which consist of one function defined by an arbitrary number of rules with an arbitrary number of non-nested recursive calls in each rule. Moreover, we present empirical results based on a prototypical implementation.     

Control sets on grammars

Given a setC of strings of rewriting rules of a phrase structure grammarG, we consider the setL _c (G) of those words generated by leftmost derivations inG whose corresponding string of rewriting rules is an element ofC. The paper concerns the nature of the setL _c (G) whenC andG are assumed to have special form. For example, forG an arbitrary phrase structure grammar,L _c (G) is an abstract family of languages ifC is an abstract family of languages, andL _c (G) is bounded ifC is bounded.Research sponsored in part by the Air Force Cambridge Research Laboratories, Office of Aerospace Research, USAF, under Contract F1962867C0008, and by the Air Force Office of Scientific Research, Office of Aerospace Research, USAF, under AFOSR Grant No. AF-AFOSR-1203-67.     

数据仓库系统中层次式Cube存储结构

区域查询是数据仓库上支持联机分析处理(on-line analytical processing,简称OLAP)的重要操作.近几年,人们提出了一些支持区域查询和数据更新的Cube存储结构.然而这些存储结构的空间复杂性和时间复杂性都很高,难以在实际中使用.为此,提出了一种层次式Cube存储结构HDC(hierarchical data cube)及其上的相关算法.HDC上区域查询的代价和数据更新代价均为O(log^dn),综合性能为O((logn)^2d)(使用C_qC_u模型)或O(K(logn)^d)(使用C_qn_q+C_un_u模型).理论分析与实验表明,HDC的区域查询代价、数据更新代价、空间代价以及综合性能都优于目前所有的Cube存储结构.     

Design of digital PID controllers using the parameter space approach

In this paper, a parameter space approach is taken for designing digital PID controllers. The stability domains of the coefficients of the controllers are computed. The existing continuous-time results are extended to the case of discrete-time systems. In this approach, the stability region is obtained in the plane of two auxiliary controller coefficients by assuming a fixed value for a third auxiliary controller coefficient. The stability region is defined by several line segments or equivalently by several linear equalities and inequalities. Then, through mapping from the auxiliary coefficient space to the original controller coefficient space, exact stability domain in the (K_P ???K_I ???K_D ) space is obtained. The method is also extended for locating the closed-loop poles of PID control systems inside the circles with arbitrary radii, centred at the origin of the z-plane. The results can be used in the design of dead-beat control systems.     

A novel neural Smith chart for use in microwave circuitry

In this article, briefly the Smith chart is mapped with an artificial neural network (ANN) covering its whole details to be exploited CAD of the microwave circuitry. Thus, relative to the similar works in the existing literature, this article provides the continuous Smith chart domain to facilitate the “Smith chart” methodology in solving the highly nonlinear transformation equations between the rectangular impedance and polar reflection planes for an infinite number of passive impedance to be used in design tasks of the microwave circuits. Data ensembles for the training and testing processes are obtained from the systematically selected locations on the Smith chart with the adaptive radius sampling algorithm. The ANN architecture is also simple, which consists of the two simple multilayer perceptron (MLP) modules with the common inputs which are the termination Z_S = R_S + jX_S, line {?, Z₀} operation bandwidth B between the defined f_min, f_max and the dielectric ε. Briefly, the outputs of these ANN modules are the standing waves and the impedance transformation, which are the characteristic features of the transmission line circuits. Activation of the hidden layers of the modules are performed by the tangential‐sigmoid type of function while the output layers are activated linearly. Furthermore, the neural unit element (NUE) is defined by the two independent neural networks as problems in the forward and reverse directions to be incorporated into the analysis and design algorithms of the unit element (UE). This can also be considered as solving the simultaneous nonlinear equation set for (?, Z₀) parameters of the required impedance transformations Z_OUT(ω) = R_OUT (ω) + X_OUT (ω) from the given complex termination Z_S = R_S + jX_S. Applications of the Neural Smith chart are given by the numerous examples with the proved accuracy. Thus it has been verified that this neural Smith chart can be exploited for the whole classical transmission line theory including impedance matching. © 2008 Wiley Periodicals, Inc. Int J RF and Microwave CAE, 2009.