建模是软件过程中的基本活动，可以帮助我们更好的理解和构造系统，还可以提供简化和复用的机会。随着软件系统的规模和复杂性的日趋增大，各部件之间的交互活动已成为系统开发过程中规约和建模的重要方面。基于场景的规约（Scenario-Based Specifications）用直观、可视的形式描述系统各部件之间的交互活动，在软件开发过程中扮演了越来越重要的角色。 自ITU-Z120推出厉，消息顺序图（Message Sequence Charts，MSCs）逐渐被工业界接受为基于场景的规约语言。随着OMG推出的统一建模语言（Unified Modeling Language，UML）将类似于MSC的顺序图（Sequence Diagrams）集成其中，类似于MSC的基于场景的规约语言被越来越多的软件开发人员认识并使用。由于系统各部件交互活动相关的复杂性不断增大，基于场景的规约语言的描述能力也不断被提高，原来描述单一场景的MSCs可以用高级消息顺序图（High-Level Message Sequence Chaits，hMSCs）组合成消息顺序图规约（MSC Specifications），从而被用来描述基于多场景的交互活动。 实时系统是一类应用广泛的复杂系统，特别是具有高安全性需求的系统（如航空航天系统、水电控制系统、武器控制系统、医疗卫生系统等）大都是实时系统。时间约束条件是实时系统所要满足的关键需求，在对实时系统各个部件之间的交互活动进行建模的过程中必须要考虑时间因素，从而就形成了基于场景时间规约（Scenario-Based Timing Specification）。为了对基于场景时间约束进行描述，目前都是在现有主流基于场景规约描述语言（如MSC，UML顺序图）中引入时间约束描述机制。 本文主要围绕基于场景时间规约的可达性验证问题展开研究工作，主要内容包括以下几个方面： 1） 给出了MSC和MSC规约的形式化定义，并引入时间约束描述机制使之可以用于描述实时系统。 2） 基于线性规划技术给出了MSC规约的可达性验证算法。给定MSC规约中的某一节点，该算法能够判断是否可以找到一条从起始节点出发的路径片断能够到达该节点，并且要满足这条路径片断上的所有时间约束。在采用正则表达式表示MSC规约路径片断集合的基础上，我们采用线性规划技术检验给定结点是否可达。 3） 对MSC规约的部分可达性验证问题，给出了有效的算法。由于所提出的MSC规约可达性验证算法的复杂度较高，我们针对部分问题进行了优化，给出了有效算法，并进行了实例分析。