论文部分内容阅读
为验证并发系统需求设计的正确性，提出一种基于场景的并发系统需求验证方法．首先，用UML顺序图建模并发系统需求场景，通过定义顺序图的操作语义及转换规则，将顺序图的XML描述文件自动转换为Promela程序，而后将描述系统需求的Promela程序和描述系统规约的线性时序逻辑作为模型检测器SPIN的输入，用模型检测的方法自动验证并发系统需求设计的一致性和完备性，最后为证明上述方法的有效性给出一个基于场景的ATM系统需求设计验证实例．实验结果表明，该方法能够有效地发现并发系统需求设计中的错误与不一致，为改进设计提