知识卡片

运行态架构验证的一致性、完整性、可追溯性

普通读书笔记卡

内容

系统运行过程中架构会呈现出不同的运行状态,每个状态都是架构在运行中出现的一个实例——运行态软件架构验证就是要验证这些架构实例有没有破坏一致性和完整性,并要求每个实例都能追溯回最初的静态架构。一致性包含四层含义:规约与实现的一致性(运行时刻的修改应及时反映到规约中,避免规约过时);系统内部状态的一致性(正在被修改的部分不应被其他用户或模块同时更改);系统行为的一致性(例如管道-过滤器风格中增加一个过滤器,必须保证该过滤器的输入输出与相连管道的要求一致);架构风格的一致性(演化前后要么风格不变,要么演化为当前风格的”衍生”风格)——这四层揭示了”一致性”这个笼统词汇背后其实是四个独立的检验维度,规约层面的一致性关心文档是否过时,状态层面关心并发安全,行为层面关心接口契约,风格层面关心宏观骨架有没有被破坏性改变。完整性意味着系统演化不能破坏架构规约中的约束(例如限制某组件最多连接1个其他组件,演化中删除或增加相连组件都可能违反这一约束而导致出错),也意味着演化前后系统状态不会丢失,否则系统会变得不安全甚至无法正确运行。可追溯性要求系统的任何一次运行时修改都能被验证并追溯——传统ADL通过逐步精化、把高抽象层次规约精化为可实现的具体规约,用形式化验证保证每步精化都符合要求,从而满足可追溯性;但对动态系统而言,可追溯性必须被延伸到运行时刻。书中指出现有工具对这一点的支持普遍较弱:基于π演算的Darwin、基于CSP的Wright这类形式化系统只能在设计阶段以声明式规约定义受限的几种演化行为,系统实现后架构信息就隐含分散在各模块及其交互中、无法在运行时维护显式的架构视图;ArchStudio用命令式的架构修改语言(AML)和约束语言(ACL)支持运行时修改并在一定程度上保证一致性完整性;ArchJava尝试把架构概念直接引入编程语言、通过语言本身把规约和实现联系起来以保证通信完整性,但代价是软件实现必须依赖这种新型语言,适用范围因此受限——三种工具路线的共同困境是:想要运行时刻的可追溯性,就必须在”表达力”和”实现依赖度”之间做出让步。

参考来源

- 位置:《软件架构理论与实践》第14章《软件架构形式化验证》"14.3.3 运行态软件架构验证"节(源文件:_epub-src/OEBPS/text00114.html) - 结论依据:原文说明一致性的四层含义("①软件架构规约与系统实现的一致性……②系统内部状态的一致性……③系统行为的一致性……④软件架构风格的一致性"),并说明ArchStudio的AML/ACL和ArchJava各自支持运行时可追溯性的方式及局限,直接支撑本卡片结论。 - 原始内容:一致性有4层含义:①软件架构规约与系统实现的一致性,运行时刻的修改应及时地反映到规约中,以保证规约不会过时……ArchJava则尝试把软件架构概念引入编程语言,通过ArchJava语言将规约和实现联系起来,可以保证通信的完整性,但由于软件的实现必须依赖于这种新型语言,使得此方法的适用范围也较为有限。