Self-adapting software adapts its behavior in an autonomic way, by dynamically adding, suppressing and recomposing components, and by the use of computational reflection. One way to enforce software robustness while adding adaptative behavior is disposing of a formal support allowing these programs to be modeled, and their properties specified and verified. We propose FracL, a formal framework for specifying and reasoning about dynamic reconfiguration programs being written in a Fractal-like programming style. The Fractal component model supports a simple and extensible set of component reflection capabilities, enabling the definition of reconfiguration wherein component based systems. The proposed framework is founded on first order logic, and allows the specification and proof of properties concerning either functional concerns or control concerns. An encoding of our model using the Focal spec
M. Simonot, M. Aponte