Vérification formelle du respect de valeurs morales dans les SMA

International audienceThe increasing use of autonomous artificial agents in hospitals or in transport control systems leads to consider whether moral rules shared by many of us are followed by these agents. This a particularly hard problem because most of these moral rules are often not compatible. In such cases, humans usually follow ethical rules to promote one moral rule or another. Using formal verification to ensure that an agent follows a given ethical rule could help in increasing the confidence in artificial agents. In this article, we show how a set of formal properties can be obtained from an ethical rule ordering conflicting moral rules with respect to a value system. If the behaviour of an agent verifies these properties (which can be proven using our existing proof framework), it means that this agent follows this ethical rule.L’utilisation croissante d’agents autonomes artificiels dans des secteurs comme le milieu hospitalier ou les transports amène à réfléchir au respect de règles morales partagées par tous. Le problème est d’autant plus crucial que les règles morales informellement validées par tous sont souvent incompatibles les unes avec les autres, et que ce sont souvent des règles éthiques qui amènent l’humain, suivant les circonstances, à privilégier telle ou telle règle morale. Utiliser la preuve pour vérifier qu’un agent respecte bien des règles morales et éthiques pourraient aider à accroître la confiance que nous pouvons avoir en de telles unités logicielles. Dans cet article, nous montrons, en nous appuyant sur une étude de cas, comment, à partir de règles morales a priori contradictoires mais ordonnées par des règles éthiques exprimant un système de valeurs, nous parvenons à définir un ensemble de propriétés formelles qui, lorsqu’elles sont établies par un agent, permettent d’assurer que l’agent en question respecte bien la règle éthique souhaitée