UML时间顺序图的自动验证技术

UML顺序图反映对象之间的消息交互顺序,在系统建模中应用十分广泛.对顺序图进行时间扩展得到UML时间顺序图,使其具备对实时系统建模的能力.在此基础上研究了UML建模工具和模型验证工具UPPAAL的接口信息,将UML时间顺序图模型转化为时间自动机模型,并对该系统模型进行形式化验证.设计和实现了基于XML的UML时间顺序图自动验证工具.     

可信分布式实时系统的面向方面的形式化方法

形式化方法具有精确数学含义的科学研究和验证方法,是建立在数学基础上的,可信分布式实时系统开发过程中的时间分析是非常复杂的,涉及到不同的方面,需要考虑很多东西,不同的可信分布式实时系统具有不同的时间性需求,不能用一种开发方法进行分析、设计和实现,由于形式化方法具有严谨、可数学分析、证明、完整性、一敌性、无二义性和精确性等特性,可以根据系统开发的不同方面采用不同的形式化语言进行分析、设计和实现,然后再把这些方面编织应用到系统中去,来完成它在系统中特定的作用,因此形式化方法已经成为人们深入研究的一个领域。     

信任协商策略的Petri网建模分析方法

对Peer-to-Peer网络环境下信任协商和信任协商策略进行了定义和形式化描述,提出了一种基于Petri网模型的信任协商策略建模分析方法,将资源、证书和资源访问策略映射为Petri网网元进行建模,通过可达分析寻找最优资源解锁序列.和其他信任协商策略建模方法相比,该方法具有较好的性能.     

基于时序逻辑的工作流建模与分析方法

提出了一种基于活动时序逻辑(TLA)的工作流建模与模型分析的形式化方法.该方法将模型及模型的性质都表示为一个TLA公式,对工作流模型性质的分析可以等价为对TLA中两个公式之间是否存在蕴涵关系的检验,从而建立了一个工作流模型各层次分析统一框架.一个工作流建模和分析的实例验证了所提出方法的有效性,该方法在建模、模型分析以及指导模型设计等方面都有较好的应用前景.     

面向服务的虚拟企业模型及其一致性检查机制

针对面向服务的虚拟企业业务运作对企业建模的需求,提出了面向服务的虚拟企业模型(SOVEM),并研究了其一致性检查机制.在分析面向服务的虚拟企业业务模式及其特点的基础上,提出了SOVEM的概念模型和形式化定义,讨论了其建模过程和成员企业模型映射方法,继而讨论了模型的一致性检查机制,定义了一致性约束并给出了模型验证算法,以...     

面向对象的流程供应链结构描述方法研究

针对流程供应链结构描述问题,首先对供应链构成体进行分解,用链节、子链、过程、子过程等作为供应链的基本构成体．为供应链建模提供了一种描述型语言;然后对供应链工作流进行形式化定义,用工作流图、前趋链节、前趋链集等的概念和定义为下一步的流程供应链建模及分析提供了概念自包的方法。最后结合上述方法以煤炭流程供应链中物流为对象,进行了工作流建模并运用定义的方法分析了需求信息对供应链运营的拉动过程,为流程供应链的描述及分析提供了一种形式化的工具。     

面向企业能效评估的能源消耗过程建模方法研究

针对企业能效评估对能源消耗系统模型的需求,在分析企业能耗过程的组成因素及其相互作用关系的基础上,提出了一种将企业的生产过程、物料移动、资源配置、余能回收利用等数字化的,基于模糊高级Petri网的企业能源消耗过程建模方法,并详细地给出了模型的形式化定义、运行规则以及建模原则.实例分析表明,该方法独立于特定的能源类型和用能设备,实现了能耗过程结构和动态行为方面信息的全面描述,是企业能源消耗过程分析与优化的基础.     

基于多设计Agent的结构设计多方案协同选择

基于Ａgent的建模方法,以及美国运筹学家Ｓaaty的层次分析法,提出了结构设计多方案的多设计专家协同选择的形式化方法,并确定了相应的数学求解模型和算法。     

基于SysML模型的需求建模及测试方法

为了将模型驱动测试有效应用于嵌入式系统测试中,本文说明了需求建模方法以及用例生成方法,以及SysML建模语言中状态机图的抽象语法、图元符号和形式化语义,针对性能测试要求,总结了关于状态机模型的性能测试建模方法,并通过实例构建状态机图描述性能需求,建立测试场景分析方法,有效覆盖系统的性能测试类型.经验证,采用基于模型驱动的测试方法能够建立明确系统执行逻辑,构建测试最长路径等场景,保证测试的充分性和覆盖性,提升测试效率和自动化程度.     

新临钢炼钢厂计算机实时局域网络

文章重点论述了局域网在炼钢工业实时系统中的应用,从网络系统的设计、异种网的互联、实时系统的开发和未来的发展设想等方面进行了阐述。     

Repair-control of enterprise systems using RFID sensory data

This paper presents an architecture for implementing real-time enterprise planning, scheduling and control processes based on information provided by radio frequency identification (RFID) sensing systems. It introduces a new paradigm, called repair, for modeling enterprise processes that is based on the idea of incremental performance improvements and disruption minimization. The proposed model is expressed using differential equations with discontinuous right-hand sides. The repair framework is suitable for implementing enterprise feedback control systems that can easily be interfaced with an existing enterprise resource planning infrastructure. RFID sensing systems have the potential to provide the real-time data needed to implement enterprise feedback functionality.     

An improved formal failure analysis approach for safety-critical system based on MBSA

It is important to analyze the failure in safety-critical system because a disaster may occur once any type of failure mode and/or failure effect is neglected or misjudged. In order to conduct the failure analysis more effectively and efficiently, the concept of formal modeling is introduced. This paper improved the model-based safety analysis (MBSA) working process to optimize the formal failure analysis approach of safety-critical system.As the core works of MBSA process, the formal modeling and model extension aim to build an integrated system model which can be used for analyzing the failure behaviors in the system by model checking. However, in order to automatically check if there are any potential failures in the structured system model and whether the model satisfies the specified system properties and requirements using model checker, model transformation is normally needed, which can introduced potential errors during the transformation. Moreover, different model checkers generally require the system models to be expressed in a particular input language, which increases the difficulty of modeling as well. In order to avoid these problems and improve the efficiency of failure analysis work, this paper focused on how to build an unified model of safety-critical system quickly and accurately using symbolic language SMV, and conduct automatic verification using the corresponding open-source model checker NuSMV soon afterwards. After the model checking, the formal verification results such as counter-examples generated by model checking need to be transformed into traditional failure analysis artifacts, such as FMEA and/or FTA, to guide the iterative improvement of system development conveniently. Therefore, to solve the transformation from formal verification conclusions to traditional failure analysis results is another key point of this paper. Finally, a case study about airborne equipment is provided to validate the proposed method.     

基于VR-CAD系统集成实现虚拟环境中建模

传统计算机辅助设计工具受制于桌面系统非自然的人机界面,而虚拟现实技术(VR)以其沉浸感、交互感等特性为设计师提供了新一代更为自然的交互方式。但由于虚拟环境中缺乏有效的建模工具,产品开发过程中这项技术主要是作为可视化工具使用。作者提出了通过VR-CAD系统集成,利用传统CAD系统所提供的强大建模工具实现虚拟环境中的建模的解决方案。分别从横向集成和纵向集成两个角度出发,文中详细分析了虚拟现实系统和传统计算机辅助设计系统之间的不同连接方式,并基于3DMAX与CUBE采用两种方式进行了集成试验。其中一种是在面片层次上通过Unix和Windows间的Socket通讯将两个软件进行整合,另一种更通用的方法则基于VRML文件的共享。尽管集成系统所能处理的产品模型复杂度还受到一定限制,但初步的结果已经显示出该设想具有很大潜力。     

Formal verification of negotiation protocols for multi-agent manufacturing systems

Formal verification is an important means of tackling behavioural problems such as deadlocks in multi-agent systems. This paper is concerned with the role played by formal verification in the simulation-based performance analysis of multi-agent manufacturing systems. A discrete-event simulation case study is presented to show how varying certain timing parameters of the agent negotiation protocol affects the performance of a multi-agent manufacturing system as well as the chance of getting deadlocks among the software agents. When one tries to determine the optimal values of these timing parameters based on the simulation results, formal verification can help refine the results by confirming whether deadlocks among software agents are indeed possible for particular parameter values. This involves modelling the system's real-time behaviour according to the simulation model and applying the techniques and tools of model checking.     

Formal verification of functional properties of a SCR-style software requirements specification using PVS

Industrial software companies developing safety-critical systems are required to use rigorous safety analysis techniques to demonstrate compliance to regulatory bodies. In this paper, we describe an approach to formal verification of functional properties of requirements for an embedded real-time software written in software cost reduction (SCR)-style language using PVS specification and verification system. Key contributions of the paper include development of an automated method of translating SCR-style requirements into PVS input language as well as identification of property templates often needed in verification. Using specification for a nuclear power plant system, currently in operation, we demonstrate how safety demonstration on requirements can be accomplished while taking advantage of assurance provided by formal methods.     

Optimal Legal Firing Sequence of Petri Nets Using Linear Programming

Petri nets (PNs) are a reliable graphical and mathematical modeling tool for the formal modeling and validation of systems (W. Reisig, A Primer in Petri Net Design, Springer-Verlag: Berlin, Heidelberg, 1992). Applications of PNs include discrete event dynamic systems (DEDS) that are recognized as being concurrent, asynchronous, distributed, parallel, and/or nondeterministic. It is also a powerful formal method for the analysis of concurrent, embedded, and distributed finite state systems (K. Varpaaniemi, Series A: Research Reports, No. 26, Helsinki University of Technology, Digital Systems Laboratory, Oct. 1993). The reachability analysis of PNs is strategically significant as it captures the dynamic behavior of the system as well as providing efficient verification of the correctness of the model. Few linear programming (LP)-based methods can be found that address the reachability problem, and some of these are suitable for optimal control problems. However, due to an inherent state explosion they are difficult to implement; other methods run easily into deadlock as they lack appropriate mechanisms to avoid the firing of critical transitions (T. Matsumoto and A. Tarek, in Proceedings of the 35th IEEE Conference on Decision and Control, Kobe, Japan, 1996-12, pp. 4459–4468). In this paper an improved and easy to implement method is proposed that combines the Optimality Principle and Linear Programming (OP + LP) techniques to find an Optimal Legal Firing Sequence (OLFS) in PNs. This method can be applied to ordinary PNs with self-loops, avoids deadlocks, and can also be used for general PNs having cycles.     

Diagnostic models for engineering process management: A critical review of objectives, constraints and applicable tools

Automated and computer-based systems for the dynamic management of complex engineering processes have been the subject of active research in recent years. Many of these systems have adopted methodology and technology from the field of artificial intelligence and expert system research.

In real-time process diagnosis and process management applications, where model based reasoning may be highly beneficial in terms of speed and functionality, a larger confluence of methods and approaches has started to form. The objective of these applications often includes, besides performing automated fault analysis and diagnosis, also establishing levels of confidence for the results that are obtained. Thus, both deterministic and uncertainty-based models and reasoning frameworks are often needed.

Of interest among the deterministic modeling techniques that can be used in a PMS (Process Management System) are binary trees, rule networks, and graph networks, which in turn include influence diagrams, logic flowgraph methodology and signed directed graph. PMS uncertainty management can be based on formal probabilistic methods, such as Bayesian estimation and updating, or less traditional methods such as certainty factors, Dempster—Schafer theory and fuzzy-set theory. The main features, advantages and disadvantages of the approaches and methods that are suitable for use in a PMS are critically examined and discussed.