论文部分内容阅读
本文提出了一种形式化模型—TTS4SD,用来描述MARTE规范定义的带时间约束的顺序图的形式语义并在此基础上展开分析。首先给出顺序图的形式定义, 把时间变迁系统(TTS) 扩充成TTS4SD, 用TTS4SD描述顺序图的形式语义, 最后对TTS4SD展开分析工作，这在很大程度上提高了设计阶段模型的正确性。通过一个实例说明从顺序图到TTS4SD 的转化过程以及基于TTS4SD的验证过程。