架构形式化验证的四类性质

软件架构形式化验证是通过模型检验或推理验证的方式，检查架构设计模型中是否存在安全性、活性、公平性、一致性方面的问题。安全性指系统不应该达到的危险状态——”坏的事情永远不会发生”，例如无死锁就是一种安全属性；安全性验证关心的是排除坏结果，而不是保证好结果一定出现。活性指系统应该达到的正确状态——”好的事情最终会发生”，例如某进程发出请求后，该请求总能得到回应；活性验证关心”承诺是否兑现”，即使过程曲折，只要最终能达成期望状态就算满足。公平性指如何保证系统资源被各个任务公平使用，不会导致某些任务长期得不到响应——即”好的事情能否无限重复地发生”；公平性比活性更进一步，它不满足于”好事至少发生一次”，而要求好事能持续、公平地反复发生，防止某个任务被系统无限期”饿死”。一致性指对同一个软件架构，不同人员由于视角不同会产生不同的架构视图，如何用形式化方法验证这些不同视图之间彼此一致——这是唯一一类不针对系统运行行为本身、而针对”人对同一架构的多种描述是否互相矛盾”的性质。这四类性质彼此独立又互补：安全性和活性分别对应”排除坏结果”与”保证好结果”这一对相反的关切；公平性是活性在”重复发生”维度上的加强版；一致性则是前三者的元层面保障——如果连”大家对架构的理解本身是否一致”都验证不了，讨论安全性活性公平性也就失去了共同的基准。