基于时序描述逻辑的UML顺序图形式化方法

根据统一建模语言(UML)顺序图的时序特征,提出一种基于时序描述逻辑ALCQIUS的UML顺序图形式化方法。研究ALCQIUS时序扩展部分的语法和语义、ALCQIUS断言公式集一致性定理,给出ALCQIUS断言公式集一致性推理算法,并证明该推理算法的可判定性。以公安报警系统为例,说明基于ALCQIUS的UML顺序图形式化规约和形式化验证具备可行性,并且ALCQIUS为UML顺序图形式化提供了合理的逻辑基础。

一种基于场景的嵌入式软件设计方法

UML顺序图是一种常用的在软件开发早期阶段用来描述系统基于场景的需求规约的一种可视化建模语言。通过在UML顺序图中加入带时间区间标志的时间约束,得到时间顺序图模板TSDT(Timed Sequence Diagram Template),用来建立嵌入式软件基于场景的需求规约模型。对消息传递自动机进行实时扩展,得到时间消息传递自动机TMPA(Timed Message Passing Automata),TMPA以自动机的形式刻画了所建立的需求规约模型,为在需求阶段验证所建立的模型是否满足用户需求奠定了基础。