A Calculus for Component Evolvability (Extended Abstract)
Résumé
We describe ongoing work on a formal framework for reasoning about dynamically evolvable aggregations of components. The framework relies on an extension of CCS with primitives describing components and evolvability capabilities. We propose and investigate two correctness properties: bounded and eventual adaptation. While bounded adaptation ensures that at most k errors will arise in future states -- including those reachable as a result of dynamic reconfigurations --, eventual adaptation ensures that the system will eventually reach a state from which no other error will arise (i.e., only finitely many errors can occur). We study the decidability of these two adaptation properties in six different variants of the calculus, which represent different evolvability patterns.