用CA方法模拟过冷熔体中自由树枝晶的生长

基于溶质扩散和界面能的作用，建立了过冷熔体中自由树枝晶的生长模型，考虑了成分过冷、曲率过冷和界面能各向异性，用胞元自动机（CA）方法模拟了枝晶生长、界面扰动以及分枝的竞争演化，对枝晶尖端生长速度和过冷度的关系进行了模拟计算，并与L-G-K理论模型进行了定量的比较。     

用宏微观耦合模型模拟铝合金凝固过程

用一种宏微观耦合模型对Al-2．5Si在金属型中的凝固情况进行了模拟。该模型结合改进的元胞自动机模型与有限差分法，考虑了温度场、浓度场和微观生长过程。该改进的元胞自动机模型与经典元胞自动机相比较，不仅考虑了温度场扩散，而且考虑了溶质在液相中的扩散、界面曲率和溶质富集对枝晶尖端过冷度的影响。在宏微观耦合模型中采用大小两套网格分别进行宏观温度场和微观组织演变的计算。在3种不同的浇注温度下得到了3种典型的柱状晶向等轴晶转变的图形。考虑边界条件后的模拟结果发现等轴晶的形核情况与理论分析有所差别。     

基于接口精化的广义无干扰性研究

在复杂构件化软件的设计和实现过程中,由于安全属性的可组合性难以实现,使得系统整体的安全需求难以得到有效保证,因而安全属性的规约和验证问题是构件化软件开发过程中关注的关键问题。针对当前构件化软件设计过程中,信息流安全属性仅局限于二元安全级格模型的问题,在现有安全接口结构基础上提出广义安全接口结构,在广义安全接口结构上定义精化关系,并利用这一精化关系定义了能够支持任意有限格模型的基于安全多执行的无干扰属性,首次将安全多执行的思想应用于构件化系统的信息流安全属性验证。使用 Coq 定理证明工具实现了接口自动机程序库以及对精化关系的判定过程,并用实例验证说明了无干扰属性定义的特点及判定方法的有效性。     

基于场景的车载设备测试用例自动生成方法研究

列控车载子系统是确保列车的安全运行的关键设备,对车载子系统进行测试是保证功能实现与系统规范一致性的重要手段。针对传统手工测试用例生成的效率低、耗时长、工作量繁杂、可重用性低等缺陷,提出一种基于场景的车载系统测试用例自动生成方法,依据CTCS-3级列控系统技术规范构造车载子系统场景树模型,由实时系统测试用例自动生成工具Co Ver对列车运行模式转换自动机网模型生成基于场景的测试用例,并由运行模式最小重复度选择算法生成全模式覆盖的测试序列。结论证明,基于场景自动生成的测试用例能够覆盖全部车载模式,并提高了模式转换测试序列生成效率。     

维吾尔语数词类命名实体的识别与翻译

针对维吾尔语数词类命名实体(时间、日期、货币、百分比)在维汉机器翻译中翻译不准确的问题,分析其构成规律及边界信息,设计基于维汉平行语料的维吾尔语数词类命名实体的识别与翻译系统。通过有限自动机结合触发词识别并翻译维语基本数词,从平行语料中自动抽取出翻译模板,匹配模板并实现翻译。实验表明,维吾尔语数词类命名实体的识别F值达到了91%,有效提高了维汉机器翻译的质量。     

基于GPU的元胞自动机熔岩流动模拟

为解决基于元胞自动机进行熔岩流动模拟的计算效率问题,提出一种应用在元胞自动机上的GPU并行计算方法。将元胞自动机中每一个方形网格映射到GPU的一个逻辑计算单元上,通过并行计算,提高模拟的效率,解决传统串行计算方法的不足,使模拟达到实时性。模拟结果表明,在元胞自动机的物理模型理论基础上,用GPU并行计算进行加速,在模拟效果和时间效率上均取得了良好的效果。     

非确定型离散事件系统双模拟控制的实现

近年来,双模拟等价关系与离散事件系统监控理论相结合的研究引起了国内外许多学者的广泛关注.本文针对作者在前期工作中提出的非确定型离散事件系统的双模拟控制机制,进一步探讨其实现问题.利用投影映射对系统规范说明语言进行等价类划分,构造了一棵计算树,得到了一个判断规范说明是否具有基于模拟关系可观性的多项式算法,证明了双模拟控制机制是多项式时间算法可实现的.同时,通过对控制器配备具有存储和判断功能的模拟关系识别器,阐述了这种双模拟控制机制是物理可实现的.     

多处理器实时系统可调度性分析的UPPAAL模型

随着多处理器实时系统在安全性攸关系统中的广泛应用,保证这类系统的正确性成为一项重要的工作.可调度性是实时系统正确性的一项关键性质.它表示系统必须满足的一些时间要求.传统的可调度性分析方法结论保守或者不完备,为了避免这些方法的缺陷,提出使用模型检测的方法来实现可调度性分析.提出了一个用于多处理器实时系统可调度性分析的模板,将与系统可调度性相关的部分包括实时任务、运行平台和调度管理模块都用时间自动机建模,并使用UPPAAL验证可调度的性质是否总被满足.符号化模型检测方法被用于推断可调度性,但是由于秒表触发的近似机制,符号化模型检测方法不能用于证明系统不可调度.作为补充,统计模型检测方法被用于估算系统不可调度的概率,并在系统不可调度时生成反例.此外,在系统可调度时,通过统计模型检测方法获取一些性能相关的信息.     

基于形式化方法的航空电子系统检测

随着航空型号的快速发展,航空电子系统的数字化程度越来越高,软件在其中所占的比例越来越大.对航空电子系统中的软件进行测试和检测是保证航空电子系统质量及可信运行的基础.通过分析航空电子系统软件体系结构,对航空电子系统进行形式化建模,并在此基础上,提出了一种形式化的系统级综合检测方法,从静态和动态两个方面对航空电子系统进行检测,最后通过设计并实现一个综合检测系统来验证该方法的有效性.     

基于场景的联锁软件形式化模型生成方法

为保证列车运行安全和旅客生命财产安全,对车站联锁控制系统进行有效的分析、验证和测试是必不可少的,而形式化模型是联锁系统分析、验证和测试的基础.以计算机联锁软件的UML半形式化模型为基础,以事件确定有限自动机模型作为描述系统的形式化模型,研究UML2.0顺序图转换为事件确定有限自动机模型的方法.首先选取一组与交互行为相关的全局变量作为状态向量来分析和消解顺序图各个场景的消息以及不同场景间的同一消息的前后置状态向量值是否存在矛盾,从而得到一致性的需求场景;然后提取各对象的事件序列生成对应的事件确定有限自动机;最后通过组合系统中对象的自动机模型得到系统的事件确定有限自动机模型.该方法改善了安全苛求软件的设计与开发,为软件质量评估提供了技术支撑.