中文摘要：

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

英文摘要：

In order to verify the correctness of requirement design in concurrent systems, this paper proposed a sce nario-based verification method of the requirements of concurrent systems. First, UML sequence diagrams were used to model the requirements scenes of the concurrent systems. By defining the operational semantics and trans formation rules of UML, the XML file of sequence diagrams was automatically converted to the Promela program. Secondly, the Promela program, which describes the system requirements, and linear temporal logic, which de scribes the specifications of a system, were used as the input of the SPIN model checker. Using the model checking method automatically validates the consistency and completeness of the requirement design of concurrent systems. Finally, to prove the validity of the above method, a scenario-based validation instance of requirement design of the ATM system was given. The results show that this method can effectively find the errors and inconsistencies in the requirement design of concurrent systems and help to improve the design.