Formal verification of multi-agent systems behaviour emerging from cognitive task analysis

The main goal of this paper is to present a novel formal approach to the verification of cognitive task analysis (CTA), an analytic tool that has been successfully used in the design of reactive behaviours, on multi-agent architectures. To achieve this, a formal logical system is developed, whose purpose is to formally check the possible success or failure of the resulting implementation. This logic's focus is on modelling an agent's behaviour based on her goals, perceptions and actions. The article starts by giving a brief introduction to current research in reactive systems and cognitive task analysis. Simple definitions are offered of the basic concepts in these fields: agent, object, reactive behaviour, control, etc. As illustration, the paper offers the results of applying CTA to a simple model of postal delivery. Then, the syntax and semantics of the proposed logic are defined. Finally, the logic is applied to the verification of some of the behaviours resulting of the previous CTA analysis.     

Abstraction and composition: a verification method for co-operating systems

Behaviour of systems is described by formal languages: the sets of all sequences of actions. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of important information when moving to the abstract level, abstracting homomorphisms have to satisfy a certain property called simplicity on the concrete (i.e. not abstracted) behaviour. To be suitable for verification of so called co-operating systems, a modified type of satisfaction relation for system properties (approximate satisfaction) is considered. The well known state space explosion problem is tackled by a compositional method formalized by so called co-operation products of formal languages.     

Ontology-based reconfiguration agent for intelligent mechatronic systems in flexible manufacturing

This paper proposes a novel approach to achieving fast reconfiguration of modular manufacturing systems, based on an ontology-based reconfiguration agent. The agent uses ontological knowledge of the manufacturing environment for the purpose of reconfiguration without human intervention. The current mass customization era requires increased flexibility and agility in the manufacturing systems to adapt changes in manufacturing requirements and environments. Our configuration agent minimises the overheads of the current reconfiguration process by automating it. It infers facts about the manufacturing environment from the ontological knowledge model and then decides whether the current environment can support the given manufacturing requirements. This paper proposes the agent architecture enabling the integration between the high level planning with the distributed low level control compliant with the upcoming IEC 61499 function blocks standard.     

Safety verification and reachability analysis for hybrid systems

Safety verification and reachability analysis for hybrid systems is a very active research domain. Many approaches that seem quite different, have been proposed to solve this complex problem. This paper presents an overview of various approaches for autonomous, continuous-time hybrid systems and presents them with respect to basic problems related to verification.     

Ontology-based feature mapping and verification between CAD systems

Data interoperability between computer-aided design (CAD) systems remains a major obstacle in the information integration and exchange in a collaborative engineering environment. The use of CAD data exchange standards causes the loss of design intent such as construction history, features, parameters, and constraints, whereas existing research on feature-based data exchange only focuses on class-level feature definitions and does not support instance-level verification, which causes ambiguity in data exchange. In this paper, a hybrid ontology approach is proposed to allow for the full exchange of both feature definition semantics and geometric construction data. A shared base ontology is used to convey the most fundamental elements of CAD systems for geometry and topology, which is to both maximize flexibility and minimize information loss. A three-branch hybrid CAD feature model that includes feature operation information at the boundary representation level is constructed. Instance-level feature information in the form of the base ontology is then translated to local ontologies of individual CAD systems during the rule-based mapping and verification process. A combination of the Ontology Web Language (OWL) and Semantic Web Rule Language (SWRL) is used to represent feature classes and properties and automatically classify them by a reasoner in the target system, which requires no knowledge about the source system.     

基于Ontology的用户模型研究

针对现有本体用户模型的难点与不足，提出了一种改进的基于领域本体的用户模型（OBUM），利用文本挖掘技术构建领域本体，通过本体学习来完成用户模型的学习和更新。     

A form verification system for the conceptual design of complex mechanical systems

This paper presents a summary of research into the development and implementation of a domain-independent, computer-based model for the conceptual design of complex mechanical systems [1]. The creation of such a design model includes the integration of four major concepts: (1) the use of a graphical display for visualizing the conceptual design attributes: (2) the proper representation of the complex data and diverse knowledge reguired to design the system; (3) the integration of quality design methods into the conceptual design: (4) the modeling of the conceptual design process as a mapping between functions and forms. Using the design of an automobile as a case study, a design environment was created which consisted of a distributed problem-solving paradigm and a parametric graphical display. The requirements of the design problem with respect to data representation and design processing were evaluated and a process model was specified. The resulting vehicle design system consists of a tight integration between a blackboard system and a parametric design system. The completed system allows a designer to view graphical representations of the candidate conceptual designs that the blackhoard system generates.     

Abstraction-based verification of codiagnosability for discrete event systems

In this paper, we investigate the verification of codiagnosability for discrete event systems (DES). That is, it is desired to ascertain if the occurrence of system faults can be detected based on the information of multiple local sites that partially observe the overall DES. As an improvement of existing codiagnosability tests that resort to the original DES with a potentially computationally infeasible state space, we propose a method that employs an abstracted system model on a smaller state space for the codiagnosability verification. Furthermore, we show that this abstraction can be computed without explicitly evaluating the state space of the original model in the practical case where the DES is composed of multiple subsystems.     

A computational model of time for stiff hybrid systems applied to control synthesis

Computation has quickly become of paramount importance in the design of engineered systems, both to support their features as well as their design. Tool support for high-level modeling formalisms has endowed design specifications with executable semantics. Such specifications typically include not only discrete-time and discrete-event behavior, but also continuous-time behavior that is stiff from a numerical integration perspective. The resulting stiff hybrid dynamic systems necessitate variable-step solvers to simulate the continuous-time behavior as well as solver algorithms for the simulation of discrete-time and discrete-event behavior. The combined solvers rely on complex computer code which makes it difficult to directly solve design tasks with the executable specifications. To further leverage the executable specifications in design, this work aims to formalize the semantics of stiff hybrid dynamic systems at a declarative level by removing implementation detail and only retaining ‘what’ the computer code does and not ‘how’ it does it. A stream-based approach is adopted to formalize variable-step solver semantics and to establish a computational model of time that supports discrete-time and discrete-event behavior. The corresponding declarative formalization is amenable to computational methods and it is shown how model checking can automatically generate, or synthesize, a feedforward control strategy for a stiff hybrid dynamic system. Specifically, a stamper in a surface mount device is controlled to maintain a low acceleration of the stamped component for a prescribed minimum duration of time.     

Design and verification of a coordination protocol for cooperating systems

 This paper proposes an approach to producing a verified design of a complex intelligent system. The system is modeled using a hierarchical structure based on a coordination protocol. The coordination protocol and the system architecture are described using a state machine representation. The Clarke-McMillan Symbolic Model Checker based on branching time temporal logic is used to verify some of the desired formal properties of the protocol such as completeness, boundedness and termination. This work shows that the model checker helps to bring the automatic verification of complex intelligent systems closer to a practical proposition.     

基于Ontology的信息抽取

为了提高Internet上的信息搜索效率,基于内容的搜索引擎成为迫切的用户需求。但内容信息的手工获取是一项繁重的工作。从文本或半结构化文档中自动地抽取用户关心的内容信息且表示成计算机能理解的形式是一项极具实用价值的挑战性研究。该文从知识表示与推理的角度研究了提高信息抽取智能性的途径,提出了将Ontology与模板规则相结合的技术,并针对线性模板表示的局限提出了基于二侧树结构的模板规则表示,同时实现了此表示下的假设生成———冲突消解推理。该技术成功地应用于招聘广告的信息抽取。     

Ontology-based assembly design and information sharing for collaborative product development

To realize a truly collaborative product design and development process, effective communication among design collaborators is a must. In other words, the design intent that is imposed in a product design should be seized and interpreted properly; heterogeneous modeling terms should be semantically processed both by design collaborators and intelligent systems. Ontologies in the Semantic Web can explicitly represent semantics and promote integrated and consistent access to data and services. Thus, if an ontology is used in a heterogeneous and distributed design collaboration, it will explicitly and persistently represent engineering relations that are imposed in an assembly design. Design intent can be captured by reasoning, and, in turn, as reasoned facts, it can be propagated and shared with design collaborators. This paper presents a new paradigm of ontology-based assembly design. In the framework, an assembly design (AsD) ontology serves as a formal, explicit specification of assembly design so that it makes assembly knowledge both machine-interpretable and to be shared. An Assembly Relation Model (ARM) is enhanced using ontologies that represent engineering, spatial, assembly, and joining relations of assembly in a way that promotes collaborative assembly information-sharing environments. In the developed AsD ontology, implicit AsD constraints are explicitly represented using OWL (Web Ontology Language) and SWRL (Semantic Web Rule Language). This paper shows that the ability of the AsD ontology to be reasoned can capture both assembly and joining intents by a demonstration with a realistic mechanical assembly. Finally, this paper presents a new assembly design information-sharing framework and an assembly design browser for a collaborative product development.     

A framework for the verification of infinite-state graph transformation systems

We propose a technique for the analysis of infinite-state graph transformation systems, based on the construction of finite structures approximating their behaviour. Following a classical approach, one can construct a chain of finite under-approximations (k-truncations) of the Winskel style unfolding of a graph grammar. More interestingly, also a chain of finite over-approximations (k-coverings) of the unfolding can be constructed. The fact that k-truncations and k-coverings approximate the unfolding with arbitrary accuracy is formalised by showing that both chains converge (in a categorical sense) to the full unfolding. We discuss how the finite over- and under-approximations can be used to check properties of systems modelled by graph transformation systems, illustrating this with some small examples. We also describe the Augur tool, which provides a partial implementation of the proposed constructions, and has been used for the verification of larger case studies.     

Automatic verification for a class of distributed systems

Summary. The paper presents a new analysis method for a class of concurrent systems which are formed of several interacting components with the same structure. The model for these systems is composed of a control process and a set of homogeneous user processes. The control and user processes are modeled by finite labeled state transition systems which interact by means of enabling functions and triggering mechanisms. Based on this structure, an analysis method is presented which allows system properties, derived by reachability analysis for a finite number of user processes, to be generalized to an arbitrary number of user processes. A procedure for the automatic verification of properties such as mutual exclusion and absence of deadlocks is presented and is then used to provide for the first time a fully automated verification of the Lamport's fast mutual exclusion algorithm. Received: October 1998/Accepted January 2000     

基于本体的分层抽象模型

KRA表示模型给出了对物理世界W进行形式化建模的一般框架。在扩展后的广义KRA模型中引入本体概念,将抽象对象库扩展为本体类,在本体类中实现KRA模型框架中的感知层、语言层和理论层的知识共享和重用,简化了KRA模型的表示。分别定义了作用在物理世界W和本体类上的3种本体抽象算子(集):基本本体抽象算子、实体本体抽象算子集和连接本体抽象算子集,并给出了本体类之间的映射关系,通过这种映射关系能够实现模型抽象和模型还原。对本体类的抽象度进行形式化的定义,并给出了相关定理,指出在这样的框架中利用抽象映射可以自动构建物理世界W的抽象度不同的模型。     

基于本体的XML Schema生成方法

本体能够精确地描述概念体系和领域知识。该文提出了一种基于本体生成XMLSchema的方法。根据这一方法,可以提高XMLSchema的语义表达能力,最终提高XML文档在概念层次上描述的准确性。     

PHAVer: algorithmic verification of hybrid systems past HyTech

In 1995, HyTech broke new ground as a potentially powerful tool for verifying hybrid systems. But due to practical and systematic limitations it is only applicable to relatively simple systems. We address the main problems of HyTech with PHAVer, a new tool for the exact verification of safety properties of hybrid systems with piecewise constant bounds on the derivatives, so-called linear hybrid automata. Affine dynamics are handled by on-the-fly overapproximation and partitioning of the state space based on user-provided constraints and the dynamics of the system. PHAVer features exact arithmetic in a robust implementation that, based on the Parma Polyhedra Library, supports arbitrarily large numbers. To force termination and manage the complexity of the polyhedral computations, we propose methods to conservatively limit the number of bits and constraints of polyhedra. Experimental results for a navigation benchmark and a tunnel diode circuit demonstrate the effectiveness of the approach. A preliminary version of this paper appeared in the Proceedings of Hybrid Systems: Computation and Control (HSCC 2005), Lecture Notes in Computer Science 3414, Springer-Verlag, 2005, pp. 258–273.     

Ontology-based similarity for product information retrieval

Product development of today is becoming increasingly knowledge intensive. Specifically, design teams face considerable challenges in making effective use of increasing amounts of information. In order to support product information retrieval and reuse, one approach is to use case-based reasoning (CBR) in which problems are solved “by using or adapting solutions to old problems.” In CBR, a case includes both a representation of the problem and a solution to that problem. Case-based reasoning uses similarity measures to identify cases which are more relevant to the problem to be solved. However, most non-numeric similarity measures are based on syntactic grounds, which often fail to produce good matches when confronted with the meaning associated to the words they compare. To overcome this limitation, ontologies can be used to produce similarity measures that are based on semantics. This paper presents an ontology-based approach that can determine the similarity between two classes using feature-based similarity measures that replace features with attributes. The proposed approach is evaluated against other existing similarities. Finally, the effectiveness of the proposed approach is illustrated with a case study on product–service–system design problems.     

基于本体的特征模型演化的一致性验证

针对特征模型的演化导致特征间的冲突问题, 从特征模型的演化方面进行研究, 提出了一种基于本体的特征模型演化的一致性验证方法。首先采用本体理论方法对特征模型的演化进行分析和建模, 建立本体的特征模型元模型; 其次基于上述元模型, 为网上购物系统实例建立相应的网上购物的领域特征模型, 根据需求裁剪出产品特征模型; 然后在Eclipse集成开发环境下, 通过Jena推理机加载规则和产品特征模型进行一致性验证, 当检测到冲突时, 采用演化策略来消除冲突; 最后通过实例研究说明了该方法的有效性。     

基于本体的知识门户

提出一种基于本体的知识门户，它建立了用户与知识之间的联系，通过提供个人化和自适应的交互手段，帮助用户方便地找到需要的知识或知识载体并与之交流，并为用户提供快速准确的知识导航和交流环境。为实现对知识门户中信息的智能访问和提供，提出一个本体驱动基于Agent的知识门户框架，通过将本体作为一个概念级支持提供访问和构造知识门户的方式，从而将传统索引和搜索方案中基于关键词的方式扩展到基于知识的方式，同时也讨论了该系统的最显著特点和知识提供的方法。