The aim of the paper is to provide a practical method to introduce design principles typical of the object-oriented approach, like “design by extension”, to the application domain of manufacturing systems control design. The proposed method is based on a domain-specific extension of the modeling language UML and on the formalization of design models as transition systems for verification purposes. Object-oriented models, formalized according to the proposed semantics, can be analyzed with model checking techniques in order to verify the behavioral conformity of object classes, according to a notion of substitutability which is defined in the paper specifically for the proposed modeling language
Verification of behavioral substitutability in object-oriented models for industrial controllers
BONFE', Marcello;
2005
Abstract
The aim of the paper is to provide a practical method to introduce design principles typical of the object-oriented approach, like “design by extension”, to the application domain of manufacturing systems control design. The proposed method is based on a domain-specific extension of the modeling language UML and on the formalization of design models as transition systems for verification purposes. Object-oriented models, formalized according to the proposed semantics, can be analyzed with model checking techniques in order to verify the behavioral conformity of object classes, according to a notion of substitutability which is defined in the paper specifically for the proposed modeling languageI documenti in SFERA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
