Pascal André

The main concern is to ensure the correctness of the components used in sofware architectures. A specification (or a model) is a scientific process which consists in working out an abstraction of a system (existing or not) in order to study and develop a software that implements it. It induces models making it possible mathematically to check the awaited properties of the real system and then to develop it by successive refinements. We study in this topic the model based methods and their application to multiparadigms software architectures. This work should lead in the medium term to the definition of methods and environments for the construction of correct software components with a compositional approach (COSTO/Kmelia project) [AA 05].

In this topic we harness ourselves being studied and elaborating concepts, mechanisms and tools to model and develop components and software with quality (safety, extensibility, maintainability). By safety we mean a correct behaviour, as it is provided by the abstract and later formal specifications. We primarily deal with the verification aspects and checking during the construction of the system by the proof of theorems. With the B method for example, this can be the proof that a concrete level corresponds "well" to an abstract level (refinement). In the framework of UML, this work fits to the concerns of the group pUML [ EBF+ 98, EBF+ 98a ] on the formalization of the UML notation. Contrarily to the majority of works of the field, we do not focus ourselves on a fixed and complete description of a model but on descriptions varying according to the positioning in a development process. Our approach is described in [Andre 02] and constitutes the chapter 4 of [AV 03] (in french). The proof of models (model-checking) is the other class of techniques for verifiying properties like safety and liveness. We propose a customized verification process for UML models that should be supported by a GUI tool.

Two main actions are directed on this topic: model verification on one hand and concepts, models and techniques for software components and services.

BOSCO is a code generator tool: it generates the underlying model (also called repository) for any modeling language expressed in MOF. In other words, it reads XMI files and generates the corresponding source code, in different object-oriented languages (Java, Eiffel, Python, C++). In the case of Java, the generated code implements the JMI interfaces. We participate to the development of the platform and we experiment a customized verification process for UML models. Bosco is an open-source platform available at http://bosco.tigris.org/.

COSTO (COmponent Study TOolkit) is prototype toolbox for the design and the verification of software models based on component and services. These are described using the associated language kmelia. The toolbox already integrates some modules: a \kmelia parser, an architectural correctness checker, a  translator to generate \Lotos processes from the component specifications.
Short description (pdf) and a overview poster available in poster.
The recent trend focus on component model testing as illustrated by the poster.

EV3-Nantes (Lego EV3) gathers several reseauch and teachning resources and works on modelling, verification and code generation from semi-formal models written in UML or SysML.
We propose an original development approach with PIM refinement based on PDM abstractions (top-down/bottom-up)[MEDI2021] with systematic definitions of model transformations ; some are implemented using ATL, Modisco, Papyrus, AgileJ.
The target platform is here a (representative) distributed system made of Java-EV3 et Java-Android programs the object communication between subsystems use Wifi et BlueTooth protocols. Several case studies are used.
The project website is available at EV3-Nantes.

Securité Security is a headache for production managers and CISOs. We must protect data and their confidentiality while ensuring the normal functioning of applications. Security is a broad field that ranges from hardware to applications to communications infrastructure. But it is often not fully taken into account in development and by developers, because it is not considered a priority in terms of suitability for the needs. The work presented here remains on a very modest scale of contribution. The idea is often to define security models and check properties on these models. We address two themes in our work:

• The composition of (web) services to set up high-level services poses security problems when the services called are remote, on other servers and access rights are necessary for the (implicit) execution of these services which can be described as third parties because we do not invoke them directly. We studied this problem in the thesis of Abdramane Bah [Bah20] for which we place ourselves in a federation of servers (Abdramane's Bah PhD).
• Security verification of mobile applications, particularly around access rights, because smartphones contain a lot of personal data and users are little aware of the dangerousness of this or that downloaded application. In Mohammed El Amin Tébib's PhD [Teb+23a,Teb+23b], we take the developer's point of view to intervene during the development of applications; developers are also not specialists in the security vulnerabilities of the code they write or the frameworks they use. (git PrivDroid).
  A specific case is Context-aware mobile app security (CASTAV Project - LCIS-LIG/LS2N (UGA/NU))

In this topic we explore the use of software engineering for Manufacturing systems (HMS). Published in the Sohoma conference series (link)

• Software engineering and Model Driven Engineering for HMS.
• MPCT, a tool for heterogeneous message communications

RODIC (ANR 2022-2026) The RODIC project aims at accelerating the RMS reconfiguration process in both the technical and usage aspects, using a multidisciplinary and model-based approach.

In this topic we explore the capture of informations from the application code in order to asset the quality of models (proof of properties, information system co-evolution).

• Reverse-engineering of component and service based systems to asset safety properties. ECONET project (funded by Egide).
• Model alignment for Enterprise Architecture (poster, tool poster) with SodiFrance.

We also explore since 2020 plagiarism and clone detection in software applications by the prim of models.

• Similarity measure between application source codes ou application models.
• Model comparison for Enterprise Architecture .