UML/OCL standard applied to algorithm validation

Placed at the end of an IDM development process, where the models represent a certain abstraction of the requirements of the applications to be developed, programming is often seen as a simple activity of generating code from the models.

How, in these conditions, can we prove that any program works properly and that the application requirements have been taken into account?

This study deals with the formal properties of programming languages, the aim of which is to reason about programs in order to verify and prove that they work correctly. The addition of axiomatic properties to modeling languages thus enables us to check that models have all the qualities we would expect from them. Axiomatic properties, applied in the context of an IDM process seen as a succession of model transformations, make it possible to check the consistency of all models and programs.

This study follows on from the operational semantics of programming languages, which describe in a precise and rigorous way the behavioral aspects of their syntactic constructs, specified using a grammar. It is therefore of the utmost importance for applications with highly critical requirements, such as those found today in a wide variety of fields, such as aeronautics and space, or for "general public" applications in administration and banking that have to manage masses of personal and private data. Confidence in such software is all the more important as it has to function like a robot, reacting in real time to the different environments it is charged with controlling, managing and supervising, and being available 24 hours a day to respond to user requests via tele-procedures.

After recalling how programs can be reasoned about using logic-based properties (axiomatic properties) to check and prove that they function correctly, we then show how such properties can be defined and applied to check that models located upstream of a development process have the expected qualities. How, then, can such properties be applied when specifying the processing of a system or subsystem described using business modeling languages such as SAM, dedicated to the development of aeronautical applications?

Can we contribute to achieving better continuity between the models and programs of a development process by proposing to apply the same reasoning and proof approaches based on predicate logic? This is the question addressed in this article.