3. IDM process. UML activity diagram and SAM

The aim of this paragraph is to show how these assertion annotation techniques can be applied to reasoning at the IDM process level. We take the UML activity diagram as an example, followed by the SAM modeling workshop. We show the value of integrating proof techniques at the modeling level to describe algorithms at different modeling levels, before code generation itself. It should be noted that UML is a general modeling language, whereas the SAM workshop is a DSL (Domain Specific Language) specialized in taking into account the requirements of specific domains such as aeronautics, for example.