论文部分内容阅读
在复杂的实时软件系统中使用构件式设计方法，已成为目前软件工程中的研究热点．如何有效地验证实时软件的设计是否满足给定的时间规约，是实时计算领域中的主要挑战之一．通过在接口自动机模型中添加时间区间标记，来扩展其对实时系统接口行为的表达能力；使用实时接口自动机网络柬描述实时软件系统的构件式设计模型；使用带布尔不等式时间约束的UML顺序图表示基于场景的需求规约，对系统设计阶段实时软件构件的动态行为进行形式化分析与检验．通过对实时接口自动机网络状态空间的分析，构造了其可兼容的整型状态等价类空间的可迭图，并在此基础上