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.