策略驱动的自配置系统形式化建模及分析验证 - 计算机工程与科学.pdf

维普资讯 CN43-1258／TP 计算机工程与科学 2008年第3O卷第 2期 ISSN 1007—130X COMPUTERENGINEERING SCIENCE V01．3O。No．2，2008 文章编号：1007—130X(2008)02-0147-04 策略驱动的自配置系统形式化建模及分析验证’ A FormalModelingandVerificationFramework forPolicy-DrivenSelf—C0nfigurati0nSystems 林煜明。蔡国永 LIN Y~-ming，CAIGuo-yong (桂林电子科技大学计算机与控制学院，广西 桂林 541004) (SchoolofComputerandControl，GuilinUniversityofElectronicsTechnology，Guilin541004，China) 摘 要 ：使计算机系统具有 自主配置的能力，可以解决复杂系统面临配置管理难度高和强度大的问题。本文针对策略 驱动的自配置系统的配置 问题，提 出采用CPN建模技术对该类系统进行建模、分析与验证，保证系统 自配置过程的正确 性；分析了策略驱动 自配置系统的基本结构，构造 出该类系统的CPN模型，引入 CTL的扩展——Asl(-CTL描述系统配置 过程中具备的性质；最后用CPNTools2．2．0进行仿真与验证。 Abstract：A natura1waytosolvetheproblemsarisingin theconfigurationofcomplexsystemsistOmakethesystems self-conflgurable．Tovalidatetheconfiguringprocessofpolicy-drivense1f-c0nfiguringsystme s，aframeworkbasedoncolor Petrinet(CPN)isproposed．Thebasicinfrastructureofpo licy-drivenself-configuringsystemsisanalyzed，andaCPN model ofthesystem isbuilt．Todescribetheimportantpropertiesoftheconfiguringprocess，na extendde CTLcalledASK-CTLis usedtOspecifytherequirements．Thesmiulationandverificationofthepropertiesarecraride outwithCPN Too ls2．2．0． 关键词：自配置；策略驱动；CPN模型；仿真；验证 Keyw0rds：self-configuration；po licy-driven；CPN mode1；simulation；verification 中图分类号：TP311 文献标识码：A 究大多集 中于 自配置系统的框架组成或某个特定应用方 l 引言 面，缺乏形式化模型，从而不能有效地描述和验证系统的行 为性质。然而，在系统 自配置的过程中，配置过程的正确性 随着计算机技术的快速发展，系统复杂性的不断提高 是系统正常运行的关键，否则可能导致系统崩溃。因此，有 使管理和配置大型复杂系统的难度和强度逐渐到达人的能 必要对配置过程进行形式化的描述及分析验证。基于上述 力极限，并且有时需要配置人员在数秒钟 内对配置问题做