Pages personnelles et professionnelles
de ThomaS Polacsek

Ingénierie des exigences, Buts et certification

Je m’intéresse à l’Ingénierie des exigences sous divers aspects. J’ai commencé par utiliser des méthodes formelles pour spécifier les échanges d’information dans une gouvernance partagée face aux crises (veille sanitaire, surveillance et gestion de catastrophes naturelles, etc.). Dans ce contexte, nous avons défini un cadre pour exprimer les tenants et les aboutissants liés aux échanges et à la diffusion d'information. Ce cadre permet de prouver formellement, à l’aide de solveurs, qu’un système remplit bien ses missions d'alertes tout en garantissant la maîtrise de l'information.

Par la suite, je me suis intéressé à la certification et la validation de système et plus particulièrement de système avionique. Pour ce faire, j'utilise des diagrammes de justification, dans divers projets (Européen FP7, avec les autorités de certification DGAC et DGA-TA, Airbus, etc.). Les diagrammes de justification permettent d'organiser et de visualiser, de manière synthétique, tous les éléments clés prouvant la validité d’une propriété pour un produit, ils organisent l’ensemble des éléments de preuves nécessaires à un développement.

Plus récemment, mes travaux se sont portés sur l’Ingénierie des exigences orientée buts, Goal-Oriented Requirements Engineering (GORE).

Publications

• Anouck Chan and Thomas Polacsek,Stroke management: defining and assigning goals to stakeholders Companion Proceedings of the 42nd International Conference on Conceptual Modeling: ER Forum, 2023.
• Anouck Chan, Anthony Fernandes Pires, Thomas Polacsek, Stéphanie Roussel, François Bouissière, Claude Cuiller and Pierre-Eric Dereux,Goal Modelling: Design and Manufacturing in Aeronautics Research Challenges in Information Science: Information Science and the Connected World - 17th International Conference (RCIS'23), 2023.
• Antoine Aubé and Thomas Polacsek, Cloud Migration High-Level Requirements Research Challenges in Information Science: Information Science and the Connected World - 17th International Conference (RCIS'23), 2023.
• Anouck Chan, Anthony Fernandes Pires et Thomas Polacsek, Eliciter, raffiner et attribuer des buts aux bons acteurs à partir d objectifs de haut niveau. Inforsid 2023
• Anouck Chan, Anthony Fernandes Pires, Thomas Polacsek et Stéphanie Roussel, L avion et sa chaîne d assemblage : des premières exigences à une conception globale. Inforsid 2023
• Anouck Chan, Anthony Fernandes Pires and Thomas Polacsek, Trying to Elicit and Assign Goals to the Right Actors Conceptual Modeling - 41st International Conference (ER'22), 2022.
• Anouck Chan, Anthony Fernandes Pires, Thomas Polacsek and Stéphanie Roussel, The Aircraft and Its Manufacturing System: From Early Requirements to Global Design 34th International Conference on Advanced Information Systems Engineering (CAISE'22), 2022.
• Antoine Aubé, Thomas Polacsek et Clément Duffau, Les exigences pour un choix d’architecture dans le cadre d’une migration dans les nuages. Inforsid 2022
• Alex Aquieta Nuñez, Anouck Chan, Alberto Donoso-Arciniega, Thomas Polacsek and Stéphanie Roussel, A Collaborative Model for Connecting Product Design and Assembly Line Design: An Aeronautical Case The Practice of Enterprise Modeling - 14th IFIP WG 8.1 Working Conference, PoEM 2021, 2021.
• Kevin Delmas, Claire Pagetti and Thomas Polacsek, Designing patterns for certification standards and guidelines 32nd International Conference on Advanced Information Systems Engineering (CAISE'20), 2020.
• Thomas Polacsek, Vérification, validation, certification : approches formelles et informelles pour établir la correction des artefacts et des logiciels Habilitation à diriger des recherches (HDR), 2020
• Thomas Polacsek, Sanjiv Sharma, Claude Cuiller and Vincent Tuloup, The need of diagrams based on Toulmin schema application: an aeronautical case study EURO Journal on Decision Processes (EJDP), 6:257, 2018.
• Frédéric Boniol, Youcef Bouchebaba, Julien Brunel, Kevin Delmas, Claire Pagetti, Thomas Polacsek and Nathanaël Sensfelder. PHYLOG: a model-based certification framework. In 37th Digital Avionics Systems Conference (DASC), 2018.
• Clément Duffau , Thomas Polacsek and Mireille Blay-Fornarino, Support of Justification Elicitation: Two Industrial Reports 30th International Conference on Advanced Information Systems Engineering (CAISE'18), 2018.
• Clément Duffau, Thomas Polacsek and Mireille Blay-Fornarino, Une sémantique pour les patrons de justification. Inforsid 2018
• Thomas Polacsek, Diagramme de justification. Un outil pour la validation, la certification et l'accréditation. Ingénierie des Systèmes d'Information 22(2): 95-119 (2017)
• Thomas Polacsek. Validation, Accreditation or Certification: a New Kind of Diagram to Provide Confidence IEEE Tenth International Conference on Research Challenges in Information Science (RCIS'16), 2016.
[abstract]

The aim of the argumentation diagram is to organize and visualize, in a synthetic way, all key elements proving the validity of a product's property. The argumentation diagram does not represent the process, but gives the rationale behind all Verification & Validation (V&V) documents. In fact, it lists and organizes necessary evidence in a development life cycle.
But the validity of the final assessment requires the validation and the identification of the evidence of each intermediate step. So, in this article, we introduce a generic argumentation pattern and its derivations, whose support a rational organization of all V&V evidence at each step. This pattern stems from legal science and argumentation theory legacies, and it is the basic building block for the argumentation diagram construction.

• Rémi Delmas, Thomas Polacsek, Vérification automatique d'exigences pour les politiques d'échange d'information. Journal Ingénierie des Systèmes d'Information Vol.21/2 p39-63 (2016)
• Rémi Delmas and Thomas Polacsek. Need-to-share & non-diffusion requirements verification in exchange policies 27th International Conference on Advanced Information Systems Engineering (CAISE'15), 2015. (springer website)
[abstract]

Whether be it for Earth observation, risk management or even companies relations, more and more interconnected organizations form decentralized systems in which the exchange, in terms of diffusion or non-diffusion of information between agents, can have critical consequences.
In this paper, we present a formal framework to specify information exchange policies for such kinds of systems and two specific requirements, the need-to-share and the non-diffusion requirements, as well as properties strongly related to them. Wiser from these formal definitions, we see how to reconcile these sometimes two antagonist requirements in a same policy specification with information filtering operations. We also explain how we use state of the art theorem provers to perform automatic analysis of these policies.

• Thomas Polacsek. A Process to Support and to Report Collaborative Decision 19th IEEE International Conference on Computer Supported Cooperative Work in Design (CSCWD'15), 2015.
[abstract]

This paper introduces a process to support a collaborative decision made by experts, like collaborative modelling, design choice or collaborative validation, and a formal framework to understand and analyze the final decision. We propose a methodology in two steps: a graphical modeling of the debate to support experts and a more formal framework to record the rationale of the decision. The intended benefits of this methodology are to support the collaborative decision process and to record the motivations of the decision, we illustrate it with an industrial study case.

• Rémi Delmas et Thomas Polacsek. Vérification automatique d'exigences pour les politiques d'échange d'information. Inforsid 2015, 2015.
• Rémi Delmas et Thomas Polacsek. Critical Information Diffusion Systems. Wisard ADBIS 2015 workshop, 2015.
• Rémi Delmas and Thomas Polacsek. Exigences de confidentialité et de diffusion concernant les politiques d échanges d information revue Génie Logiciel, numéro 111, pp. 49-53, 2014. (Article disponible sur HAL)
• Thomas Polacsek. Réflexions sur les liens possibles entre Argumentation et V&V pour le Logiciel Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2014.
• Anthony Fernandes Pires, Thomas Polacsek, Virginie Wiels and Stéphane Duprat. Use of formal methods in embedded software development: stakes, constraints and proposal Embedded Real Time Software and Systems (ERTS2) (Public archive), 2014.
• Anthony Fernandes Pires, Thomas Polacsek, Virginie Wiels and Stéphane Duprat. Vérifier le comportement du code d'un système embarqué à partir de son modèle. Modélisation des Systèmes Réactifs (MSR2013), 2013.
• Anthony Fernandes Pires, Thomas Polacsek, Virginie Wiels and Stéphane Duprat. Behavioural Verification in Embedded Software, from Model to Source Code ACM/IEEE 16th International Conference on Model Driven Engineering Languages and Systems (MODELS2013), 2013.(springer website)
[abstract]

To reduce the verification costs and to be more confident on software, static program analysis offers ways to prove properties on source code. Unfortunately, these techniques are difficult to apprehend and to use for non-specialists. Modelling allows users to specify some aspects of software in an easy way. More precisely, in embedded software, state machine models are frequently used for behavioural design.
The aim of this paper is to bridge the gap between model and code by offering automatic generation of annotations from model to source code. These annotations are then verified by static analysis in order to ensure that the code behaviour conforms to the model-based design. The models we consider are UML state machines with a formal non-ambiguous semantics, the annotation generation and verification is implemented in a tool and applied to a case study.

• Rémi Delmas and Thomas Polacsek. Formal methods for exchange policy specification. 25th International Conference on Advanced Information Systems Engineering (CAISE'2013), 2013.(springer website)
[abstract]

This paper introduces a modelling framework to perform automatic analyses on the specification of an information exchange policy. To avoid the increase of development costs and risks of uncontrolled dissemination of information, the specification errors need to be detected before the implementation phase. We propose a minimalistic core language to unambiguously represent an exchange policy specification and a gateway to logic solvers to verify some properties, namely: completeness, consistency, applicability and minimality. The aim is to check wether the formalisation of an exchange policy is consistent with user expectations.

• Anthony Fernandes Pires, Thomas Polacsek and Stéphane Duprat. Formal software verification at model and at source code levels. 2nd International Conference on Model & Data Engineering (MEDI'2012) , 2012. (paper in hal) (springer website)
[abstract]

In a software development cycle, it is often more than half of the development time that is dedicated to verification activities. Formal methods offer new possibilities for verification. In the specification phase, simulation or model-checking allow users to detect errors in models. In the implementation phase, analysis techniques, like static analysis, make the verification tasks more exhaustive and more automatic. In that context, we propose to take advantage of these methods to improve embedded software development processes based on the V-model.

• Thomas Polacsek and Laurence Cholvy. A Framework to Report and to Analyse a Debate. Proc. IEEE 15th International Conference on Computer Supported Cooperative Work in Design, CSCWD 2011, 2011. (best paper award) (IEEE website)
[abstract]

The paper introduces a framework whereby arguments put forward in a discussion concerning a specific decision can be graphically represented as a directed graph and analysed according to different decision procedures. The intended benefits of the proposed framework are to support a decision manager in the light of the experts' arguments and to record the motivations for the decisions in a corporate memory.

• Thomas Polacsek and Laurence Cholvy. Organize, report and understand an experts' group debate. 4th European Conference for Aerospace Sciences, EUCASS 2011, 2011.