Modularity and Part-Whole Compositionality for Computing the State Semantics of Statecharts

The paper discusses modularity and compositionality issues in state-based modeling formalisms and presents related recent research results. Part-Whole State charts provide modular constructs to traditional State charts in order to allow incremental and fully reusable composition of behavioral abstractions, enforcing explicitly the coordinated systemic behavior and bringing benefits to subsequent modeling and implementation phases. The paper shows that Part-Whole State charts have a computable semantics, which can be specified through a constraint-driven specification method. Such a method allows to specify and verify the intended meaning of states directly at design time, thus avoiding to employ less effective verification techniques, such as exhaustive testing or model checking.