MARTE顺序图到CCSL模型的转换

CCSL定义的模型可对系统的时间属性进行建模,基于Observer技术,还可对CCSL模型的正确性进行分析。但与顺序图相比,CCSL模型不利于用户理解。利用形式化方法实现了顺序图到CCSL模型的转换并证明了两者的互模拟关系。这在一定程度上扩大了MARTE在软件设计中的应用范围和效率:用顺序图对系统的动态行为进行建模,使用户和设计者对系统行为达成一致;将顺序图转换成CCSL模型进行分析,以保证模型的正确性。

采用CCSL仿真与分析反应式系统事件链模型

目前,能够对汽车电子领域中复杂嵌入式系统安全关键软件功能建模和时间分析的方法尚在研究中,而这些系统作为反应式控制系统,应该确保其具有准确的、可分析的时间行为.时钟约束规范语言CCSL是反应式系统的标准描述语言中描述时钟约束的规范语言.采用CCSL时钟模型对事件链模型中的时间约束进行分析与仿真;设计了事件链模型到时钟模型的转换规则,将事件链中的时间约束表达为时钟模型的时间约束;使用CCSL仿真工具Time Square对转换得到的时钟模型进行仿真分析,验证事件链是否满足相应的时间约束.

基于SMT的时钟约束语言CCSL的形式化分析方法与工具

时钟约束语言CCSL是一种用于描述实时嵌入式系统中事件之间约束的形式化语言,它是UML针对实时嵌入式系统建模的扩展包MARTE(modeling and analysis of real-time and embedded systems)中用于对时间建模的一个子语言.给定一组由CCSL定义的时钟约束条件,需要判断是否存在某种调度策略满足约束、是否所有满足这些约束的行为都不会导致系统死锁等分析.目前已经有一定的针对CCSL的形式化分析研究工作,如基于状态迁移系统与时间自动机的方法等.但这些方法要么只针对某种特定的分析,要么只适用于部分CCSL约束,要么分析效率较低.提出了基于SMT的统一且高效的CCSL形式化分析方法.统一性体现在其可用于有效性证明、迹分析、死锁检测、LTL模型检测等方面的验证与分析.基于该方法开发了原型工具,同时支持上述4种验证功能.工具集成了当前最高效的SMT求解器Z3和CVC4.得益于SMT求解器的高效性,实验中大部分的验证可以在短时间内完成.

组合抑制剂CCSL浮选分离PbS、ZnS与单斜Fe_(1-x)S的研究

进行了组合抑制剂CCSL分离方铅矿、闪锌矿与磁黄铁矿的浮选研究.单矿物浮选实验结果表明,浮选过程添加该组合抑制剂时,磁黄铁矿基本不浮,而方铅矿与闪锌矿的可浮性很好.方铅矿与磁黄铁矿混合矿浮选实验结果表明,添加该组合抑制剂时,方铅矿的浮选回收率可达90%以上,而磁黄铁矿基本不浮,从而很好地实现两种矿物的分离;闪锌矿与磁黄铁矿混合矿浮选实验结果表明,添加该抑制剂时也能实现两种矿物的分离,但分离效果不及方铅矿与磁黄铁矿.X射线光电子能谱、红外光谱、Zeta电位测试表明,CCSL处理后的磁黄铁矿表面的醋酸根吸附不是单纯的物理吸附.紫外吸收光谱扫描结果表明,CCSL中的醋酸根并没有阻碍磁黄铁矿表面双黄药的生成,磁黄铁矿可浮性下降仅仅是由于醋酸根对其造成的亲水性大于双黄药造成的疏水性.CCSL中的醋酸根既与磁黄铁矿中的Fe^(3+)发生亲合,又与水中的H^+形成氢键,最终增强了磁黄铁矿的亲水性;而醋酸根对方铅矿和闪锌矿基本没有影响,这是组合抑制剂CCSL能够分离方铅矿、闪锌矿与磁黄铁矿的原因.

安全关键的信息物理系统中时序行为的组合与精化

信息物理系统(cyber physical systems, CPS)通常被应用于安全关键的场景中,需要进行实时监控,并计算反馈信息,实现对外部环境的自动控制与管理.基于模型驱动的开发方法是针对实时的、异构的CPS进行开发的,而模型的可组合性是其中的核心关键点.针对时序行为的可组合问题,首先通过时序约束语言(clock constraint specification language, CCSL)建立系统的时序行为需求模型,在此基础上通过迁移系统描述CCSL的时序行为语义,并给出其组合操作方法及可组合性的形式化定义.进一步地,对时序行为进行精化操作,给出从时序行为需求模型到任务执行模型的转换方法.同时,基于L*方法对模型行为进行学习,实现组合验证以缓解状态爆炸问题,并验证精化后模型的可组合性.最后通过仿真实验及主从智能小车实例对精化与验证方法进行评估.相关数据显示,精化与组合验证方法在处理时间和内存使用上具有一定的性能优势.

光学非球面先进制造关键技术的探讨

在光学制造领域计算机控制技术的发展促进了非球面先进制造技术的不断进步。使用计算机控制光学表面成形法、计算机控制应力盘抛光技术和磁流变抛光技术可以实现高精度的非球面加工,其关键在于计算机数字控制技术的综合运用。提出了光学非球面的固着磨料研磨加工。

MARTE顺序图到TTS4SD的转换

MARTE对UML的顺序图进行了扩充,使其适用于实时系统的建模阶段,但它不能直接用于正确性验证阶段。对象管理组织提出用模型转换的方法将依照MARTE构造的顺序图(记为A)转换成具有完备的验证方法和工具的形式化模型(记为B)。用B表示A的语义可以保证B能够完整且准确地模拟A的行为。提出了形式化模型——TTS4SD,用来描述MARTE顺序图的形式语义,并在此基础上展开了验证。首先给出顺序图的形式定义,把时间变迁系统(TTS)扩充成TTS4SD;然后用TTS4SD描述顺序图的形式语义,并给出从顺序图到TTS4SD的转换算法;最后对TTS4SD展开分析。通过一个实例说明了从顺序图到TTS4SD的转化过程以及基于TTS4SD的验证方法。

一种实时系统时间约束验证方法研究

目前,能够对汽车电子领域中复杂嵌入式系统安全关键软件功能模和时间约束分析的方法尚在研究中,而这些系统作为实时控制系统,应该确保其具有准确的、可分析的时间行为。时钟约束规范语言CCSL是实时系统的标准描述语言中描述时钟约束的规范语言。采用CCSL规范表达式描述实时系统时间约束;设计了CCSL基本元素到时间自动机基本元素的转换规则;使用时间自用机验证工具UPPAAL对转换得到的自动机模型进行验证分析,验证实时系统是否满足相应的时间约束。

β-FeSi_2/Si薄膜位向关系的计算

利用从固态相变产生的沉淀相惯习面总结出的Δg平行法则 ,计算了 β FeSi2 半导体薄膜和Si基体之间可能的择优取向关系。根据界面匹配和结构的分析 ,建议最优衬底基面的晶体学位向。预测的界面是一个无理面 ,含有原子尺度台阶 ,晶格间具有良好匹配关系。以该界面位向作为Si衬底的基面有可能导致高质量金属硅化物 β FeSi2