One of the key research challenges in autonomic computing is to define rigorous mathematical models for specifying, analyzing, and verifying high-level self-* policies. This paper presents the FracToy formal methodology to specify self-configurable component-based systems, and particularly both their component-based architectural description and their self-configuration policies. This rigorous methodology is based on the first-order relational logic, and is implemented with the Alloy formal specication language. The paper presents the dierent steps of the FracToy methodology and illustrates them on a self-configurable component-based example.