基于场景规约的构件式系统设计分析与验证

使用接口自动机及接口自动机网络来描述构件式系统的行为设计模型,使用UML顺序图表示基于场景的需求规约,对系统设计阶段的构件交互行为的动态兼容性进行形式化分析和检验.通过对接口自动机网络状态空间的分析,给出了一系列算法以检验系统行为的存在一致性以及几种不同形式的强制一致性性质,包括前向强制一致性、逆向强制一致性以及双向强制一致性等.

Checking Component-Based Designs for Scenario-Based Specifications

Component-based system design is becoming more and more popular in software engineering. Checking the important behavioral properties formally in the design phase is an effective way to improve the system reliability. In this paper, the authors consider the problem of checking component-based system designs for scenario-based specifications. Specifically, the authors use the interface automata networks to model the component-based system designs which include a set of interface automata synchronized by shared actions, and the scenario-based specifications are specified by UML sequence diagrams. Based on investigating the reachability graph of the state space of the interface automata networks, the authors develop several algorithms to check the existential consistency and mandatory consistency including the forward, backward and bidirectional consistency.