This thesis investigates a method for tackling the verification of parametric systems, systems whose behaviour may depend on the value of one or more parameters. The range of allowable values for such parameters may, in general, be large or unknown. This results in a large number of instances of a system that require verification, one instance for each allowable combination of parameter values. When one or more parameters are unbounded, the family of systems that require verification becomes infinite. Computer protocols are one example of such parametric systems. They may have parameters such as the maximum sequence number or the maximum number of retransmissions. Traditional protocol verification approaches usually only analyse and verify properties of a parametric system for a small range of parameter values. It is impossible to verify in this way every concrete instance of an infinite family of systems. Also, the number of reachable states tends to increase dramatically with increasing parameter values, and thus the well known state explosion phenomenon also limits the range of parameters for which the system can be analysed. In this thesis, we concentrate on the parametric verification of the Stop-and-Wait Protocol (SWP), an elementary flow control protocol. We have used Coloured Petri Nets (CPNs) to model the SWP, operating over an in-order but lossy medium, with two unbounded parameters: the maximum sequence number; and the maximum number of retransmissions. A novel method has been used for symbolically representing the parametric reachability graph of our parametric SWP CPN model. This parametric reachability graph captures exactly the infinite family of reachability graphs resulting from the infinite family of SWP CPNs. The parametric reachability graph is represented symbolically as a set of closed-form algebraic expressions for the nodes and arcs of the reachability graph, expressed in terms of the two parameters. By analysing the reachability graphs of the SWP CPN model for small parameter values, structural regularities in the reachability graphs were identified and exploited to develop the appropriate algebraic expressions for the parametric reachability graph. These expressions can be analysed and manipulated directly, thus the properties that are verified from these expressions are verified for all instances of the system. Several properties of the SWP that are able to be verified directly from the parametric reachability graph have been identified. These include a proof of the size of the parametric reachability graph in terms of both parameters, absence of deadlocks (undesired terminal states), absence of livelocks (undesirable cycles of behaviour from which the protocol cannot escape), absence of dead transitions (actions that can never occur) and the upper bounds on the content of the underlying communication channel. These are verified from the algebraic expressions and thus hold for all parameter values. Significantly, language analysis is also carried out on the parametric SWP. The parametric reachability graph is translated into a parametric Finite State Automaton (FSA), capturing symbolically the infinite set of protocol languages (i.e. sequences of user observable events) by means of similar algebraic expressions to those of the parametric reachability graph. Standard FSA reduction techniques were applied in a symbolic fashion directly to the parametric FSA, firstly to obtain a deterministic representation of the parametric FSA, then to obtain an equivalent minimised FSA. It was found that the determinisation procedure removed the effect of the maximum number of retransmissions parameter, and the minimisation procedure removed the effect of the maximum sequence number parameter. Conformance of all instances of the SWP over both parameters to its desired service language is proved. The development of algebraic expressions to represent the infinite class of Stop-and-Wait Protocols, and the verification of properties (including language analysis) directly from these algebraic expressions, has demonstrated the potential of this method for the verification of more general parametric systems. This thesis provides a significant contribution toward the development of a general parametric verification methodology.

Les systèmes de production manufacturiers sont une classe des systèmes à événements discrets. Leur taille nécessite de distribuer le logiciel de contrôle sur une architecture industrielle de plusieurs ordinateurs reliés en réseau. Dans ce contexte, il devient essentiel d'être capable d'évaluer l'impact d'une architecture réseau spécifique sur les services des systèmes manufacturiers en termes de la performance et la qualité. Les performances du réseau sous-jacent peuvent notamment nuire à la productivité du système. Dans la méthodologie traditionnelle proposée dans la littérature, cet aspect n'est pas pris en compte au niveau conception. Cependant, la modélisation de tels systèmes est importante pour vérifier certaines propriétés. Dans cette thèse, nous proposons une approche de modélisation par composants à l’aide des réseaux de Petri haut niveau pour la modélisation de certains protocoles de réseaux afin d'évaluer les systèmes manufacturiers comme étant des systèmes distribués. La sélection des réseaux de Petri est justifiée par leur pouvoir d'expression en ce qui concerne la modélisation des systèmes distribués et concurrents. L’approche par composants permet de diminuer la complexité de la modélisation et encourage la généricité, la modularité et la réutilisabilité des composants prêt-à-utiliser. Cela permet de construire facilement de nouveaux modèles et de réduire les coûts de développement de systèmes. En outre, cela peut aider à une meilleure gestion des services et des protocoles et à changer facilement/modifier un élément du système. Notre modélisation permet enfin d'évaluer ces systèmes par le biais de simulations centralisées / Manufacturing systems belong to the class of distributed discrete event systems. Their size requires distributing the software to control them on architecture of several industrial computers connected by networks. In this context, it becomes crucial to be able to evaluate the impact of a specific architecture on the manufacturing systems services both in terms of performance and quality. The performance of the underlying network can notably affect the productivity of the system. In traditional methodology proposed in literature, this aspect is not taken into account in the design stage. Thus, modeling such systems is important to verify some properties at that stage. In this thesis, we propose a component-based modeling approach with High Level Petri nets based method for modeling some network protocols in order to evaluate the manufacturing systems as being distributed systems. The selection of Petri nets is justified by their expression power with regard to the modeling of distributed and concurrent systems. Component-based approach can decrease modeling complexity and encourages genericity, modularity and reusability of ready-to-use components. This allows building new models easily and reducing the systems development cost. Moreover, this can help in better managing services and protocols and to easily change/modify a system element. Finally, this modeling enables us to evaluate discrete event systems by means of centralized simulations

Cette thèse a été réalisée dans le cadre du projet « Gestion et Optimisation de la Chaîne Documentaire », projet labellisé par le Pôle de compétitivité des Industries du Commerce. Le projet a pour but de concevoir et de développer un nouveau workflow et un outil d’aide à la décision. Ce système doit être capable de gérer et d’optimiser le flux complet dématérialisé de contrats reçus à COFIDIS.Nous présentons d’abord le framework retenu dans le cadre du projet pour modéliser et implémenter le workflow. En phase de conception BPMN a été choisi. Pour la partie développement, l’utilisation de BPEL a été préconisée pour implémenter et exécuter l'application finale (services web).Cependant la flexibilité offerte par BPMN peut conduire à des propriétés indésirables du processus telles que blocage et inaccessibilité. De plus, BPMN a été conçu pour fournir des modèles Orientés Process. Les données ou les ressources y sont donc peu représentées. En conséquence, l'analyse de performance sur un modèle BPMN est quasi inexistante.Afin de surmonter ces problèmes nous proposons d’insérer dans le framework deux nouvelles phases. Ces deux phases sont appliquées au modèle BPMN. La première est une phase de vérification et de validation et la deuxième une phase d'optimisation. Ces deux phases sont réalisées en transformant le modèle BPMN vers un langage formel. Notre choix dans ce travail a été d'utiliser les réseaux de Petri. Ce qui nous a permis de vérifier et de valider de bonnes propriétés du process. Quant à l’optimisation, nous avons défini une nouvelle variante du problème d’affectation (bin packing problem) et proposé une résolution à intégrer dans le processus d’aide à la décision / This thesis has been realized as a part of the project GOCD (French acronym for Management and optimization of document life cycle) and within the context of the French competitive cluster PICOM. The project aims to design and develop a new paperless workflow system and decision making tool to replace the current paper based system. The new workflow system must manage and optimize received credit demands at COFIDIS.The first part of this thesis presents and discusses a framework to model and implement workflow systems. The proposed framework allows more flexibility in workflow reengineering process and operational analysis for different business process. The proposed framework uses the most recent and promising language to model and execute workflow the Business Process Modeling Notation (BPMN) and Business Process Execution Language (BPEL).The flexibility offered by BPMN can also lead to undesirable properties for business process such as deadlocks and unreachablity. More, BPMN notation was designed to model business process, and little consideration was concentrated to represent data and resources. As a result, carrying out performance analysis on a BPMN model is also limited.To overcome these problems, we propose two additional phases in the reengineering process. They are applied to the target BPMN model. The first phase is verification and validation and the second one is optimization. These two phases are realized by transforming the BPMN model to a formal language, Petri nets. As for optimization, a new variant of bin packing problem has been defined. And we propose to integrate its resolution in a decision making tool

Le but de ce rapport est de présenter une méthode globale de développement à partir de spécifications informelles, depuis la modélisation graphique des exigences temporelles d'un système ferroviaire critique jusqu'à une implantation systématique au moyen de méthodes formelles. Nous proposons d'utiliser ici les réseaux de Petri temporels pour décrire le comportement attendu du logiciel de contrôle-commande à construire.Tout d'abord nous construisons un modèle des exigences p-temporel prenant en compte toutes les contraintes que doit vérifier le système. Nous proposons des outils et des méthodes capables de valider et de vérifier ce modèle. Ensuite, il s'agit de construire un modèle de processus solution en réseau de Petri t-temporel. Ce modèle illustre des exigences techniques relatives à un choix technologique ou architectural. L'objectif est double : tout d'abord il est nécessaire de vérifier la traçabilité des exigences ; ensuite, il faut vérifier que l'ensemble des exigences sources sont bien implémentées dans la solution préconisée et dans sa mise en oeuvre. Enfin, nous proposons une approche visant à transformer de façon systématique le modèle de processus en machine abstraite $B$ afin de poursuivre une procédure formelle $B$ classique. Finalement, le cas d'étude du passage à niveau, composant critique dans le domaine de la sécurité ferroviaire est décrit / The introduction of new European standards for railway safety, coupled with an increasing use of software technology changes the method of development of critical railway systems. Indeed, new systems have to be at least as good as the previous ones. Therefore the appropriate safety level of critical systems has to be proved in order to obtain the necessary approval from the authorities. Accordingly a high level of reliability and correctness must be reached by the use of mathematical proofs and then formal methods. We focus on the treatment of the temporal requirements in the level crossing case study which is modelled with p-time Petri nets, and on the translation of this model in a more formal way by using the B method. This paper introduces a methodology to analyse the safety of timed discrete event systems. First, our goal is to take out the forbidden state highlighted by a p-time Petri net modelling. This model deals with the requirements of the considered system and has to contain all the constraints that have to be respected. Then we aim at describing a process identified as a solution of the system functioning. This method consists in exploring all the possible behaviours of the system by means of the construction of state classes. Finally, we check if the proposed process corresponds to the requirements model previously built.Our case-study is the level crossing, a critical component for the safety of railway systems

Les systèmes complexes ferroviaires étant de plus en plus contraints par des autorités de décision placées à un haut niveau d'abstraction, il devient problématique d'imposer des critères à une autre échelle que fonctionnelle. Ainsi, dès lors que l'on descend plus bas, nous sommes confrontés à des spécificités des systèmes nationaux qui font perdre la généralité du travail des décisionnaires Européens. Le problème est qu'à chaque niveau d'abstraction, des méthodes d'évaluation du risque existent, mais sans être compatibles entre elles. Par ailleurs, la combinaison des couches et la vision fonctionnelle du système ne prennent pas en compte l'impact des fonctions les unes sur les autres, ni le lien entre le niveau global et les composants afin d'allouer la sécurité.Nous proposons donc une démarche harmonisée d'évaluation du risque, capable de répartir les contraintes définies au niveau fonctionnel abstrait sur les entités qui implémentent les systèmes avec leurs spécificités.Notre contribution est méthodologique. Elle part d'un modèle fonctionnel du système ferroviaire constitué en couches. Le but étant de représenter ce système sans dépendance entre les fonctions, il a fallu les traduire indépendamment des autres en faisant apparaître les entrées/sorties comme des places/transitions d'un réseau de Petri. A chaque couche de la décomposition correspond une classe de réseau de Petri. Ainsi, à la couche structurelle, nous associons les réseaux de Petri Temporels; à la couche fonctionnelle les réseaux de Petri stochastiques et à la couche logique les réseaux de Petri Prédicats Transitions / The railway systems are being more and more forced by decision authorities. As they are placed at a high level of abstraction, it becomes problematic to impose another criterion or scale. In fact, since we come down lower, we are confronted with specificities of the national systems which make lose the majority of the work of the European decision-makers. The issue is that, at every level of abstraction, risk assessment methods exist, but without being compatible. Besides, the combination of layers and the functional vision of the railway system do not take into account the impact of some functions on the others, nor the link between the global level of risk and the components to assign the safety.Thus, we propose a harmonized approach for risk assessment. This approach allows us to distribute the constraints defined at the abstract functional level on the entities which implement both the systems and their specificities.Our contribution is methodological. It leaves a functional model of the layered railway system. The purpose is to represent this system without any dependencies between the functions. For instance, it was necessary to translate them independently by creating entrances/exits as places/transitions of a Petri net. A Petri net class corresponds to each layer. To the structural layer, we associate the time Petri net; to the functional layer, the stochastic Petri nets and to the logical layer, the predicate transitions nets

Les services de stérilisation sont des lieux de production de soins caractérisés par une multitude d’activités et situations auxquelles ils sont confrontés. En outre, les services de stérilisation doivent assurer leurs missions dans un environnement caractérisé par la présence d’une variété de risques. Les risques présents dans ces milieux peuvent aller des pannes des équipements jusqu’aux contaminations et transmission des maladies nosocomiales. Ces services sont aussi tenus de garder un niveau de performances satisfaisant pour assurer la continuité des soins dans les blocs opératoires.Pour aider ces services dans leur quête d'un système performant, capable d’évoluer dans un environnement à haut niveau de risques, nous nous intéressons dans ce travail de recherche au développement d’une approche intégrée pour l’analyse de risques et l’évaluation des performances. Ce travail s’intègre dans un cadre collaboratif entre le laboratoire G-SCOP et le service de stérilisation du CHU de Grenoble, terrain d’étude choisi pour mettre en œuvre l’approche proposée.L'approche que nous proposons se déroule en plusieurs étapes: tout d’abord, suite à une comparaison entre les méthodes de gestion des risques, nous nous sommes orientés vers l’approche pilotée par modèle, dénommée FIS (Fonction Interaction Structure). En nous basant sur FIS, nous avons développé un modèle de risque dans ce service de stérilisation, décrivant à la fois les fonctions, les ressources permettant la réalisation de ces fonctions ainsi que les différents risques qui peuvent être rencontrés. Dans un deuxième temps, nous avons représenté le comportement dynamique du modèle de risques obtenu. Ce modèle dynamique permet de simuler le comportement du service de stérilisation et le voir évoluer dans les situations normales de fonctionnement et les situations de risques. Pour ce faire, nous avons introduit une nouvelle classe de réseau de Petri appelée réseau de Petri PTPS (Predicate-Transition, Prioritized, Synchronous) permettant de représenter et simuler le comportement dynamique du modèle FIS. Par la suite, nous avons automatisé le passage entre le modèle de risque et le modèle dynamique. Cette automatisation est effectuée par un ensemble d’algorithmes de traduction, capables de convertir automatiquement le modèle FIS et le modèle de simulation en réseau de Petri PTPS.Cette approche a donné lieu à un outil de modélisation et de simulation en mode dégradé, appelé SIM-RISK. Nous avons également montré l’utilité de cet outil sur des exemples inspirés des différents risques rencontrés dans le service de stérilisation. / Sterilization services are vulnerable to risks, due to the contagious nature of their environment and to the degradation that risks can cause to their performances and to the safety of patients and staff. The risks in these facilities can range from equipment failure to the transmission of nosocomial infections and diseases. In this kind of high risk environment, these services are also required to maintain an adequate level of performance to ensure continuity of care in operating theaters.We focus in this research on the development of an integrated approach for risk analysis and performance assessment. This work is part of a collaborative work between the G-SCOP laboratory and the sterilization service of the University Hospital of Grenoble, which was the case study chosen to implement the proposed approach.The approach we propose is conducted in several steps: first, following a comparison of the risk analysis methods, we have chosen a model driven approach called FIS (Function Interaction Structure). Based on FIS, we have developed a risk model of Grenoble University Hospital sterilization service. This model describes the functions, the resources to achieve these functions as well as the various risks that may be encountered. Secondly, we introduced a new view to the FIS model dedicated to describe the dynamic behaviour of the resulting risk model.This dynamic model can simulate the behaviour of the sterilization service in normal situations of operations and risk situations.To do this, we have introduced a new Petri Net class called PTPS (Predicate-Transition, Prioritized, Synchronous) Petri Net to represent and simulate the dynamic behaviour of the FIS model. Subsequently, we automated the switching between the risk model and the dynamic model. This automation is performed by a set of translation algorithms capable of automatically converting the FIS model to a PTPS Petri Net simulation model .This approach resulted in a modelling and simulation tool in degraded mode called SIM-RISK. We also showed the usefulness of this tool by some examples based on different risks encountered in the sterilization service.

Considerando as complexidades envolvidas no processo de tomada de decisão nas organizações de hoje, é fácil ver que este processo representa um ponto importante para a obtenção de vantagens na competição pelo mercado. Portanto, observa-se que a função de gerenciamento é fundamental para a empresa, seja qual for o seu setor de atividade, tamanho, complexidade e tecnologia dos produtos ou serviços por ela oferecidos. Por este motivo, é importante que seja dada uma atenção particular ao aperfeiçoamento desta função e, para que isto seja possível, é necessário que, primeiro, seja feita uma análise detalhada do Sistema de Gerenciamento existente na empresa através da utilização de uma ferramenta que permita criar um modelo que represente as informações necessárias. De acordo com esta necessidade, este trabalho tem como objetivo propor uma técnica que auxilia na criação do modelo da Estrutura de Decisão associada ao Sistema de Gerenciamento da empresa. A técnica descrita está baseada no método de refinamentos sucessivos, e visa permitir que, a partir do modelo macro da estrutura de decisão, sejam criados modelos específicos, com um nível de formalização adequado para a implementação de sistemas de informação automatizados, que possam apoiar o processo da tomada de decisão. A preocupação principal foi propor uma técnica que forneça a facilidade de uma ferramenta gráfica, a qual permita um rápido aprendizado e proporcione ao analista um canal de comunicação com o usuário, assim como também permita a criação de um modelo com um alto grau de detalhamento. Para que isto seja possível a proposta alia o uso das Redes de Petri e do modelo TF-ORM. Ao final é apresentado um estudo de caso focando a estrutura de decisão em um ambiente de manufatura, o qual é utilizado para mostrar a aplicação prática da técnica. / Considering the complexities involved in the process of decision-taking in organizations nowadays, it is easy to realize that this process represents an important point in the acquisition of advantages concerning the competition for the market. Therefore, it is observed that the function of the management is fundamental to the enterprise, whatever its section of activity, size, complexity, technology of its products or services are. That is why it is important to give particular attention to the improvement of that function, and for that to be possible, first it is necessary to do a detailed analysis of the Management System that exists in the enterprise through the utilization of a tool which permits to create a model to represent the needed information. According to this necessity, this paper proposes a technique which helps in the creation of a model of the Decision Structure associated with the Enterprise Management System. This technique has been based on the method of successive refinement and aims at allowing to be created, from the macro model of the decision structure, specific models and with a formalization level adequate to the implement of automatic information's systems that can support the process of decision-taking. The goal was to propose a technique that provides the facility of a graphic tool and permits a fast learning, providing the analyst with a way to communicate with the user, as well as it should permit the creation of a model with a high level of details. For this to be possible, the proposal associates the use of Petri Nets and TF-ORM model together. At the end a case study focusing on the decision structure in a manufacturing environment, with is used to show the practical application of the technique is presented.

Teaching model of the Police Negotiation Process Based on Petri Nets is a study that aims to help the teaching process of strategic negotiation in critical situations involving hostages, allowing the improvement of the Military Police of the State of Alagoas in non-routine police reports. Two types of research were used in the methodology construction of this study: literature research through printed and electronic sources, as well as field research, questionnaires and interviews with military policemen working at the Center of Crisis Management, Human Rights and Community Police (CGCDHPC) in the State of Alagoas. Initially, it discussed the Learning Environment, focusing them as a support system to the learning process. Strategies of persuasion are formally defined in order to be applied in the police negotiation process. We understood the process of strategic negotiation in situations where hostages are involved. We studied different teaching models of the strategic negotiation process. At the end of the study the following results were achieved: proposal for a working model of the persuasion techniques, propose an organizational model of strategic negotiation process and formalization of the model of negotiation process where hostages are involved, based on Petri Nets. / Modelo de Ensino do Processo de Negociação Policial Baseado em Redes de Petri é um estudo que tem como meta auxiliar o ensino do processo de negociação estratégica em situações críticas envolvendo reféns, permitindo o aprimoramento de Policiais Militares do Estado de Alagoas em ocorrências policiais não rotineiras. Na construção metodológica desse estudo foram adotados dois tipos de pesquisas: a pesquisa bibliográfica, mediante fontes impressas e fontes eletrônicas, e a pesquisa de campo, questionários e entrevistas com Policiais Militares lotados no Centro de Gerenciamento de Crise, Direitos Humanos e Polícia Comunitária (CGCDHPC) do Estado de Alagoas. Inicialmente, abordam-se os Ambientes de Aprendizagem, enfocando esses como um sistema de apoio em aprendizagem. Definem-se formalmente estratégias de persuasão com a finalidade de aplicá-las no processo de negociação policial. Compreende-se o processo de negociação estratégica em situações envolvendo reféns. Estudam-se os diversos modelos de ensino do processo de negociação estratégica. Ao final da pesquisa foram alcançados os seguintes resultados: proposta de um modelo de funcionamento das técnicas de persuasão, proposta de um modelo organizacional do processo de negociação estratégica e formalização do modelo do processo de negociação, envolvendo reféns, baseado em Redes de Petri.

Les systèmes temps réel (STR) sont au coeur de machines souvent jugés critiques pour lasécurité : ils en contrôlent l’exécution afin que celles-ci se comportent de manière sûre dans le contexte d’un environnement dont l’évolution peut être imprévisible. Un STR n’a d’autre alternative que de s’adapter à son environnement : sa correction dépend des temps de réponses aux stimuli de ce dernier.Il est couramment admis que le formalisme des réseaux de Petri temporels (RdPT) est adapté àla description des STR. Cependant, la modélisation de systèmes simples, ne possédant que quelquestˆaches périodiques ordonnancées de façon basique se révèle être un exercice souvent complexe.En premier lieu, la modélisation efficace d’une gamme étendue de politiques d’ordonnancementsse heurte à l’incapacité des RdPT à imposer un ordre d’apparition à des évènements concurrentssurvenant au même instant. D’autre part, les STR ont une nette tendance à être constitués de caractéristiques récurrentes, autorisant une modélisation par composants. Or les RdPT ne sont guèreadaptés à une utilisation compositionnelle un tant soit peu générale. Afin de résoudre ces deuxproblèmes, nous proposons dans cette thèse Cifre – en partenariat entre Airbus et le Laas-Cnrs– d’étendre les RdPT à l’aide de deux nouvelles relations, les relations d’inhibition et de permission,permettant de spécifier de manière plus fine les contraintes de temps.Afin de cerner un périmètre clair d’adéquation de cette nouvelle extension à la modélisation dessystèmes temps réel, nous avons défini Pola, un langage spécifique poursuivant deux objectifs :déterminer un sous-ensemble des systèmes temps réel modélisables par les réseaux de Petri temporelsà inhibitions/permissions et fournir un langage simple à la communauté temps réel dont lavérification, idéalement automatique, est assurée par construction. Sa sémantique est donnée par traduction en réseaux de Petri temporels à inhibitions/permissions. L’explorateur d’espace d’états de laboite à outils Tina a été étendu afin de permettre la vérification des descriptions Pola / Real time systems (RTS) are at the core of safety critical devices : they control thedevices’ behavior in such a way that they remain safe with regard to an unpredictable environment. ARTS has no other choices than to adapt to its environment : its correctness depends upon its responsetime to the stimuli stemming from the environment.It is widely accepted that the Time Petri nets (TPN) formalism is adapted to the description ofRTS. However, the modeling of simple systems with only a few periodic tasks scheduled according toa basic policy remains a challenge in the worst case and can be very tedious in the most favorable one.First, we put forward some limitations of TPN regarding the modeling of a wide variety of schedulingpolicies, coming from the fact that this formalism is not always capable to impose a givenorder on events whenever they happen at the same time. Moreover, RTS are usually constituted of thesame recurring features, implying a compositional modeling, but TPN are not well adapted to sucha compositional use. To solve those problems we propose in this Cifre thesis – in partnership withAirbus and the Laas-Cnrs – to extend the formalism with two new dual relations, the forbid andallow relations so that time constraints can be finely tuned.Then, to assess this new extension for modeling of real time systems, we define Pola, a specificlanguage aimed at two goals : to determine a subset of RTS which can be modeled with forbid/allowtime Petri nets and to provide a simple language to the real time community which, ideally, can bechecked automatically. Its semantics is given by translation into forbid/allow Time Petri nets. Thestate space exploration tool of the Tina toolbox have been extended so that it can model check Poladescriptions.

Considerando as complexidades envolvidas no processo de tomada de decisão nas organizações de hoje, é fácil ver que este processo representa um ponto importante para a obtenção de vantagens na competição pelo mercado. Portanto, observa-se que a função de gerenciamento é fundamental para a empresa, seja qual for o seu setor de atividade, tamanho, complexidade e tecnologia dos produtos ou serviços por ela oferecidos. Por este motivo, é importante que seja dada uma atenção particular ao aperfeiçoamento desta função e, para que isto seja possível, é necessário que, primeiro, seja feita uma análise detalhada do Sistema de Gerenciamento existente na empresa através da utilização de uma ferramenta que permita criar um modelo que represente as informações necessárias. De acordo com esta necessidade, este trabalho tem como objetivo propor uma técnica que auxilia na criação do modelo da Estrutura de Decisão associada ao Sistema de Gerenciamento da empresa. A técnica descrita está baseada no método de refinamentos sucessivos, e visa permitir que, a partir do modelo macro da estrutura de decisão, sejam criados modelos específicos, com um nível de formalização adequado para a implementação de sistemas de informação automatizados, que possam apoiar o processo da tomada de decisão. A preocupação principal foi propor uma técnica que forneça a facilidade de uma ferramenta gráfica, a qual permita um rápido aprendizado e proporcione ao analista um canal de comunicação com o usuário, assim como também permita a criação de um modelo com um alto grau de detalhamento. Para que isto seja possível a proposta alia o uso das Redes de Petri e do modelo TF-ORM. Ao final é apresentado um estudo de caso focando a estrutura de decisão em um ambiente de manufatura, o qual é utilizado para mostrar a aplicação prática da técnica. / Considering the complexities involved in the process of decision-taking in organizations nowadays, it is easy to realize that this process represents an important point in the acquisition of advantages concerning the competition for the market. Therefore, it is observed that the function of the management is fundamental to the enterprise, whatever its section of activity, size, complexity, technology of its products or services are. That is why it is important to give particular attention to the improvement of that function, and for that to be possible, first it is necessary to do a detailed analysis of the Management System that exists in the enterprise through the utilization of a tool which permits to create a model to represent the needed information. According to this necessity, this paper proposes a technique which helps in the creation of a model of the Decision Structure associated with the Enterprise Management System. This technique has been based on the method of successive refinement and aims at allowing to be created, from the macro model of the decision structure, specific models and with a formalization level adequate to the implement of automatic information's systems that can support the process of decision-taking. The goal was to propose a technique that provides the facility of a graphic tool and permits a fast learning, providing the analyst with a way to communicate with the user, as well as it should permit the creation of a model with a high level of details. For this to be possible, the proposal associates the use of Petri Nets and TF-ORM model together. At the end a case study focusing on the decision structure in a manufacturing environment, with is used to show the practical application of the technique is presented.