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.
Part-Whole Formal Specification and Verification of Complex Systems / Pazzi, Luca; Pradelli, Marco. - In: ELECTRONIC COMMUNICATIONS OF THE EASST. - ISSN 1863-2122. - ELETTRONICO. - 40:(2011), pp. 1-21. (Intervento presentato al convegno AVOCS 2010 tenutosi a Duesseldorf (D) nel September 20-23, 2010).