Synthesis of Configuration Change Procedure Using Model Finder

スポンサーリンク

概要

• 論文の詳細を見る

• Managing the configurations of complex systems consisting of various components requires the combined efforts by multiple domain experts. These experts have extensive knowledge about different components in the system they need to manage but little understanding of the issues outside their individual areas of expertise. As a result, the configuration constraints, changes, and procedures specified by those involved in the management of a complex system are often interrelated with one another without being noticed, and their integration into a coherent procedure for configuration represents a major challenge. The method of synthesizing the configuration procedure introduced in this paper addresses this challenge using a combination of formal specification and model finding techniques. We express the knowledge on system management with this method, which is provided by domain experts as first-order logic formulas in the Alloy specification language, and combine it with system-configuration information and the resulting specification. We then employ the Alloy Analyzer to find a system model that satisfies all the formulas in this specification. The model obtained corresponds to a procedure for system configurations that satisfies all expert-specified constraints. In order to reduce the resources needed in the procedure synthesis, we reduce the length of procedures to be synthesized by defining and using intermediate goal states to divide operation procedures into shorter steps. Finally, we evaluate our method through a case study on a procedure to consolidate virtual machines.

著者

• Hiraishi Kunihiko

  Japan Advanced Inst. Of Sci. And Technol. Nomi‐shi Jpn

• TSUCHIYA Satoshi

  FUJITSU LABORATORIES LTD.

• KIKUCHI Shinji

  FUJITSU LABORATORIES LTD.

関連論文

• Special Section of Selected Papers from the 9th Karuizawa Workshop on Circuits and Systems
• Special Section on Concurrent/Hybrid Systems : Theory and Applications
• A Heuristic Algorithm for One-Machine Just-In-Time Scheduling Problem with Periodic Time Slots
• Special Section on Discrete Mathematics and Its Applications
• Approximate Algorithm for Hybrid Model Predictive Control with Time-Varying Reference
• MLD-Based Modeling of Hybrid Systems with Parameter Uncertainty
• Optimization-Based Synthesis of Self-Triggered Controllers for Networked Systems
• Synthesis of Configuration Change Procedure Using Model Finder
• Self-Triggered Model Predictive Control with Delay Compensation for Networked Control Systems

スポンサーリンク