Vérification d'assemblages de composants logiciels : Application aux modèles de composants UML2.0 et Ugatze
This addresses the challenge of component reuse and assembly verification for software engineers, but it appears incremental as it builds on existing models and tools.
The paper tackles the problem of ensuring coherent assembly of software components by proposing a contractual approach with syntactic, structural, semantic, synchronization, and service quality contracts, successfully applying it to UML2.0 and Ugatze models through two verification approaches and tools like Wr2fdr and Wright2Ada.
The component approach aims for the reuse by a coherent and easy components assembly. But obtaining a coherent components assembly is not an easy exercise. To achieve this, we advocate a contractual approach distinguishing different syntactic, structural, semantic, synchronization and service quality contracts. We have successfully applied this approach on two models of semi-formal contractual components: UML2.0 and Ugatze. Indeed, we propose two approaches: VerifComponentUML2.0 and VerifComponentUgatze. The VerifComponentUML2.0 approach aims the verification of syntactic, structural, synchronization and quality service contracts on a UML2.0 component assembly through two formal component models Acme/Armani and Wright. VerifComponentUML2.0 has two tools: Wr2fdr and Wright2Ada. The tool Wr2fdr allows translating Wright expression to CSP contracts in order to verify synchronization using the model checker FDR. It is a IDM tool Wright2Ada which allow is transforming Wright code to Ada, in order to open UML2.0 on static analysis and dynamic tools associated with Ada. VerifComponentUgatze approach provides a frame allowing to check syntactic and structural contracts of an Ugatze component assembly through Acme/Armani.