UML2ADA for Early Verification of Concurrency Inside the UML2.0 Atomic Components

Abstract

In recent years, the Unified Modeling Language (UML) has emerged as a de facto industrial standard for modeling Component-Based Software (CBS). However, in order to ensure the safety and vivacity of UML CBS, many approaches have been proposed to verify the concurrency between interconnected components. But, rare are the works that tackle concurrency verification inside atomic components. In this paper, our purpose was the verification of the concurrency inside UML2.0 atomic components endowed with behavioral specifications described by protocol state machines (PSM). To achieve this, we propose to translate the UML2.0/PSM source component to an Ada concurrent program. Using an Ada formal analysis tool such as FLAVERS or INCA tools, we could detect the potential behavioral concurrency properties such as the deadlock of an Ada concurrent program.