软件模型检测中的抽象

软件模型检测对保证软件的正确性和可靠性具有十分重要的意义，而抽象是减轻模型检测中状态爆炸问题最重要的技术之一。本文综述当前广泛应用于软件模型检测中的抽象技术，介绍了该领域的进展及研究方向。     

基于层次单元划分的软件模型检测技术研究

通过对近年来软件模型检测领域流行的几种技术进行综述,提出了一种基于层次单元划分,使用引导式搜索方式的软件模型检测方案。本方案分为预处理、单元划分、状态空间搜索三个阶段,其中使用on-the-fly技术提高了搜索性能。实验证明,该方案在解决状态爆炸问题上有较好的效果。     

具有公平性约束的CTL部分状态空间模型检测

检测部分状态空间是近年来出现的有效解决状态爆炸的模型检测技术，部分Kripke 结构是描述部分状态空间的形式框架。文章主要讨论一类具有公平性约束条件的CTL（计算树逻辑）模型检测问题。定义了部分公平Kripke结构和公平序，分别来表征部分公平状态空间和它们之间的序关系。并给出相应的3值CTL语意和相关定理来说明部分状态空间模型检测技术同样适用于具有公平性约束条件的CTL模型检测问题。     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

多主体系统时态认知规范的"On the Fly"模型检测算法研究

时态认知逻辑已被广泛应用于分布式系统和协议的规范描述，模型检测时态认知规范已成为一个新的研究领域，因此着重研讨时态认知规范的“On the Fly”模型检测算法．在“On the Fly”模型检测时态逻辑描述规范的基础上，根据自动机理论、深度优先方法和知识的语义，提出了“On the Fly”模型检测时态认知规范的算法，该算法在模型检测带有知识算子的时态规范时，在找到一个反例之前，往往只需构造系统的部分甚至小部分状态空间，从而避免了时态认知规范的模型检测中内存不足和状态爆炸等问题，实现了“On the Fly”模型检测时态认知规范，并且算法的复杂性是多项式时间的．最后，通过该方法在验证TMN密码协议中的应用来作为一个例子说明该方法的有效性．     

面向随机模型检验的模型抽象技术

随机模型检验是经典模型检验理论的延伸和推广,由于其结合了经典模型检验算法和线性方程组求解或线性规划算法等,并且运算处理的是关于状态的概率向量而非经典模型检验中的位向量,所以状态爆炸问题在随机模型检验中更为严重.抽象作为缓解状态空间爆炸问题的重要技术之一,已经开始被应用到随机模型检验领域并取得了一定的进展.以面向随机模型检验的模型抽象技术为研究对象,首先给出了模型抽象技术的问题描述,然后按抽象模型构造技术分类归纳了其研究方向及目前的研究进展,最后对比了目前的模型抽象技术及其关系,总结出其还未能给出模型抽象问题的满意答案,并指出了有效解决模型抽象问题未来的研究方向.     

基于动态内存和状态管理的模型检测新方法

模型检测是并发系统验证的主要形式化方法之一,但其存在因状态空间爆炸而导致内存不够的问题,这也是大规模并发系统验证的瓶颈.很多研究人员尽管做了很多相关研究,但仍然没有很好地解决这个问题.在研究动态内存和状态管理的基础上,提出了一种新的模型检测方法,避免了因为内存不足而无法模型检测的问题.     

基于Petri网的模型检测研究

模型检测是关于系统属性验证的算法和方法.它通常采用状态空间搜索的方法来检测一个给定的计算模型是否满足某个用时序逻辑公式表示的特定属性.系统模型的状态空间的爆炸问题是模型检测所面临的主要问题,其主要原因是系统自身的并发特性和状态变迁的语义交织对基于Petri网的模型检测理论和验证技术进行了较为详细的研究,着重探讨了基于Petri网状态可达图的偏序简化和偏序语义技术、基于自动机的模型检测算法、基于Petri网的状态聚合法以及基于系统对称性的参数化和符号模型检测技术，并给出了研究思路以及未来所要进行的重点研究工作.模型检测技术已在通信协议和硬件系统的验证等领域得到成功应用，并且随着各种状态空间简化技术和模型检测算法的不断优化，其在其他应用领域也展示出广泛的应用前景.     

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

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

基于Verds的C语言子集的模型检测方法

针对现今软件使用逻辑错误的问题越来越多的出现,提出了对最流行最普遍的编程语言1语言子集的模型检测方法的研究．采用基于Verds工具的模型,运用C语言子集转化成Verds模型的算法,结合Verds工具和MAGIC工具实现模型检测．引入反例引导的抽象精化方法使模型检测解决状态爆炸的问题．     

Call for Papers The 6^th International Conference on Grid and Cooperative Computing

Recent years have seen rapid advances in various grid-related technologies, middleware, and applications. The GCC conference has become one of the largest scientific events worldwide in grid and cooperative computing. The 6th international conference on grid and cooperative computing (GCC2007) Sponsored by China Computer Federation (CCF),Institute of Computing Technology, Chinese Academy of Sciences (ICT) and Xinjiang University ,and in Cooperation with IEEE Computer Soceity ,is to be held from August 16 to 18, 2007 in Urumchi, Xinjiang, China.     

法律信息库系统

本文分析了法律数据库的结构和特点，介绍了采用面向对象设计方法和超文本数据库技术开发和实现法律信息库系统将作为重要网络资源之一为不同用户进行法律咨询服务。     

International Journal of Automation and Computing Table of Contents

正~~     

Information for authors

正SCIENCE CHINA Information Sciences(Sci China Inf Sci),cosponsored by the Chinese Academy of Sciences and the National Natural Science Foundation of China,and published by Science China Press,is committed to publishing highquality,original results of both basic and applied research in all areas of information sciences,including computer science and technology;systems science,control science and engineering(published in Issues with odd numbers);information and communication engineering;electronic science and technology(published in Issues with even numbers).Sci China Inf Sci is published monthly in both print and electronic forms.It is indexed by Academic OneFile,Astrophysics Data System(ADS),CSA,Cabells,Current Contents/Engineering,Computing and Technology,DBLP,Digital Mathematics Registry,Earthquake Engineering Abstracts,Engineering Index,Engineered Materials Abstracts,Gale,Google,INSPEC,Journal Citation Reports/Science Edition,Mathematical Reviews,OCLC,ProQuest,SCOPUS,Science Citation Index Expanded,Summon by Serial Solutions,VINITI,Zentralblatt MATH.     

Erratum to: Fast global kernel fuzzy c-means clustering algorithm for consonant/vowel segmentation of speech signal

正Erratum to:J Zhejiang Univ-Sci C(ComputElectron)2014 15(7):551-563doi:10.1631/jzus.C1300320The original version of this article unfortunately contained mistakes.Algorithm 6 should be as follows:Algorithm 6 FGKFCM-F clustering Input:(1)X={x_1,x_2,…,x_N},,x_iR~d,i=1,2,…,N,the dataset;(2)C,1C≤N,the number of clusters;(3)ε0,the stopping criterion;     

Journal of Zhejiang University-SCIENCE C (Computers & Electronics) Total contents

正~~     

磨机负荷专家控制系统设计及仿真研究

磨矿过程的大滞后和时变性等特点,致使对磨机负荷的最佳工作点很难进行稳定、高效的控制,针对以上情况,借鉴生物界的免疫反馈原理和遗传算法,利用模糊控制可以有效地实现对非线性、纯滞后、复杂的对象进行控制的优点,并结合PID与自寻优方法,设计出磨机负荷专家控制系统,用VB编写OPC客户端及控制程序,实现对磨机负荷的动态优化控制;试验结果表明,文章提出的控制策略能够增强系统的稳定性,且在干扰存在的情况下也能很好的跟随系统的参数变化,在提高磨机台时产量的同时增加了矿厂的经济效益.     

基于人工蜂群的无线传感器网络能耗均衡算法

由于无线传感器网络中的节点链路状况、数据传输能耗及节点剩余能量的限制,造成网络中部分感知节点寿命缩短,影响网络生存周期,提出了一种基于人工蜂群算法的WSNs能耗均衡算法,优化网络能耗均衡,从而提高网络寿命;文章给出了网络能耗相应的数学模型及优化求解算法,介绍人工蜂群算法的寻找食物过程,阐述了人工蜂群算法在网络能耗均衡方面的实现步骤;通过实验仿真证明,文章提到的算法与LEACH分簇算法、蚁群优化算法相比,具有更好的能耗和负载均衡能量、丢包率和时延性,有效地提高了网络生存周期.     

Thermodynamic modeling of the Al–Bi,Al–Sb,Mg–Al–Bi and Mg–Al–Sb systems

All available thermodynamic and phase diagram data of the binary Al–Bi and Al–Sb systems and ternary Mg–Al–Bi and Mg–Al–Sb systems were critically evaluated, and all reliable data were used simultaneously to obtain the best set of the model parameters for each ternary system. The Modified Quasichemical Model used for the liquid solution shows a high predictive capacity for the ternary systems. The ternary liquid miscibility gaps in the Mg–Al–Bi and Mg–Al–Sb systems resulting from the ordering behaviour of the liquid solutions can be well reproduced with one additional ternary parameter. Using the optimized model parameters, the experimentally unexplored portions of the Mg–Al–Bi and Mg–Al–Sb ternary phase diagrams were more reasonably predicted. All calculations were performed using the FactSage thermochemical software package.