混成系统形式化验证

混成系统是实时嵌入式系统的一种重要子类,其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况,因此行为复杂,难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域,因此,如何对相关系统进行有效的分析与理解,从而保障系统安全运营,是一项具有重要意义的工作.常规的系统安全性分析手段,如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为,无法穷尽地检测复杂混成系统在所有可能输入下的行为,因此并不足以保证系统的安全性.区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此,其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上,针对现阶段实时嵌入式系统复杂化、网络化的特性,对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.     

带数据约束实时系统的模型检测

带数据约束的实时系统是指一种既带有时间约束又带有数据变量约束的计算系统。目前将离散数据约束和连续时间约束统一在一个模型中的规范及验证研究较少。文中提出了一种既带有连续数据约束又带有离散数据约束的规范——基于连续时间的ZIA规范,并给出它的时序逻辑。MARTE是UML在嵌入式实时系统领域的建模规范,在工业界的应用非常广泛,但是目前对其模型检测的研究较少。在MARTE的基础上扩展Z,提出了Z-MARTE,并将Z-MARTE转换为基于连续时间的ZIA模型,在实现对连续时间ZIA模型检测的同时,也实现了对Z-MARTE的模型检测。最后通过一个实例进行验证,说明此方法可行有效。     

基于XYZ/E的混成系统

混成系统是由计算机和物理设备组成的嵌入式实时计算系统.它允许在交互式实时系统中引入连续变化的单元.XYZ/E 是基于Manna-Pnueli的线性时序逻辑的程序设计语言.它将程序的动态语义与静态语义统一在同一框架中,支持从抽象的程序规范到可执行代码的逐步求精的全过程.该文使用XYZ/E语言描述和验证混成系统.首先介绍了计算模型,然后介绍了XYZ语言对混成系统的形式化描述,最后介绍了混成系统的验证.与同类工作相比,XYZ/E支持状态转换,从而可以方便地描述复杂的控制算法.     

基于MDA的MARTE模型形式化方法

针对嵌入式系统对可靠性和可预测性的要求,提出基于MDA对嵌入式系统的建模语言MARTE进行形式化描述的方法。建立Object-Z的元模型,定义了MARTE元模型与Object-Z元模型之间的模型转换关系,给出了MARTE模型到Object-Z模型的语义映射和语法转换的具体过程。该方法支持将MARTE模型形式化转换为Object-Z模型,有利于软件开发早期的检验和验证。     

多机器人路径规划的安全性验证

近些年来,伴随着人工智能领域的浪潮,机器人越来越多的出现在我们的日常生活中,例如足球机器人、无人机、无人车等.如何保证这些自治机器人尤其是多个机器人在移动过程中的安全成了人们一直很关心的问题.混成通信顺序进程（Hybrid Communicating Sequential Process,HCSP）是一个针对混成系统的形式化建模语言,在通信顺序进程（Communicating Sequential Process,CSP）的基础上引入了微分方程以描述混成系统中的连续行为和控制逻辑,可以方便高效地对大型控制系统尤其是在有通信事件发生时的情形进行形式化建模.本文就是用HCSP建模多机器人的路径控制算法,并用定理证明工具HProver进行形式化验证.结果证明了在满足一定初始条件下,机器人团队在整个运行途中不会发生碰撞.     

混成系统研究综述

混成系统是一类既包含连续动态行为又包含离散动态行为的系统,这类系统在实际应用中显得越来越重要,对这类系统需要探索新的模型和研究方法。从建模、分析与验证三个方面综述了混成系统的研究现状和需要进一步研究的课题。     

基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究

能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合MARTE语义信息的扩展Sys ML活动图模型,用于描述安全关键应用中的嵌入式系统动态行为的设计,并对此扩展模型展开基于模型转换的系统设计安全性特征的形式化分析与验证方法的研究;包括:构建了Sys ML活动图与MARTE中非功能性质建模语义相结合的元模型,以及验证工具UPPAAL的时间自动机元模型,并且给出了二者之间的语义映射规则;建立了从时间自动机模型描述到UPPAAL工具输入格式之间的语法转换方法;设计了一个基于AMMA平台的面向扩展Sys ML活动图的模型转换与验证框架;最后,给出了一个高铁控制系统设计模型的安全性验证的实例分析.     

MARTE顺序图到TTS4SD的转换

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

穿刺机器人运动安全性的形式化分析与建模

混成系统是实时嵌入式系统的重要子类,其行为中存在连续变化和离散跳转混杂的情况,使得混成系统行为复杂,安全性难以掌握。近年来,混成系统在医疗环境中得到越来越广泛的应用。其中,医疗机器人的穿刺运动控制系统呈现高度复杂的混成性,如果机器人在穿刺过程中失控将导致不可挽回的严重后果。因此穿刺机器人运动行为的安全性设计成为了亟需解决的问题。首先根据穿刺机器人的运动学设计,将机器人的复杂运动分解。然后基于微分动态逻辑理论从混成系统的角度出发对穿刺机器人的运动控制系统进行了形式化建模与分析,并使用证明工具KeYmaera归纳出微分不变式,获得了控制模型的参数约束。最后提出了针对机器人运动到某一靶目标区域这类运动学问题的一般性验证模型。     

爬行机器人的分层可控混成Petri网建模研究

飞机表面爬行机器人是一个复杂的离散事件和连续动态事件相结合的混成运动系统,为描述系统的静态特性和动态行为,提出一种分层可控混成Petri网模型.依据爬行运动机构定义了Petri网模型组成元素,建立了爬行机器人单轴和双轴分层可控混成Petri网,该模型可接收上层运动轨迹指令并输出爬行动作序列.实验表明,基于该模型实施的飞...     

基于改进高斯混合模型的运动目标检测方法

基于高斯混合模型,提出了一种自适应的运动目标检测算法。首先,根据各像素点的像素值的集中程度,自适应地选择高斯分布的个数对背景模型进行学习与更新,再通过背景差分获取差分图像;其次,在对图像二值化的过程中,提出了一种改进的自动调整阈值的方法,用以对差分图像的像素进行分类后分别进行阈值化分割,这样就能得到前景目标;接着采用形态学重构的方法对阴影进行有效消除,从而使前景目标分割的效果得到有效的提高。实验证明,该方法具有较好的鲁棒性和检测效果,同时也具有较好的自适应性,特别是在检测目标本身灰度变化比较大等特殊情况下,更能体现出本算法的优越性。     

A framework for hybrid model predictive control in mineral processing

Model Predictive Control (MPC) is an advanced technique for process control that has seen a significant and widespread increase in its use in the process industry since its introduction. In mineral processing, in particular, several applications of conventional MPC can be found for the individual processes of crushing, grinding, flotation, thickening, agglomeration, and smelting with varying degrees of success depending on the variables involved and the control objectives. Given the complexity of the processes normally found in mineral processing, there is also great interest in the design and development of advanced control techniques which aim to deal with situations that conventional controllers are unable to do. In this aspect, Hybrid MPC enables the representation of systems, incorporating logical variables, rules, and continuous dynamics. This paper firstly presents a framework for modeling and representation of hybrid systems, and the design and development of hybrid predictive controllers. Additionally, two application examples in mineral processing are presented. Results through simulation show that the control schemes developed under this framework exhibit a better performance when compared with conventional expert or MPC controllers, while providing a highly systematized methodology for the analysis, design, and development of hybrid MPC controllers.     

车辆正碰安全性的混合可靠度分析

研究汽车结构可靠性能优化问题,由于设计中原材料加工、装配等众多不确定因素,整车的舒适度及承受碰撞能力不符合可靠性标准的要求等,导致汽车的实际状况存在抗击模型不确定性,使结构可靠性准确计算变得较为困难。根据概率与非概率混合可靠度模型及其求解技术,结合有限元软件分析以及代理模型技术构造响应面,进行轿车正碰可靠性计算,通过计算获得可靠性指标区间。实际算例表明算法具有较高的计算效率及精度,对实际设计工作有一定参考价值。     

A hybrid fuzzy model for selecting and evaluating the e-book business model: A case study on Taiwan e-book firms

This study evaluates an appropriate business model for e-book firms in Taiwan. We apply expert questionnaires to calculate the weights, which contain five criteria, namely, business strategy (BS), finance characteristics (FC), market characteristics (MC), quality measurements of product and service (QS) and implementation (IM) (BCCSM) for the capability of developing the firms’ business. Then, a fuzzy analytic hierarchy process (FAHP) is adopted to explore the weights of indices, and the VlseKriterijumska Optimizacija I Kompromisno Resenje (VIKOR), grey relation analysis (GRA), and the technique for order preference by similarity to ideal solution (TOPSIS) are utilized to rank the three alternatives. The results show that a single brand is the best e-book firms’ business strategy that is simultaneously integrated by content, platforms, and devices, while the top two weights of the evaluation criteria are the business strategy and market characteristics to enable firms to develop an appropriate e-book business model.     

基于混合粒子群优化SVM算法的红斑鳞状皮肤病诊断

红斑鳞状皮肤病的诊断是皮肤病科的一个难题,针对这一问题,提出一种基于混合粒子群的支持向量机(SVM)模型HAPSO-SVM来提高红斑鳞状皮肤病的诊断精度。模型考虑了特征选择机制和参数优化两者对SVM模型起着同等重要的作用,使用自适应的混合粒子群算法(HAPSO)同步实现特征选择机制和SVM的参数寻优,同时设计的线性加权多目标函数综合考虑了分类准确率和支持向量个数,从而提高了算法的准确率和效率。结果表明,提出的模型不仅获得了较少的支持向量个数,找出了红斑鳞状皮肤病紧密相关的特征,并且得到了很高的分类准确率,是一种有效的红斑鳞状皮肤病诊断模型。     

混合系统建模理论与混合系统模型

在现代工程仿真中,大部分仿真对象表现出同时具有连续和离散对象的特征,利用现有的离散或者连续建模理论不能全面的反应出对象特性,需要对混合系统的建模进行相应的理论研究.从系统理论出发,围绕着系统的连续属性和离散属性,以及他们对系统信息的响应,还有他们之间的相互作用为中心,建立混合系统模型的形式化表达和系统理论基础,并在此基础上建立了混合系统模型.以此模型为基础,在实践中为某大型仿真项目中的工程对象建立了混合模型,在仿真中得到有效的应用.     

网络混合仿真及其在NS-2下的实现

将流仿真与数据包仿真结合的混合仿真可以同时利用两种仿真技术的优势。该文在Vishal Misra的流模型的基础上提出了混合仿真模型的实现框架。在仿真模型基础上,基于数据包仿真工具NS-2实现了混合仿真。在混合模型仿真实现中,对需要包级网络性能参数的子网采用包仿真技术,其余部分采用流仿真,在得到具体包级信息的同时,大大改善了仿真效率。混合模型实现的关键在于解决包仿真和流仿真间的接口问题,文中给出了解决接口问题的具体方法。该文设计了一组试验对该混合模型进行验证,仿真结果表明模型既可以准确捕获TCP流的动态特性,又可以提高整个网络的仿真效率。     

基于区域混合活动轮廓模型的医学图像分割

针对变分水平集算法在图像分割过程中计算量较大且收敛速度慢的现象, 在一些基于区域的活动轮廓模型基础上提出了一种新的基于区域混合模型的非凸正则化活动轮廓模型。该模型构造了一个新的能量泛函,该能量泛函结合了考虑图像局部聚类性质的LBF模型和测地线模型,增加了非凸正则化项,加快了轮廓曲线的收敛速度,可以很好地保持区域形状并能防止边缘过平滑,然后通过经典有限差分法求得能量泛函的极小值。最后,在合成图像和医学图像上做了仿真实验,结果表明,该算法具有较快的收敛速度 和很好的鲁棒性,分割结果也较准确。     

Hybrid cutting simulation via discrete vector model

Geometric cutting simulation and verification play an important role in detecting NC machining errors in mold and die manufacturing, thereby reducing the correcting time and cost on the shop floor. According to workpiece model, current researches may be categorized into view-based, solid-based, and discrete vector-based methods. Each methodology has its own strengths and weaknesses in terms of computing speed, representation accuracy, and its ability to perform numerical inspection. This paper proposes a cutting simulation methodology via a hybrid workpiece model which consists of the general discrete vector model and its simplified model. Workpiece modeling scheme, cutting simulation via tool swept surface modeling and vector intersection, and some case studies of mold and die machining are presented in this paper.