ThomaS Polacsek's
home page

Requirements Engineering, Goals and Certification

I work on Requirements Engineering from several angles. Early on, I used formal methods to specify information exchanges in shared governance during crises, developing a framework to formally prove that a system meets its intended missions.

Later, I focused on system certification and validation, especially for avionics, using justification diagrams to model and to organize all the evidence supporting a system’s properties. These diagrams help ensure that all key elements are considered in the development process.

More recently, I have been working on Goal-Oriented Requirements Engineering (GORE), exploring how to combine formal methods, like optimization, with goal-based approaches, and developing techniques to capture expert knowledge effectively.

Publications

• Anouck Chan, Anthony Fernandes Pires, Thomas Polacsek, Stéphanie Roussel, François Bouissière, Claude Cuiller, Pierre-Eric Dereux, Goal modelling in aeronautics: Practical applications for aircraft and manufacturing designs Data & Knowledge Engineering (Data Knowl. Eng. 155: 102375), 2025.
• Anouck Chan, Thomas Polacsek, Stéphanie Roussel, Exploring Goal Relationships in Satellite Assembly Line Design DB&IS 2024, 2024. (best paper award)
• Anouck Chan, Janis Stirna, Jelena Zdravkovic, Thomas Polacsek, Simon Hacks, Janis Grabis, Claudio Favi, Towards a New Method for Designing Manufacturing Capabilities DB&IS 2024, 2024.
• Anouck Chan, Thomas Polacsek, Brieuc Danet, Application of KJ Method in an Aeronautics Collaborative Project 17th IFIP WG 8.1 Working Conference on the Practice of Enterprise Modeling Forum (PoEM Companion 2024), 2024.
• 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 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.
• 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, 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.
• 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 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.
• 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.