业务流程建模与测试方法研究

针对复杂业务流程设计测试效率低、自动化程度不高、测试用例正确性难以保证的问题,在研究接口自动机模型的基础上,提出了一种基于模型的业务流程测试方法。该方法首先采用扩展带约束的接口自动机对业务流程设计进行形式化描述,并给出了从业务流程设计模型到带约束的接口自动机模型的转换算法;然后基于模型完成了对业务流程设计与需求的一致性验证,将验证后的接口自动机模型作为业务流程的测试模型,通过其特有的"乐观方法"和博弈思想实现了流程间的嵌套调用组合;最后定义了业务流程的测试覆盖准则,并在满足活动约束条件组合覆盖准则的前提下,设计了相应的测试用例生成算法。实例分析表明:该方法能够简化测试过程,可用于业务流程设计的测试用例自动化生成,有效保证了测试用例的正确性,提高了测试效率。     

PPTL模型检测器实现的一个关键技术

针对命题线性时序逻辑表达能力有限的问题,设计并开发了基于SPIN(Simple Promela interpreter)验证系统的命题投影时序逻辑(PPTL)模型检测器.将协议元语言(ProMeLa)描述的系统转换为系统自动机,将PPTL公式表达的性质转换为性质自动机,通过判定系统与性质自动机的积自动机接受的语言是否为空来判断系统是否满足性质.PPTL模型检测器修改了SPIN的匹配机制,从而改进了验证算法,使得PPTL模型检测器支持有穷和无穷模型的验证.实验结果表明,该模型检测器可以减少无效验证产生的无效迹数目,有效地实现PPTL模型检测.     

采用模型检测器的软件安全模型验证方法

针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型,并使用线性时序逻辑描述安全属性,将形式化模型与安全属性共同作为模型检测器的输入,得到模型是否满足性质的验证结果,从而实现了软件安全设计与验证技术的有机结合.实验结果表明,该方法能够在软件设计初期对所涉及的安全性进行有效分析与验证.     

基于线性时序逻辑的业务流程验证

目的为了解决业务流程设计与需求的不一致性问题。方法提出了一种基于XML过程定义语言和线性时序逻辑的业务流程验证方法。结果采用Promela语言描述业务流程模型,线性时序逻辑表示抽象的业务需求,通过模型检测器Spin完成流程的验证工作。结论实现了对流程正确性的判断。     

应用UML2.0模型的测试用例生成方法

针对软件开发过程中测试自动化程度低的问题,在研究基于模型的测试用例生成技术的基础上,提出了一种基于UML2.0序列图与用例描述的测试用例生成方法.采用事件确定有限自动机来描述系统序列图,通过命题投影时序逻辑的模型检测技术,验证了自动机模型的正确性.使用自动机模型与用例描述来生成测试用例,该用例满足事件与全路径覆盖准则.通过对图书管理系统的分析表明,该方法不仅能够提高软件的测试效率,而且还确保了针对管理员的执行动作所产生的测试用例的正确性.     

温控系统的时序Petri网建模与验证

基于时序Petri网对温控系统进行建模和性质描述.利用可达图、Büchi自动机和ω-正则表达式理论三者相结合的方法分析得到温控系统时序Petri网模型变迁引发序列集合的ω-正则表达式,进一步分析证明该ω-正则表达式满足温控系统的功能性需求说明,从形式上验证了温控系统时序Petri网模型与需求说明一致.结果表明,时序Petri网可用来描述和验证具有时序关系和因果关系的并发系统模型,是一种并发系统形式化描述和分析的有效工具.     

矿井机车自主驾驶过程的建模及验证

文章首先使用自然语言描述了矿井机车自主驾驶系统的结构和控制过程;然后基于时间自动机理论对自主驾驶中涉及的机车控制器、机车运行服务器以及其他车载设备、被控对象建模,从而得到自主驾驶的时间自动机网络模型;最后应用时间自动机模型验证工具UPPAAL对自主驾驶模型进行了仿真分析和验证。验证结果表明建立的模型满足系统的功能性需求和实时性需求,证明了系统设计的正确性。     

一种航空电子系统体系结构错误行为验证方法

针对航空电子系统体系结构安全性评估过程中,组件故障影响分析,正确性难以保证的问题,提出了一种基于模型的体系结构错误行为描述和验证方法。首先,针对系统功能需求和安全性目标,建立体系结构模型;然后,采用错误模型附件描述组件的错误行为和导致的故障影响,并使用层次自动机作为中间状态,通过转换算法实现体系结构错误行为模型的形式化描述;最后,通过模型检测实现安全性需求的正确性验证。实例分析表明,该方法能够验证体系结构设计的组件错误影响和应对措施是否满足系统的安全性目标,提升安全性评估的准确性和效率。     

基于LSC模型检验的性质抽取

采用LSC(live sequence chart)描述基于场景的需求规格说明,根据设计模型必须满足需求规格说明的一致性原理,针对安全性、可达性、活性等性质,设计3种用于自动生成和抽取性质的覆盖准则,并根据准则从LSC需求规格说明中抽取与设计模型相关的性质.抽取的结果可用于自动化验证,为验证需求模型与设计模型的一致性提供保障.     

基于价格时间自动机的飞机着陆最优成本研究

针对目前航空运输系统中对飞机着陆调度成本效益研究的不足,提出采用价格时间自动机作为形式化描述方法,将飞机着陆过程建模为其相关实体的交互行为,引入时间和价格因素描述各实体的属性和行为,从而将飞机着陆形式化为时间价格的动态交互协作,并分别为相关实体和服务建模,形成彼此独立又相互协作的价格时间自动机网络,将飞机着陆调度成本表示为价格时间自动机网络上的状态转换路径。最后提出一组系统模型需要满足的性质,使用价格时间自动机模拟验证工具UPPAAL CORA仿真并验证其正确性,使用最优成本标准分支算法分析求解飞机着陆调度最优成本的可达性。     

面向结合面密封性能要求的装配连接工艺设计

为在产品设计阶段规划出满足密封性能要求的装配连接工艺,提出了一种面向结合面密封性能要求的装配连接工艺数字化设计方法.采用接触非线性有限元技术和弹性相互作用理论建立了螺栓组连接有限元模型,研究了螺栓预紧顺序、预紧力水平与结合面连接性能间的关系,构建了各螺栓预紧力大小与结合面压力间的关联模型,进而利用该关联模型,根据工况载荷下设备对密封性能的要求反求装配连接工艺.以发动机缸体缸盖装配连接为例,建立了发动机曲柄连杆机构动力学模型,分析了其工况载荷,并在缸体、缸盖和缸垫有限元模型的基础上,确定出工况载荷下发动机密封性能对结合面压力分布的要求,最后利用螺栓组连接与结合面压力间的关联模型反求出各螺栓预紧力的大小,通过与该型发动机已有装配连接工艺对比,验证了该设计方法的可行性.     

面向定制化需求的冷轧产品多目标质量控制方法

To deal with the increasing demand for low-volume customization of the mechanical properties of cold-rolled products, a two-way control method based on mechanical property prediction and process parameter optimization (PPO) has become an effective solution. Aiming at the multi-objective quality control problem of a company’s cold-rolled products, based on industrial production data, we proposed a process parameter design and optimization method that combined multi-objective quality prediction and PPO. This method used the multi-output support vector regression (MSVR) method to simultaneously predict multiple quality indices. The MSVR prediction model was used as the effect verification model of the PPO results. It performed multi-process parameter collaborative design and realized the optimization of production process parameters for customized multi-objective quality requirements. The experimental results showed that, compared with the traditional single-objective quality prediction model based on support vector regression (SVR), the multi-objective prediction model could better take into account the coupling effect between process parameters and quality index, the MSVR model prediction accuracy was higher than that of the SVR, and the optimized process parameters were more capable and reflected the influence of metallurgical mechanism on the quality index, which were more in line with actual production process requirements.     

基于DAML-S和扩展Petri网的Web业务流程建模方法

为实现Web上业务流程动态装载和调用以及跨企业业务流程的动态集成目标,提出了一种Web上的业务流程建模方法.该方法扩展了具有良好过程建模性能的Petri网,并将其与Web服务描述的本体语言DAML-S相结合.首先将Petri网扩展为业务流程建模,用DAML-S来描述流程模型,然后利用结合了DAML-S的UDDI注册中心来查找最佳服务,并在执行阶段动态调用合作伙伴提供的Web服务,从而实现了在企业间相对通用的一些业务流程的动态集成.通过一个实例对整个过程进行了验证讨论.     

Multi-objective quality control method for cold-rolled products oriented to customized requirements

To deal with the increasing demand for low-volume customization of the mechanical properties of cold-rolled products, a two-way control method based on mechanical property prediction and process parameter optimization(PPO) has become an effective solution. Aiming at the multi-objective quality control problem of a company's cold-rolled products, based on industrial production data, we proposed a process parameter design and optimization method that combined multi-objective quality prediction and PPO. This method used the multi-output support vector regression(MSVR) method to simultaneously predict multiple quality indices. The MSVR prediction model was used as the effect verification model of the PPO results. It performed multi-process parameter collaborative design and realized the optimization of production process parameters for customized multi-objective quality requirements. The experimental results showed that, compared with the traditional single-objective quality prediction model based on support vector regression(SVR), the multi-objective prediction model could better take into account the coupling effect between process parameters and quality index, the MSVR model prediction accuracy was higher than that of the SVR, and the optimized process parameters were more capable and reflected the influence of metallurgical mechanism on the quality index,which were more in line with actual production process requirements.     

支持多租约个性化业务定制的SaaS业务-租约模型

面对多租约日益增长的个性化业务需求,目前大多数业务模型存在不能够灵活、简单地满足租约的个性化定制的问题,因此,提出了基于ex-WSCL的SaaS业务-租约模型(exWSCL-SBTM)作为SaaS业务流程描述方法.利用该模型以交互及变迁组织业务流程的特点,以及将业务端与租约端相分离的方式,能够提高多租约个性化业务定制的方便性和灵活性.在此基础上,给出了个性化业务定制操作行为的定义,以及提出了基于SBTM的多租约个性化业务定制框架.     

基于体系结构的软件分析设计过程模型

引入软件体系结构技术，将软件分析设计过程细分为需求分析、体系结构设计、系统设计3个阶段，并提出了基于体系结构的软件分析设计过程(SADPBA)模型，该模型是一种采用迭代增量方法将功能设计空间映射到结构设计空间，再由结构设计空间映射到系统设计空间的过程．应用函数理论对模型进行了严格的数学定义和形式化描述，确保设计结果满足完备性、一致性和正确可追踪要求．在扩展设计空间建立了需求规范与体系结构、系统设计间的可追踪机制，并建立了基于体系结构的软件分析设计开发环境模型．与传统软件分析设计过程相比，SADPBA模型有严格的理论基础和工程原则，解决了软件系统从需求到实现的平缓过渡问题，提高了软件分析设计的质量和效率．     

面向灾害蔓延仿真的元胞自动机通用模型

为模拟灾害蔓延而建立的元胞自动机模型种类繁多,但尚无一种通用的建模方法。基于此提出了一种面向灾害蔓延仿真的元胞自动机通用模型。首先,通过解析灾害蔓延机理和理论模型,根据灾害动态发展变化过程的相似性,将灾害蔓延分解为灾害量集、时空邻域集、判定规则集、更新规则集4个部分;其次,采用元胞自动机的建模方法将4个部分重新组合,构建灾害蔓延的元胞自动机参数计算仿真模型;最后,利用所提方法改进了A.Ohgai的城市火灾蔓延模型,并进行了实例验证分析。研究结果表明：所提模型只需输入环境数据和灾害起始扰动,就能得到灾害模型中的各项动态参数,可为多种灾害蔓延仿真提供通用建模方法和实现模式。     

P2P网络中基于非确定有限自动机的XML数据流过滤

将自动机方法对XML数据的过滤延伸到P2P网络中,依据在本地XML系统YFilter中构造非确定有限自动机(NFA)的思想,采用Chord环建立起分布式的NFA对于peer节点中的XML数据的查询过滤系统,并基于递归法执行查询过滤,在不同的peer节点上得到满足查询条件的数据集合。通过实验验证了当查询的数量和网络大小发生变化时分布式NFA的方法的执行性能。结果表明:本文方法可在不同的过滤场景中处理百万数量级的XPath查询,具有良好的网络流量和过滤延迟。