连续流动体系仿真程序的形式化确定

以一个基本的连续流动体系对象，讨论了传统的仿真建模过程在程序模型选择方面存在的不足，并以程序正确性断言理论方法处理了该体系的程序模型选择问题，导出了必要的程序前置断言，不变式和循环界函数，从而给出了一个具体的规范描述和一个正确的程序实现。     

基于演算的工作流建模方法研究

工作流模型缺乏一种支持过程定义以及过程分析的形式化数学模型,而π演算是一种移动进程代数运算,可用于对并发和动态变化的系统进行建模.首先提出了基于兀演算的工作流建模方法,然后经过对多种建模工具的比较和分析后,利用π演算对业务流程结构进行了形式化定义,详细地阐述了各种活动和依赖关系在π演算中的表示.该方法是完全形式化的方法,具有较强的语义表达能力,便于工作流的执行、推理和仿真等.     

基于程序蓝图的软件再工程模型化研究

针对传统再工程为遗留系统建模过程中,所采用模型表现出的片面性及模型之间的不一致性,提出了一种基于过程蓝图和类图的再工程高层抽象模型——程序蓝图。利用模型驱动的方法,给出了程序蓝图模型的形式化定义,提出了一种基于程序蓝图模型的再工程过程架构,详细规划了该过程中的活动、任务、制品以及工作流。应用实践初步表明,该模型能有效全面表现系统特征,保持了再工程过程中模型变换的一致性。     

基于形式化方法的集成电路设计简化技术研究

通过形式化方法建模,对集成电路设计过程中的模型简化技术进行了研究．对互模拟、模拟偏序概念提出判定算法,利用交互式马尔科夫链模型的事件结构构造及功能模块细化方法、软件工程方法,得到模型验证程序,该程序能够对集成电路系统设计过程中的模型进行简化,实践证明具有良好的应用价值．     

业务过程建模及其形式化验证

针对业务过程建模复杂、模型一致性难以保证的问题,提出一种求精式业务过程建模及其形式化验证方法.结合语义本体技术、基于统一建模语言(UML)的扩展机制,实现对业务过程中的不同关注点进行多视角地可视化建模.业务过程建模是一个“整体抽象过程→声明式过程→命令式过程”多阶段的求精过程.引入环境本体的概念,以软件交互对环境状态的影响来描述软件行为和能力,并在此基础上给出了模型相关定义及其形式化语义.结合一个简化的产品交易系统实例详细论述如何采用声明式形式化语言Alloy进行业务过程模型定义和模型求精的形式化验证.实例表明,采用分阶段求精式业务过程建模方法,并围绕模型语义通过Alloy语言进行形式化验证,可以有效地提升建模过程的灵活性和保证模型规范的一致性.     

层次建模的小组软件过程仿真

提出针对TSP的多层次软件过程仿真模型,该模型结合了离散和连续建模思想,给出了形式化描述,用验证实例来说明模型的执行过程及结果.此模型能够从不同角度模拟TSP,并能对软件开发过程进行监督和预测,有效提高软件过程质量.     

基于Petri网的项目管理模型研究

项目管理是一类典型的离散并发不确定系统,经典Petri网及其扩展可以很好的对项目工序逻辑关系、时间约束、资源约束、项目执行过程监控等进行可视化建模的同时,提供形式化理论支撑.在综合研究现有Petri网项目管理模型基础上,提出了基于着色时间约束Petri网的项目动态管理模型,并对该模型的变迁激发规则、状态空间、可达性及可调度性进行分析.该模型能够对项目管理中时间约束及资源约束进行建模,为项目动态管理提供可视化、形式化建模工具.     

基于ABAQUS的月壤有限元建模及仿真分析

在月球探测设备设计初期阶段,建立较为精确的月壤有限元模型,对于仿真和分析探测工具与月壤的相互作用情况至关重要.阐述了用ABAQUS软件建立月壤有限元模型的优越性,介绍了建模方法,包括本构模型的选择、月壤参数的确定,以及具体的建模步骤,并通过算例证明了该模型的有效性.该模型亦可转化为动力学模型,与ADAMS进行联合仿真分析.     

一种基于角色的MDA模型转换方法

模型转换是MDA（Model Driven Architecture）中的关键技术，正成为一个新的研究热点．提出一种基于角色的模型转换方法，通过角色的分配和组合，灵活、自然地实现模型的转换．给出了其转换规则及形式化描述方法，介绍了该方法在Web应用程序建模中的应用．使用这些转换规则及形式化描述方法可以清晰地描述角色问的约束关系，有助于设计者实现角色的分配及组合．该方法特别适用于基于模式的软件开发．     

自适应阈值估计的MS模型仿真建模

提出了一种改进的模拟电路多信号模型(MS模型)的仿真建模方法。采用Monte-Carlo方法实现电路的仿真,以获取电路特征的统计数据,利用经验公式法确定Monte-Carlo仿真的分析次数,可以减少仿真时间开销;同时,根据统计数据检验该特征的统计分布情况,再以此为依据采用自适应方法确定该特征的阈值估计区间,从而提高模型精度。最后进行了实例分析,验证了该建模方法的有效性;并从仿真时间与建模精度两个方面进行了性能比对,说明其具有的优势。     

基于抽象解释的数据迷惑正确性分析

数据迷惑是代码迷惑中重要的一类迷惑变换,在软件保护领域中应用广泛,常被用于防止攻击者对程序进行数据流分析、程序切片等逆向工程攻击。从语义的角度,给出了一种基于抽象解释的数据迷惑正确性的分析方法。首先使用抽象解释理论,从程序语义的角度,对数据迷惑进行形式化描述,用一种语义变换形式化地描述数据迷惑。然后在形式化描述的基础上,由语义变换和语法变换之间的关系,构造得到数据迷惑算法。最后在基于抽象解释的数据迷惑的形式化描述的基础上,对数据迷惑变换的正确性进行分析和讨论。     

SOC的形式化验证方法

针对SOC验证的需要,研究了形式化验证方法,重点分析了二元决策图(BDD)的等效性检查技术,设计了FSM等效性检查的程序,以及算法级描述控制流程到BDD转换方法;研究了利用计算树逻辑进行的模型检查技术,给出了CTL模型检查的处理流程;提出了形式化仿真的模型以及测试向量生成算法.     

六杆式干草压捆机的参数优化及仿真

建立了六杆式压捆机的运动学和动力学模型,用序列求解法对其进行了求解,并验证了建立的模型和求解方法的正确性。基于遗传算法运用Matlab编制了六杆式压捆机压缩机构的优化程序,对各杆件长度进行了优化,获得了最优参数。在相同工况下,把曲柄滑块式和六杆式压捆机在Adams环境中的运动学和动力学仿真结果进行了对比,验证了同样工况下六杆式压捆机具有省力的特点。     

VV＆A and confidence assessment of a complex giant system simulation model

Modernsocietyisinundatedwithinformation ,networksandsystems .Manycomplexsystemshaveappearedinvariousfieldssuchasengineeringtechnolo gy ,socialeconomyandecologicalenvironment ,etc .,(asshowninFig .1 ) [1 ] .Fig .1　Complexgiantsystem　　Howdowemanagesuchacomplexsystem ?Howdoweanalyze ,predict,programanddesignthecom plexityofsuchasystemsoastoimprovethesystemoperationstateandefficiency ?Peoplearefacingthesemajorproblems .　　Asacomplexsystemmayconcernfieldsincludingengineeringtechnology ,social…     

Verilog程序的命题投影时序逻辑符号模型检测

为了保证以Verilog硬件描述语言设计的片上系统的正确性,提出了Verilog程序的符号模型检测方法．依据形式化操作语义将Verilog程序建模为有限状态机,将设计规范用命题投影时序逻辑公式描述,并采用命题投影时序逻辑符号模型检测工具对程序进行验证,从而证明片上系统满足设计规范．以Verilog程序描述的四位同步二进制计数系统的验证实例表明,Verilog程序的命题投影时序逻辑符号模型检测方法是可行的．     

实时嵌入式系统并发程序检测方法研究

近年来随着实时嵌入式系统自动化程度的不断提升,其设计复杂度不断加大,在设计中大量的使用了并发程序设计方法。但目前在基于实时嵌入式系统应用程序开发以及测试的过程中,由于中断和线程的相互交叠,始终缺乏有效的针对实时嵌入式系统的并发程序测试方法。本文设计了面向实时嵌入式系统并发程序动态测试的算法,提出以标记迁移系统作为并发程序的系统模型,对常见的并发错误给出了形式化定义,使用偏序化简算法缩减程序的状态空间,实现了对多线程、多重中断的并发程序错误检测。     

多体系统分析软件的开发与应用

多体系统动力学作为研究机构动态特性的应用基础学科 ,最终目的是编制通用仿真软件为工程技术领域提供强有力的计算机辅助分析工具 .介绍了凯恩 -休斯顿方法的优点 ,基于该方法建立起多体系统动力学模型 ,根据软件工程和面向对象编程技术的要求开发出具有友好的用户界面、集成度高、能够对任意拓扑结构的多体系统的运动学和动力学进行正、逆问题分析的多体系统分析软件MBSA(Multi BodySystemAnalysis) .介绍了软件的模块组成 ,详细叙述了核心运算模块的流程 ,算例分析验证了该软件的正确性和可靠性     

多径中继传输系统网络仿真设计与实现

基于应用层中继的多径传输系统(MPTS-AR)是一种基于应用层中继的多径传输系统,通过基于用户数据报协议的中继服务器构建端到端的多径传输条件,并可支持多种业务实现多径传输. 提出基于OMNeT++平台上的INET Framework实现MPTS-AR网络仿真的方法,包括用户代理、中继服务器和中继控制器等网络逻辑实体的二次开发方法、相关网络链路和网络拓扑的构建方法、消息定义与处理方法等;讨论了应用程序接口兼容和多业务支撑等重难点技术. 最后,通过H.264业务传输实例验证了所设计MPTS-AR网络仿真的正确性和有效性.     

系统级描述语言SystemC到时间Petri网的转换技术

SystemC作为一种系统级描述语言能够同时描述硬件和软件,但缺乏形式化分析的手段.针对其存在的问题,提出引入Petri网的设想,通过分析了SystemC程序本身的结构特点,指出其主要由顺序、分支、循环以及并发等结构组成,并分别给出与Petri网的对应关系.同时提出了由SystemC程序到时间Petri网的转换方法.使用Petri网的工具对并发程序进行分析,将SystemC程序转换成时间Petri网,为基于SystemC的系统设计提供形式化的分析方法.并应用Petri网的可达图检测出原SystemC程序中的死锁,该转换方法的有效性达到了引入形式化方法的目的.     

核电站反应堆冷却剂平均温度内模控制系统仿真

采用系统开环脉冲响应序列,创造了一种非参数建模方法,解决了复杂非线性系统的建模难题,并应用内模控制原理创造了一种反应冷却剂平均温度恒定控制的非参数模型。该模型设计简单、跟踪调节性能好、鲁棒性强、能消除不可测干扰。仿真实验证明了本设计方法的正确性和有效性,实现了系统的高精度控制。