Part-Whole Formal Specification and Verification of Complex Systems

The paper explores the overall feasibility and possible advantages of part-whole hierarchical state-based modeling with respect to formal specification and verification. It is shown, partly by a running example, that the identification of pattern of coordinated behavior allows to partition the overall complexity of a state based design by self-contained and uncoupled modules. Such modules can be incrementally validated against specification constraints, thus allowing to reuse al- ready validated modules. Finally, the proposed approach interleaves validation and design, forcing the designer to transform specification statements into state proposi- tions which further improve understandability