Extending Statecharts by Under- and Over-Approximation Mechanisms for Top-Down Development Support

状态图及其变体不能适当地支持当前的自上而下开发技术。它们可以被解释为欠近似(细化步骤可能仅添加可能的执行)或过度逼近(细化步骤仅可能移除可能的执行)。然而，对于欠近似和过度近似的组合建模，它们的表现力有限。因此，我们将开发一个状态图变体，它具有从下到上限制可能执行的表达机制，即具有欠近似和过近似描述形式。因此，该状态图变体具有更具表现力的精化概念，这改进了它的使用，例如，用于软件的自上而下的开发。这种扩展的状态图变体的精确语义将在适用于欠近似和过近似的语义模型中给出。这些语义模型将被研究。我们还将为这一扩展的状态图概念制定完善规则。通过构造，这些细化规则是正确的。此外，还将调查有关这一改进概念的核实情况。最后，将给出细化和验证的工具支持。

Statecharts and their variations do not appropriately support current top-down development techniques. They can be interpreted as under-approximation (a refinement step may only add possible executions) or as over-approximation (a refinement step may only remove possible executions). However, they have a limited expressiveness for modeling combinations of under and over-approximation. Therefore, we will develop a statechart variant that has expressive mechanisms for restricting the possible executions from below and also from above, i.e, having both under- and over-approximation description formalisms. This statechart variant has, therefore, a more expressive refinement concept, which improves its usage, e.g., for the top-down development of software. A precise semantics of this extended statechart variant will be given in semantical models appropriate for under- and over-approximation. These semantical models will be investigated. We will also develop refinement rules for this extended notion of statechart. These refinement rules are correct by construction. Furthermore, verification respecting this refinement concept will be investigated. Finally, tool support for refinement and verification will be given.