V\'erification d'assemblages de composants logiciels : Application aux mod\`eles de composants UML2.0 et Ugatze

TL;DR

This paper presents verification methods for component assemblies in UML2.0 and Ugatze, using formal models and tools to ensure contract coherence across syntax, structure, and behavior.

Contribution

It introduces two approaches, VerifComponentUML2.0 and VerifComponentUgatze, with tools for formal verification of component contracts in UML2.0 and Ugatze models.

Findings

Successful application of verification approaches on UML2.0 and Ugatze models.

Development of tools Wr2fdr and Wright2Ada for contract verification.

Enhanced assurance of component assembly coherence.

Abstract

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.