INPI-France/Brevets-Francais-2024-Chunked huggingface dataset:
On notera par ailleurs que les première et deuxième configurations ci-dessus ne sont pas incompatibles. Le sous-module 24A est par exemple inclus dans ou équivalent au sous-module 26A, tandis que le sous-module 24B peut dans certains cas être considéré comme équivalent au(x) sous-module(s) 26B et/ou 26C.
Un procédé de validation formelle d’un système physique électronique ou électromécanique définissable par modélisation selon un principe d’ingénierie des systèmes à l’aide du système informatique 10 de la va maintenant être détaillé en référence à la .
Au cours d’une première étape 100 exécutée dans un environnement logiciel E1 de modélisation, un ensemble structuré de spécifications techniques 32 du système physique, exprimées dans un langage de modélisation prédéterminé compatible avec l’environnement E1, est enregistré en mémoire 14. Comme indiqué précédemment, l’environnement logiciel E1 est par exemple Matlab et le langage de modélisation prédéterminé est alors Simulink, ou l’environnement logiciel E1 est par exemple OpenModelica ou Dymola et le langage de modélisation prédéterminé est alors Modelica.
Au cours d’une étape suivante 102, l’interface utilisateur UI 20 du module solveur 20 propose à un utilisateur le choix entre plusieurs solveurs, notamment les solveurs S1, S2 et S3 dans l’exemple non limitatif de la . Parmi ces solveurs, le solveur S1 est apte à vérifier les propriétés de validation P1, …, PN de l’ensemble structuré de spécifications techniques 32 à partir des premiers modèles de validation précités.
Si c’est le solveur S1 qui est choisi, le procédé de validation formelle passe donc à une étape 104 au cours de laquelle le module fonctionnel 18 de la plate-forme logicielle 16 exécutée par le processeur 12 ayant accès à la mémoire 14 traite l’ensemble structuré de spécifications techniques 32 pour engendrer, de façon connue en soi, des premiers modèles de validation MV à partir en outre des propriétés de validation précitées P1, …, PN. Ces dernières peuvent être définies, soit au cours de l’étape 100, soit de façon totalement indépendante.
Puis le procédé de validation formelle passe à une étape 106 d’exécution du solveur S1 pour la vérification des propriétés de validation P1, …, PN de l’ensemble structuré de spécifications techniques 32 à partir des premiers modèles de validation MV. Comme indiqué précédemment, ce sont les négations des premiers modèles de validation MV qui sont fournies en entrée du solveur S1 et ce dernier est apte à renvoyer un résultat RES sous la forme de réponses SAT, UNSAT ou UNKNOWN, un exemple pouvant alors être optionnellement associé à chaque réponse SAT, c’est-à-dire à chaque modèle de validation non vérifié.
Si c’est un autre solveur que le solveur S1 qui est choisi, c’est-à-dire un solveur non applicable aux premiers modèles de validation, par exemple le solveur S2 ou S3, le procédé de validation formelle passe à l’exécution de cet autre solveur pour la vérification des propriétés de validation P1, …, PN de l’ensemble structuré de spécifications techniques 32. Mais cela ne se fait pas directement à partir des premiers modèles de validation MV. Conformément aux principes généraux de la présente invention, cela se fait par la génération, à partir de l’ensemble structuré de spécifications techniques 32, de requêtes REQ’’ exécutables par cet autre solveur pour la vérification des propriétés de validation P1, …, PN de l’ensemble structuré de spécifications techniques 32.
Cette génération de requêtes REQ’’ comporte par exemple une étape 108 de traduction de l’ensemble structuré de spécifications techniques 32 dans un format commun d’interprétation prédéterminé, par exemple Python, d’un environnement logiciel E2 (i.e. celui de Python) autre que le langage de modélisation de l’environnement logiciel E1 qui a permis d’exprimer l’ensemble structuré de spécifications techniques 32. On obtient alors un ensemble structuré de spécifications techniques 32’ traduites dans ce format commun d’interprétation prédéterminé, c’est-à-dire sous Python par exemple. L’étape 108 est exécutée par le sous-module 26A du module fonctionnel 26 ou par le sous-module 24A du module fonctionnel 24.
La génération de requêtes REQ’’ comporte par exemple en outre une étape 110 de génération de deuxièmes modèles de validation MV’, par exemple sous Python, à partir de l’ensemble structuré de spécifications techniques 32’ exprimées dans le format commun d’interprétation et des propriétés de validation P1, …, PN. Cette étape est exécutée par le sous-module 26B du module fonctionnel 26 ou par le sous-module 24B du module fonctionnel 24. Pour l’exécution de cette étape, il est possible d’envisager un menu contextuel dédié à la validation formelle et pouvant être ouvert par l’utilisateur afin de choisir quelles propriétés de validation vérifier pour les spécifications techniques étudiées.
La génération de requêtes REQ’’ comporte par exemple en outre une étape 112 de génération des requêtes REQ’’ à partir des deuxièmes modèles de validation MV’. Les requêtes REQ’’ sont exprimées dans un environnement logiciel E3 qui est celui du solveur S2 ou S3 sélectionné. Cette étape est exécutée par le sous-module 26C du module fonctionnel 26 ou par le sous-module 24B du module fonctionnel 24. Elle est optionnelle. En effet, il peut arriver que les deuxièmes modèles de validation MV’ soient en fait exprimés sous forme de requêtes directement exploitables par le solveur S2 ou S3 sélectionné, i.e. MV’ = REQ’’, l’environnement logiciel E3 étant alors notamment le même que E2.
En variante, on notera que les deuxièmes modèles de validation MV’ peuvent être engendrés directement par traduction des premiers modèles de validation MV, par exécution d’un module fonctionnel, équivalent aux modules 24 et 26 mais non représenté sur la , au cours d’une étape 108’ se substituant aux étapes 108 et 110. Dans ce cas, l’étape 104 de génération des premiers modèles de validation MV doit être exécutée même si ce n’est pas le premier solveur S1 qui a été sélectionné à l’étape 102.
En variante également, on notera que l’étape 104 peut précéder l’étape 102 s’il est considéré que, quel que soit le choix de solveur réalisé à l’étape 102, il est nécessaire d’engendrer les premiers modèles de validation MV, notamment si c’est l’étape 108’, et non la succession d’étapes 108 et 110, qui est exécutée pour l’obtention des deuxièmes modèles de validation MV’ lorsqu’un autre solveur que S1 est choisi.
Suite à la succession d’étapes 108, 110 et 112, ou suite aux étapes 108 et 110, ou suite aux étapes 108’ et 112, ou suite à l’étape 108’, le procédé de validation formelle passe à une étape 114 d’exécution du solveur S2 ou S3 sélectionné pour la vérification des propriétés de validation P1, …, PN de l’ensemble structuré de spécifications techniques 32 à partir des requêtes REQ’’. Comme indiqué précédemment, ce sont les négations des deuxièmes modèles de validation MV’ qui sont fournies sous forme de requêtes en entrée du solveur S2 ou S3 sélectionné et ce dernier est apte à renvoyer un résultat RES’’ sous la forme de réponses SAT, UNSAT ou UNKNOWN, un exemple pouvant alors être optionnellement associé à chaque réponse SAT, c’est-à-dire à chaque modèle de validation non vérifié.
De façon optionnelle mais avantageuse, compte tenu du fait que les environnements logiciels E1, E2 et E3 sont potentiellement différents, le procédé de validation formelle peut en outre comporter au moins une étape de traduction du résultat RES’’ dans un format tel qui aurait été fourni par le premier solveur S1 dans l’environnement E1. Le résultat RES’’ est ainsi traduit en un résultat RES’ conforme à l’environnement logiciel E2 au cours d’une étape 116 et le résultat RES’ est traduit pour obtenir le résultat RES conforme à l’environnement logiciel E1 au cours d’une étape finale 118. En variante, notamment lorsque l’environnement E3 est E2, le résultat RES’’ peut être directement traduit en RES. Dans l’exemple non limitatif de la , les étapes 116 et 118 sont réalisées par exécution du module fonctionnel 28 ou 30, respectivement pour le solveur S2 ou S3.
Un premier exemple concret d’application de la présente invention va maintenant être détaillé. Il s’agit de pouvoir valider formellement un système physique modélisé dans le langage de modélisation Modelica sous environnement OpenModelica (i.e. environnement E1) à l’aide d’un solveur SMT, non inclus dans OpenModelica, sous un environnement de ce solveur compatible avec la bibliothèque logicielle SMT-LIB (i.e. environnement E3 différent de E1).
Le système physique est modélisé dans le langage Modelica au cours de l’étape 100.
Au cours de l’étape 102, l’utilisateur opte pour le solveur SMT non inclus dans OpenModelica, par exemple S2 ou S3. Les étapes 104 et 106 ne sont alors pas exécutées.
Au cours de l’étape 108, l’ensemble structuré de spécifications techniques 32 exprimées en langage Modelica est transformé en un ensemble d’équations à arbres syntaxiques pouvant lui-même être interprété à l’aide de la bibliothèque logicielle SMT-LIB. Cette transformation est réalisée sous environnement logiciel Python (i.e. l’environnement E2) qui permet de bénéficier de la bibliothèque logicielle OMPython pour interagir avec OpenModelica.
Les spécifications techniques se présentent sous la forme d’une structure de données contenant : le nom d’un fichier contenant les spécifications ; les sorties du système physique et leurs types ; les conditions PBR associées à chaque sortie. Cette description du système physique est rédigée par l’utilisateur. Elle peut aussi être au moins en partie automatisée, ce qui est possible si les spécifications sont rédigées en suivant certaines conventions.
Un exemple de description partielle de système physique est :
Project_descriptor_exemple2 = {
'file' : 'Exemple.mo',
'PBRs' : {
'signal_val' : ('Real', [
('Exemple.PBRSum.C','Exemple.PBRSum.D'),
('Exemple.PBRProd.C', 'Exemple.PBRProd.D'),
]),
'threshold_crossed' : ('Bool', [
Cependant, la présence de la couche 105 de phosphure d’indium diminue toujours l’efficacité quantique du capteur à certaines longueurs d’onde de lumière visible, typiquement autour de 600nm. En outre, l’utilisation d’une même couche d’InGaAs 104 pour la détection des ondes visibles et infrarouges signifie que les dimensions et l’espacement des pixels visibles doivent être les mêmes que pour les pixels SWIR. La résolution du capteur est donc limitée par la résolution des pixels sensibles aux rayons infrarouge, qui est typiquement bien moindre que celle qu’on souhaiterait obtenir pour des pixels sensibles aux ondes visibles. Cette solution ne permet donc pas d’obtenir une résolution satisfaisante pour les pixels sensibles à la lumière visible.
Afin de remédier à ces inconvénients, l’invention propose un procédé de fabrication d’un capteur d’image pour la détection de la lumière visible et des rayons infrarouges à ondes courtes, le procédé comprenant les étapes suivantes : fourniture d’un substrat support comprenant un premier matériau semiconducteur ; formation, dans le substrat support, de cavités afin de définir des pixels sensibles à la lumière visible dans le premier matériau semiconducteur entre lesdites cavités ; formation d’une couche protectrice électriquement isolante au moins sur les surfaces latérales de chaque pixel sensible à la lumière visible ; croissance, dans les cavités, d’un second matériau, différent du premier matériau, de sorte à former des pixels sensibles aux rayons infrarouges à ondes courtes.
Ainsi, l’invention permet d’obtenir un capteur sensible à la fois aux rayons lumineux du spectre visible et aux rayons infrarouges à ondes courtes, dont les pixels sensibles à ces deux types de rayons sont situés dans un même plan, sans avoir à empiler verticalement des couches successives de matériaux semi-conducteurs. Le capteur ainsi obtenu n’a pas de perte d’efficacité quantique, et la résolution de ses pixels sensibles aux rayons lumineux visible n’est pas limitée par celle de ses pixels sensibles aux rayons infrarouges à ondes courtes.
Selon un mode de réalisation, le procédé comprend, entre l’étape a et l’étape b, une étape a’ de formation d’un film protecteur du substrat support, pour protéger les pixels sensibles à la lumière visible lors de l’étape b de formation des cavités ; et entre l’étape c et l’étape d, une étape c’ de retrait du film protecteur afin d’exposer la surface supérieure des pixels sensibles à la lumière visible.
Selon un mode de réalisation, le procédé comprend, entre l’étape a et l’étape b, une étape a’ de formation d’un film protecteur du substrat support, pour protéger les pixels sensibles à la lumière visible lors de l’étape b de formation des cavités ; et après l’étape d, une étape d’ de retrait du film protecteur afin d’exposer la surface supérieure des pixels sensibles à la lumière visible.
Selon un mode de réalisation, l’étape c comprend la formation de la couche protectrice par recuit thermique rapide.
Selon un mode de réalisation, le premier matériau semiconducteur est du silicium.
Selon un mode de réalisation, le second matériau semiconducteur est un semiconducteur III-V, préférentiellement choisi parmi le phosphure d’indium, l’arséniure d’indium gallium, des alliages de germanium, ou des points quantiques, par exemple des points quantiques colloïdaux à base de sulfure de plomb(II).
Selon un mode de réalisation, le substrat support est de type silicium sur isolant, et comprend successivement un substrat de base, une couche intermédiaire électriquement isolante et une couche monocristalline du premier matériau semiconducteur.
Selon un mode de réalisation, le procédé comprend, entre l’étape b et l’étape c, une étape b’ d’épaississement de la couche monocristalline par homo-épitaxie.
Selon un mode de réalisation, l’étape b est une étape de gravure pratiquée dans le substrat support jusqu’à atteindre la couche intermédiaire électriquement isolante.
Selon un mode de réalisation, le procédé comprend après l’étape c, et éventuellement l’étape c’, une étape c’’ de retrait, dans les cavités, du matériau formant la couche intermédiaire électriquement isolante, et en ce que les pixels sensibles aux rayons infrarouges à ondes courtes sont formés, à l’étape d, sur la face du substrat de base révélée par l’étape c’’ de retrait.
Selon un mode de réalisation, le substrat support est un substrat massif du premier matériau semiconducteur.
L’invention propose en outre un capteur d’image pour la détection de la lumière visible et des rayons infrarouges à ondes courtes, comprenant : un substrat support ; une pluralité de pixels sensibles à la lumière visible, formés dans le substrat support, et de pixels sensibles aux rayons infrarouges à ondes courtes, lesdits pixels sensibles aux rayons infrarouges étant disposés sur une région superficielle du substrat support ; une couche protectrice disposée au moins sur les parois latérales de chaque pixel de sorte à isoler électriquement chaque pixel des pixels adjacents ;
les pixels formant un agencement disposé sur un même plan.
Selon un mode de réalisation, le substrat support est de type silicium sur isolant (SOI), comprenant successivement un substrat de base dans un matériau semiconducteur, une couche intermédiaire électriquement isolante et une couche monocristalline dans un matériau semiconducteur.
Le dispositif de contrôle 3110 peut comporter une ou plusieurs unités centrales de traitement (CPU), et peut contrôler chaque élément du dispositif utilisateur 3601 pour réaliser des fonctions liées au contrôle de communication, au traitement de signal audio, au contrôle du traitement de signal audio, au traitement et au contrôle de l’image fixe et animée et à d’autres types de traitement de signal. Le dispositif de contrôle 3110 peut réaliser ces fonctions en exécutant des instructions stockées dans une mémoire 3150. En variante ou en plus du stockage local de la mémoire 150, les fonctions peuvent être exécutées en utilisant des instructions stockées sur un dispositif externe dont l’accès se fait sur un réseau ou sur un support lisible par ordinateur non transitoire. Comme décrit ci-dessus en lien avec la , le dispositif de contrôle 3110 peut exécuter des instructions permettant au dispositif de contrôle 3110 de fonctionner comme l’unité de contrôle d’affichage 3211, l’unité de gestion des opérations 3212 et l’unité de gestion du jeu 3213 schématisées sur la .
Bien entendu, de nombreuses modifications et variations de la présente invention sont possibles à la lumière des enseignements ci-dessus. Il est donc entendu que, dans le cadre des revendications annexées, l’invention peut être mise en pratique autrement que comme cela est spécifiquement décrit dans les présentes.
Procédé de détermination d’au moins un paramètre colorimétrique caractérisant une composition cosmétique, dispositif électronique de détermination et produit programme d’ordinateur associés La présente invention concerne un procédé de détermination d’au moins un paramètre colorimétrique. La présente invention concerne également un produit programme d’ordinateur et un dispositif électronique de détermination associés.
La présente invention concerne le domaine des produits cosmétiques, préférentiellement des compositions cosmétiques pour la coloration de poils, notamment des cheveux.
Plus généralement, un « produit cosmétique » est un produit tel que défini dans le
Règlement CEN-1223/2009 du Parlement Européen et du Conseil daté du 30 novembre
2009, relatif aux produits cosmétiques.
La personnalisation de produits et services cosmétiques peut concerner n’importe quelle partie du corps humain mais revêt un intérêt tout particulier pour les parties corporelles exposées, telles que le visage (produits de maquillage ou de soin), et les cheveux ou une barbe le cas échéant (produits de coloration par exemple).
Dans le domaine des compositions cosmétiques pour la coloration de poil(s), notamment de cheveux, de nouvelles compositions cosmétiques sont régulièrement développées pour s’adapter à la demande des utilisateurs.
Ces nouvelles compositions cosmétiques visent, dans un premier cas, à atteindre une nouvelle couleur ou un nouvel effet visuel des poils sur lesquels elles sont appliqués. Dans un deuxième cas, ces nouvelles compositions cosmétiques visent à atteindre une couleur déjà connue mais comprennent des composants qui n’étaient pas précédemment utilisés à cet effet. Ce deuxième cas est particulièrement intéressant lorsque l’approvisionnement en certains composants devient difficile, s’accompagne de coûts élevés, ou présente un risque pour l’environnement
Toutefois, l’obtention de nouvelles compositions cosmétiques résulte d’un processus long et complexe.
Tout d’abord, des experts chimistes développent des prototypes de compositions cosmétiques. Ces prototypes résultent de l’expérience des experts chimistes et sont régis par certains principes chimiques.
Ensuite, ces prototypes sont testés individuellement en laboratoire pour vérifier que l’effet visuel obtenu est conforme aux attentes des experts chimistes.
Dans certains cas et de façon imprévisible, l’effet visuel associée à un prototype nouvellement développé n’est pas conforme aux attentes. Il n’est donc pas toujours possible de capitaliser sur le travail des experts chimistes ayant développé ces prototypes.
Il existe donc un besoin pour des outils permettant de simplifier le développement d’une nouvelle composition cosmétique.
('Exemple.PBRCrossed.C','Exemple.PBRCrossed.D'),
Dans cet exemple, le fichier 'Exemple.mo' est lui-même un fichier en langage Modelica contenant des données de description du système physique considéré.
Dans cet exemple également, certaines données descriptives peuvent être représentées en blocs fonctionnels organisés visuellement, ce qui est par exemple le cas de la condition 'Exemple.PBRSum.C' qui est illustrée en partie supérieure gauche de la .
Comme par ailleurs illustré sur cette même figure, la transformation 108 comporte une première sous-étape éventuelle 200 de récupération d’une version instanciée (i.e. les causes et les effets de chaque condition PBR) de chaque fonction de la représentation en blocs fonctionnels, lorsque cette version instanciée n’est pas initialement disponible. La version instanciée d’une fonction est une version textuelle où tous les objets sont remplacés par la définition de la fonction dont ils dépendent. Elle est donc composée d’un ensemble de déclarations de variables et d’équations. Une telle version instanciée peut être obtenue, de façon connue en soi, directement en utilisant OMPython, notamment à l’aide de la commande « InstanciateModel ».
La transformation 108 comporte une deuxième sous-étape 202 d’analyse logicielle syntaxique et lexicale de ces fonctions instanciées. Cette sous-étape est réalisée à l’aide de l’outil Python Lex-Yacc qui permet de créer facilement des lexeurs et des parseurs. Le résultat obtenu est une liste d’équations exprimées dans un langage se présentant sous forme d’arbres syntaxiques, assez proche de la syntaxe des termes de la bibliothèque logicielle SMT-LIB.
Enfin, la transformation 108 comporte une troisième sous-étape 204 d’interprétation de cet ensemble d’équations sous forme d’arbres syntaxiques en une fonction SMT-LIB. Cette fois-ci, c’est la gestion native par SMT-LIB des équations et des quantificateurs existentiels qui aide à représenter les fonctions voulues sous la forme de spécifications techniques 32’ traduites dans le format commun de l’environnement E2.
On notera que la représentation en arbres syntaxiques précitée ne peut théoriquement être obtenue que s’il n’y a pas de boucles dans les conditions PBR de l’ensemble structuré de spécifications techniques 32. De manière générale, ces boucles ne sont pas utilisées puisque cela engendre des boucles algébriques, c’est-à-dire des boucles de dépendances qui sont insolubles. Pour éviter de telles boucles algébriques, il est possible d’avoir recours à des blocs de mémoire, ce qui permet de supprimer les dépendances cycliques en ajoutant des délais. Ce recours aux blocs de mémoire n’est cependant toujours pas compatible avec la représentation sous forme d’arbre. Pour résoudre ce nouveau problème, chaque bloc de mémoire pourrait être transformé en une sortie du système (sa valeur à l’état courant) et une entrée du système (sa valeur à l’état précédent). Mais cela peut poser des problèmes lors de la validation formelle, puisque cela ajoute des entrées sans lien entre elles, alors qu’elles en ont potentiellement un. Par exemple, une fonction f(a) = a + pre(a) + pre(a) pourrait devenir f(a, p1, p2) = a + p1 + p2, en perdant l’information p1 = p2.
Pour ce qui est de l’exécution de l’étape 110, c’est-à-dire la génération des deuxièmes modèles de validation MV’, il suffit d’appliquer les résultats obtenus à la troisième étape 204 de la transformation 108 aux propriétés de validation P1, …, PN. Cela consiste tout simplement à exprimer ces propriétés sous forme de formules logiques, à partir des spécifications techniques 32’, le tout dans un langage mathématique. Le langage de la bibliothèque logicielle SMT-LIB étant très proche d’un langage mathématique, il est rapide et aisé d’obtenir les formules mathématiques à vérifier. Celles-ci sont ensuite insérées dans une requête « SMT-LIB template » de la forme suivante, qui permet de demander au solveur SMT si la propriété est valide :
; Initialisation
(set-logic ALL)(set-option :produce-models true)
; Déclaration des variables
(declare-const x1 Int) (declare-const x2 Real) …
; Déclaration de l’objectif de preuve
La sélection peut se faire par exemple selon une règle prédéterminée. Cette règle peut par exemple comprendre la sélection d’un élément d’émission selon un ordre défini par sa position sur la dalle et/ou le motif correspondant(e).
Lors d’une étape suivante 120, le premier module 22 introduit une modulation particulière dans le signal élémentaire à émettre par l’élément d’émission à tester, à travers les unités de formation expliquées précédemment. Cela se fait alors en place ou en supplément du signal élémentaire nominal à émettre par cet élément d’émission.
Cette modulation particulière comprend par exemple l’introduction dans le signal élémentaire à émettre, d’une phase (et/ou retard) et amplitude supplémentaires, dans chaque intervalle temporel ΔT prédéterminé.