中文摘要：

为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用UML2.0序列图对模块之间交互行为进行描述.采用基于命题投影时序逻辑的模型检测技术,将对象状态机图转换为Promela模型,系统交互性质转换为命题投影时序逻辑公式,通过模型检测器验证交互模型是否满足于系统的性质,若不满足于该性质,则能够获得反例执行的路径.给出了一个分布式软件系统测试框架,在验证后的序列图模型基础上,使用基于模型的测试用例自动生成方法得到测试用例集合,该集合能够实现对交互行为的有效测试.实例结果表明,该方法可以提高分布式软件系统中模块交互行为的有效性和可靠性.

英文摘要：

To ensure the correctness of interactive behaviors in distributed software systems,an abstraction approach of modular interaction is proposed.First,system state machine diagrams and object state machine diagrams are utilized to describe state transitions while UML2.0sequence diagrams are adopted to express the interactive behaviors.Further,the model checking approach with propositional projection temporal logic（PPTL）is applied to verify whether the interactive modular can satisfy the system properties.Using the algorithms,object state machine diagram is transformed into Promela model,and the desired property of the system is specified by a PPTL formula.As a property specification language,PPTL has the expressive power of both full regular and omega regular expressions.At the same time,it is proper for the specification of state sensitive properties.Within the model checker based on Spin,if the system cannot satisfy the property,a counter-example and the execution path can be found.Finally,a novel framework for testing distributed software is given.Based on the verified sequence diagram,test case generation method can be used to get the set of test cases.Experimental results show that the proposed method is useful in improving the effectiveness and reliability of interactive behaviors in distributed software systems.