Checking MSC Specifications for Timing Inconsistency

• 作 者: 李宣东 谭文凯 郑国梁
• 机 构: State Key Laboratory for Novel Software Technology, Department of Computer Science and Technology Na
• 出 处: 计算机科学技术学报(英文版)
• 发表日期: 2002年1期
• 关键词: real-time system message sequence chart model checking timing inconsis tency

Message sequence chart (MSC) is a graphical and textual language for the description and specification of the interactions between system components. MSC specifica tions allow convenient expression of multiple scenarios, and offer an intuitive and visual way of describing design requirements. Like any other aspect of the specification and design process, MSCs are amenable to errors, and their analysis is important. In this paper, the verification problem of MSC specification for timing inconsistency is studied, which means that no execu tion scenario described by an MSC specification is timing consistent. An algorithm is developed to check MSC specifications for timing inconsistency.