随着计算机技术应用的日益广泛和深入,软件系统的规模和复杂性不断增大,系统各部分之间的交互及时间约束成为软件需求和设计的重要方面。场景规约作为一种有效的、可视化的系统交互行为描述手段,已经在工业界广泛使用。当前国际主流场景规约描述语言包括消息序列图(Message Sequence Charts,MSC)和统一建模语言(Unified Modeling Language,UML)交互模型图,仅提供了简单的时间约束描述机制,难以满足复杂时间约束的描述需求。在实际应用中,系统通常都由多个场景组合而成,场景组合采用同步或异步的连接方式。对于同步连接的场景规约来说,时间性质分析问题通常被转换为时间自动机上的分析问题,复杂性难以控制;对于异步连接的场景规约来说,时间性质分析问题一般来说都是不可判定问题。本文主要围绕多个场景组合而成的场景规约时间性质分析问题展开研究工作。针对同步连接的场景规约时间性质分析问题,提出了基于场景规约进行直接编码、并将时间性质分析问题转换为线性规划问题的方法,相关分析问题的复杂性得到有效控制;针对不可判定的异步连接场景规约时间性质分析问题,识别出一种称为柔性闭环的场景规约的可判定子类,解决了该类场景规约的可达性分析和有界延时分析问题。本文的主要工作包括以下几个方面:针对场景规约时间性质分析的需求,给出了场景规约的形式化定义,特别是场景规约在同步组合和异步组合语义下的时间行为定义;同时扩充了场景规约的时间约束描述机制,使得时间约束能够描述多个事件之间时间间隔的复杂关系。针对同步连接的场景规约,提出了基于场景规约进行直接编码、将时间性质分析问题转换为线性规划问题的方法,利用成熟的线性规划算法高效地求解,从而把分析问题的复杂性限制在可控的范围内;基于此方法,针对一类"环不受限场景规约",解决了可达性分析、约束一致性分析和有界延时分析问题。针对异步连接的场景规约,识别出一种称为"柔性闭环场景规约"的可判定子类;该类场景规约不限制规约的结构,只对时间约束做限制;解决了该类场景规约的可达性分析和有界延时分析问题。提出了面向路径的场景规约时间性质有界分析方法,在把单路径上时间性质的有界分析问题归约为线性规划问题的基础上,通过优化的深度优先遍历算法对规约中给定阈值内的所有路径进行遍历和分析,从而实现了场景规约时间性质的有界分析,控制了相关复杂性。基于以上工作,实现了一个场景规约的时间性质分析器TASS:Timing Analyzer of Scenario-based Specifications。TASS 具备—个友好的图形化界面用于创建和编辑场景规约,实现上述工作所对应的所有场景规约时间性质分析功能;通过实验显示,在实际应用系统的场景规约案例上,TASS表现出了良好的处理能力和扩展能力。