Components monitoring through formal specifications

The paper presents a specification-based approach for runtime monitoring of components in the field of component-based software engineering. The conformance of a component is checked with respect to a formal specification given in terms of Abstract State Machines. The validity of the approach is proved showing how the technique can be used for the monitoring of web services developed using Axis2. The theoretical approach is implemented in a technical framework where Java annotations are used to link the web service with its formal specification, and AspectJ is used to check the conformance runtime.