Information Technology Reference
In-Depth Information
5Conluon
This paper presented the logical machinery of a mechanized framework for reason-
ing about structured component systems; especially targeting distributed compo-
nents. We have first illustrated and motivated the specification of components and
the provided proof infrastructure. Furthermore, we have shown this machinery in
action by showing how reconfiguration of components can be formally specified,
and how properties over component structure and reconfiguration can be han-
dled. This paper also illustrated our approach by showing the specification of a
semantics for components, and associated proofs. Overall, the developed frame-
work consists of more than 4000 lines, including almost 300 lemmas and theorems,
approximately 500 lines for defining the component model and its semantics, and
1800 lines focusing on properties specific to future registration which were not pre-
sented here. As usual with mechanised proofs, the main diculty is the choice of
the right structures providing the suitable level of abstraction. Some proofs are
lengthy and technical but no major diculty was encountered.
In contrast to existing works, our approach focuses on increasing confidence in
global properties of component models. For this, we provide a framework and ap-
ply it to prove generally valid results. The established infrastructure of structured
components with asynchronous communication provides an elegant abstraction
from implementation detail while fully preserving the communication structure
and defining a precise semantics. One limiting factor of our framework is that a
precise semantics for components had to be chosen to allow mechanised proofs.
Overall we have developed a reliable basis for the mechanical proofs of proper-
ties of hierarchical component models, and we have shown its adequacy to deal
with first proofs entailing reconfiguration, or component semantics. We addi-
tionally provide subsequent support for distributed components communicating
by asynchronous requests with futures.
A promising follow up project would be to analyse information flows based on
this model, or properties entailing component synchronisation at reconfiguration
time. More generally we expect to prove properties on reconfiguration that will
entail reasoning simultaneously on component execution and on evolution of
component structure. This would show the correctness of complex adaptation
procedures that can be applied in autonomous component systems.
References
[1] Sensoria - software engineering for service-oriented overlay computers (2005)
[2] Abraham, E., Grabe, I., Gruner, A., Steffen, M.: Behavioral interface description
of an object-oriented language with futures and promises. Journal of Logic and
Algebraic Programming 78(1-2), 491-518 (2008)
[3] Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural
models for distributed fractal components. Annales des Telecommunications
64(1-2), 25-43 (2009)
[4] Baude, F., Caromel, D., Dalmasso, C., Danelutto, M., Getov, V., Henrio, L., Perez,
C.: GCM: A Grid Extension to Fractal for Autonomous Distributed Components.
Annals of Telecommunications (2008) (accepted for publication)
