共查询到20条相似文献，搜索用时 281 毫秒
1.
实时互斥协议是一类重要且复杂的系统协议,其性质分析工作通常是通过数学方法来进行,不利于使用与推广。针对这一问题,提出基于形式化方法的实时互斥协议验证技术。采用时间自动机对一个典型的实时互斥协议进行建模,并定义了它的语义。同时,分析了该协议所应具有的性质并转化为形式化公式。最后,使用模型检测工具UPPAAL对协议性质进行了自动验证。验证结果表明,该协议虽然满足互斥与无死锁两个基本性质,但无法保证进程活性。该方法具有自动化程度高、验证速度快的特点,易于运用与推广。 相似文献
2.
朱敬鹏 《周口师范学院学报》2005,22(2):81-83
进程并发是操作系统设计中的基础性问题,而进程的互斥则是进程并发执行的最基本需求.笔者对用于实现互斥的Dekker算法进行了详细的分析,对算法进行了升级,提出了算法中存在的若干问题,提出了问题出现的根本原因,据此提出了解决问题的具体方案,并最终给出了一个改进的实现两个进程间互斥的算法. 相似文献
3.
就刻画安全的本质而言,基于非演绎信息流安全模型较之与基于访问控制的安全模型更为确切。文章在基于迹语义对非演绎信息流安全模型进行分析的基础上,给出了基于扩展Petri网的非演绎模型的形式化描述,进一步基于Petri网的形式化描述给出非演绎模型的验证算法且开发相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。 相似文献
4.
形式化方法在程序验证、模型检测的研究有着重要作用,集成形式化方法是形式化方法发展的一个方向.BCCS模型是集成B方法和进程代数CCS构建的一个混成模型,模型中给出了一个轻量级的描述语言,但缺少语义的支持.为了保证这个描述语言的完备性和一致性,本文则在传值CCS操作语义的基础上,结合B方法对抽象数据结构的定义、系统的限制以及功能处理,给出了BCCS的操作语义,进一步刻画BCCS模型. 相似文献
5.
王亚男 《科学技术哲学研究》2020,37(2):33-38
模型化一直是社会科学重构认识论逻辑的有力途径。基于计算机模拟技术的发展,社会科学的建模路径从基于变量走向基于对象,特别是基于主体的建模。基于主体的模型一方面将社会系统整体的自下而上的突现过程展示出来,另一方面将系统要素之间交互作用受到的自上而下的整体性约束予以形式化,为动态地理解社会系统的生成和演化机制提供了新的认知模式与方法论工具,以一种复杂系统思维推动了社会科学朝着“问题导向”的趋向发展。 相似文献
6.
7.
空间方向关系形式化模型是判定空间关系的基础,为了提高模型的可靠性,提出了一种基于F直方图的空间方向关系形式化模型。首先给出了基本的F直方图算法,然后提出了基于F直方图的空间方向关系判定方法。采用人工图片作为算例进行实验的结果表明该模型是可行的。 相似文献
8.
讨论了一类基于T-S模糊模型的非线性系统,根据满意控制思想提出一种条件约束下的状态反馈控制设计方法。即在H∞控制基础上,加入圆形极点指标和状态协方差指标约束。进而研究了圆形极点约束和状态协方差约束下,系统被控输出对扰动输入的H∞抑制界优化问题,并且将H∞优化、圆形极点和状态协方差指标约束的状态反馈控制器设计归结为求一组线性矩阵不等式(LMI)的可行解问题,通过求解LMI得到满足要求的控制器参数。仿真结果表明该方法可行有效。 相似文献
9.
10.
多角度讨论了业务系统的图形用户界面开发,从开发中存在的问题出发,首先提出支持获取业务系统界面逻辑的表示模型——RU模型,通过RU模型,对界面开发的全过程进行建模;其次,基于RU模型,提出了业务系统的界面逻辑的获取方法,并且给出自动获取算法以及建模工具. 相似文献
11.
按照存在量词公式的证据是全称量词公式的反例的特性,通过考察时态逻辑算子,用模型检查的反例生成机制对测试用例生成技术进行研究．然后把模型检查的算法引入到软件测试领域,寻找验证的路径,生成测试用例,据此对系统进行测试．通过实例说明了测试用例的具体实现过程． 相似文献
12.
提出了一种基于SIFT（尺度特征变换）特征点校正几何参数的小波域盲检彩色图像水印算法。该算法利用彩色图像RGB提取特征点,估计几何参数校正几何攻击的彩色图像,从而提取受攻击的水印信息。利用Matlab6.5实验平台实现算法,实验结果表明该算法对几何攻击具有较好的透明性和鲁棒性。 相似文献
13.
针对网络控制系统中的随机延迟会恶化控制品质,甚至使系统变得不稳定这一问题,把标准预测函数控制算法推广到带随机延迟的网络控制系统中,提出了时戳预测函数控制算法.该算法通过时戳方法来估计网络在控制系统中引入的总延迟,根据系统离散的延迟状态空间模型来预测未来输出,并由预测函数控制的思想得到了适用于网络控制系统的控制规律.在基于TrueTime工具箱搭建的网络控制系统仿真平台上,对比了时戳预测函数算法和传统预测函数算法,系统响应曲线显示前者具有更好的控制品质. 相似文献
14.
1IntroductionSoftware reverse engineering is a process of analyz-ing a software system to identify its components andtheir interrelationships and create representations ofthe system in another form,or at a higher level ofabstraction[1].Xi Dian reverse engineering tool(XDRE)[2]previously developed in the author’s labcan partially recover the UML diagrams from C source codes[3].However,the fact that crosscuttingconcerns cannot be extracted by most software reverseengineeringtools is ani mp… 相似文献
15.
Traditional studies on integrated statistical process control and engineering process control (SPC-EPC) are based on linear autoregressive integrated moving average (ARIMA) time series models to describe the dynamic noise of the system.However,linear models sometimes are unable to model complex nonlinear autocorrelation.To solve this problem,this paper presents an integrated SPC-EPC method based on smooth transition autoregressive (STAR) time series model,and builds a minimum mean squared error (MMSE) controller as well as an integrated SPC-EPC control system.The performance of this method for checking the trend and sustained shift is analyzed.The simulation results indicate that this integrated SPC-EPC control method based on STAR model is effective in controlling complex nonlinear systems. 相似文献
16.
推导了基于流体流理论的网络简化模型,并基于该模型将遗传算法应用于PID控制器参数优化,定义了一个综合调节时间、上升时间、超调量、系统误差等动静态性能指标函数,在给定的参数空间进行组合优化搜索,迅速求得使性能指标优化函数极小化的一组PID控制器参数,而将PID控制器应用于网络主动队列管理系统中。仿真结果表明,在大时滞和突发业务流的冲击两种情况下,该方法设计的控制器的动静态性能优于RED、PI算法。 相似文献
17.
SU Cheng-li WANG Shu-qing 《浙江大学学报(A卷英文版)》2006,7(10):1723-1732
INTRODUCTION In recent years, research on nonlinear model predictive control has attracted significant attention because most practical processes are nonlinear. In industry process control, model predictive controllers based on linear models (LMPC) are often used to control nonlinear systems. When the operating con- ditions undergo significant changes, the performance of LMPC can deteriorate drastically. Under such conditions, predictive control based on nonlinear models (NMPC) shoul… 相似文献
18.
利用高阶模糊推理系统进行曲线拟合．首先构建高阶模糊推理系统模型,然后基于梯度下降的学习算法对高阶模糊推理系统模型的权值进行改进,最后进行曲线拟合,并与基于最小二乘的曲线拟合结果进行比较．结果表明,高阶模糊推理系统比基于最小二乘的曲线拟合具有更强的非线性处理能力,更适用于曲线拟合． 相似文献
19.
田苗苗 《廊坊师范学院学报(自然科学版)》2011,11(6)
特征识别是语义特征造型系统面临的一个难题。尤其是当遇到复杂的拓扑结构或是较多的特征数量时,如何提高特征识别的效率以及采取何种识别方法,成为该技术领域的热门课题之一。通过运用BAM神经网络检测技术,提出了一种全新的特征识别策略,有效解决了CAD／CAM系统的性能瓶颈问题。 相似文献
20.
Object-oriented model possesses inherent concurrency. Integration of concurrency and object-orientation is a promising new field. MPI is a message-passing standard and has been adopted by more and more systems. This paper proposes a novel approach to realize concurrent object-oriented programming based on Message-passing interface(MPI) in which future method communication is adopted between concurrent objects. A state behavior set is proposed to solve inheritance anomaly, and a bounded buffer is taken as an example to illustrate this proposal. The definition of ParaMPI class, which is the most important class in the concurrent class library,and implementation issues are briefly described. 相似文献