VERIFICATION AND DIAGNOSIS OF COMPUTER SYSTEMS BASED ON DISTRIBUTED CONSTRAINT SATISFACTION OF AGENTS

点击翻译按钮获取中文摘要

This research focuses distributed constraint satisfaction of agents, develops organization of agents for their reasoning ability, and applies it to verification and diagnosis problems of computer systems. The results are summarized by the following four items.1. Verification of software is investigated by formulating termination verification of rewrite systems as constraint satisfaction problems. The method for solving these problems is developed which organizes the agents by using the structure of binary decision diagrams (BDDs). The point is that the agents do not work independently, but share the information by exchanging it through the organized BDD structure, thus making the overall system more efficient.2. Completion procedures of equational systems, a reasoning mechanism for constraint satisfaction of equality-based specifications, are multi-agentified for its application to hardware fault diagnosis in mind. This allows the agents to handle the partial orders in parallel and cooperate via the unique truth maintenance system, leading to efficient constraint satisfaction procedures.3. A reflective computation mechanism is introduced into the rewrite language as a structural framework of epistemic agents for rewrite programs. Message exchange protocols between base- and meta-levels are designed. Axiomatic definition of agents' behavior is developed, while its operational semantics defines the model of computation for agents.4. Agent-based distributed constraint satisfaction systems and fault diagnosis systems on real network environments are implemented in Java-based distributed object-oriented software architecture. The evaluation by typical test problems shows its effectiveness as expected.