System automation through policy-based management allows IT administrators to define high-level policies for various management tasks, such as networked systems and applications for business environments, network planning, problem detection, and quality of service provisions. Policies can be understood as specifications; therefore they can be translated more or less easily into formal languages and then be verified by formal techniques such as model checking. In this paper, we focus on formal verification of real-life industrial policies of the Tivoli System Automation for Multi-Platform (TSA). We use PSL to model the system and describe the desired behavior and the RuleBase PE model checker to verify it.
By: Emmanuel Zarpas; Cindy Eisner; Sivan Tal
Published in: H-0254 in 2006
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .