论文部分内容阅读
针对网构软件行为中的不确定性和不完整性，提出了一种支持协商的网构软件体系结构行为建模与验证方法，在建模中，该方法借鉴了UML时序图元素表示法，并增加了建模元素支持行为的不确定与不完整建模在验证中，除了集成广泛应用的模型检查工具Spin以提供行为模型的验证能力以外，还引入了基于反例引导的抽象，精化过程思想的协商检查，以解决不确定和不完整建模所带来的正确性验证问题。