Pages personnelles et professionnelles
de ThomaS Polacsek

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.

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.

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.

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.

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.

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.

Modular approaches (objects, components and service-based) offer efficient solutions to face the complexity of Information Systems. However, today they involve major problems in dealing with data/information and decisionmaking (from the standpoint of the end- user). In this article, we aim to initiate a dialogue between digital/interaction design and model-driven engineering through the study of a new data representation-visualisation approach based on generative visualisation. Due to recent advances in graphical user interfaces and interaction techniques, we expect to prove that the world of modeling could benefit from creating views of existing models defined in a modeling language complying with Meta-Object Facility.

In software systems engineering, the generally understood goal of verification is to assess the compliance of a software component with respect to the inputs and standards applying to a given phase in the design process. The goal of validation is to determine if the requirements are correct and complete, and validation is performed in the final system assessment phase. Nevertheless, the introduction of formal methods in model based engineering tends to blur the boundary between verification and validation, by allowing validation tasks to be performed early in the process, before the system has been fully designed and implemented. In particular, we consider recent work using constraint satisfaction techniques to perform formal verification and validation tasks at model level. The purpose of this article is twofold. First, we attempt to fit the existing methods and tools in a global design, verification and validation process. Second, we show that in addition to verification and validation, constraint based techniques can be used to automate part of the design activity itself, by synthesizing correct by construction and quantitatively optimal models from a specification.

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.

A general framework for update-based planning is presented. We first give a new family of dependence-based update operators that are well-suited to the representation of simple actions and we identify of query entailment from an update belief base. Then we introduce conditional, nondeterministic and concurrent updates so as to encode the corresponding types of action affect. Plan verification and existence are expressed in this update-based framework.

We study a modal logic of knowledge and action, focussing on test actions. Such knowledge-gathering actions increase the agents knowledge. We propose a semantics, and associate an axiomatics and a rewriting-based proof procedure.

We propose an epistemic dynamic logic EDL able to represent the interactions between action and knowledge that are fundamental to planning under partial observability. EDL enables us to represent incomplete knowledge, nondeterministic actions, observations, sensing actions and conditional plans; it also enables a logical expression of several frequently made assumptions about the nature of the domain, such as determinism, full observability, unobservability, or pure sensing. Plan verification corresponds to checking the validity of a given EDL formula. The allowed plans are conditional, and a key point of our framework is that a plan is meaningful if and only if the branching conditions bear on the knowledge of the agent only, and not on the real world (to which that agent may not have access); this leads us to consider plans that reason which may contain branching conditions referring to implicit knowledge to be evaluated at execution time.