Добірка наукової літератури з теми "Réseaux de Petri colorés de haut niveau"
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Зміст
Ознайомтеся зі списками актуальних статей, книг, дисертацій, тез та інших наукових джерел на тему "Réseaux de Petri colorés de haut niveau".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Дисертації з теми "Réseaux de Petri colorés de haut niveau"
Pajault, Christophe. "Model checking parallèle et réparti de réseaux de Petri colorés de haut-niveau : application à la vérification automatique de programmes Ada concurrents." Phd thesis, Université Pierre et Marie Curie - Paris VI, 2008. http://tel.archives-ouvertes.fr/tel-00812685.
Повний текст джерелаHaur, Imane. "AUTOSAR compliant multi-core RTOS formal modeling and verification." Electronic Thesis or Diss., Ecole centrale de Nantes, 2022. http://www.theses.fr/2022ECDN0057.
Повний текст джерелаFormal verification is a solution to increase the system’s implementation reliability. In our thesis work, we are interestedin using these methods to verify multi-core RTOS. We propose a model-checking approach using time Petri nets extended with colored transitions and high-level features. We use this formalism to model the Trampoline multi-core OS, compliant with the OSEK/VDX and AUTOSAR standards. We first define this formalism and show its suitability for modeling real-time concurrent systems. We then use this formalism to model the Trampoline multi-core RTOS and verify by model-checkingits conformity with the AUTOSAR standard. From this model, we can verify properties of both the OS and the application, such as the schedulability of a real-time system and the synchronization mechanisms: concurrent access to the data structures of the OS, multicore scheduling, and inter-core interrupt handling. As an illustration, this method allowed the automatic identification of two possible errors of the Trampoline OS in concurrent execution, showing insufficient data protection andfaulty synchronization
Fronc, Lukasz. "Compilation de réseaux de Petri : modèles haut niveau et symétries de processus." Thesis, Evry-Val d'Essonne, 2013. http://www.theses.fr/2013EVRY0034/document.
Повний текст джерелаThis work focuses on verification of automated systems using model-checking techniques. We focus on a compromise between potentially contradictory goals: decidability of systems to be verified, expressivity of modeling formalisms, efficiency of verification, and certification of used tools. To do so, we use high level Petri nets annotated by real programming languages. This implies the semi-decidability of most of problems because termination is left to the modeler (like termination of programs is left to the programmer). To handle these models, we choose a compilation approach which produces programs in the model annotation language, this allows to execute them efficiently. Moreover, this compilation is optimizing using model peculiarities. However, this rich expressivity leads to the use of explicit model-checking which allows to have rich model annotations but also allows to easily recover errors from verification, and remains compatible with simulation (these compiled models can be used for efficient simulation). Finally, to tackle the state space explosion problem, we use reduction by symmetries techniques which allow to reduce exploration times and state spaces
Bon, Philippe. "Du cahier des charges aux spécifications formelles : une méthode basée sur les réseaux de Pétri de haut niveau." Lille 1, 2000. https://pepite-depot.univ-lille.fr/RESTREINT/Th_Num/2000/50376-2000-149.pdf.
Повний текст джерелаMarsal, Gaëlle, and (épouse Marsal) Gaëlle Poulard. "Evaluation des performances temporelles d'architectures d'automatisation distribuées sur Ethernet par simulation d'un modèle eb réseau de Petri de haut niveau." Phd thesis, École normale supérieure de Cachan - ENS Cachan, 2006. http://tel.archives-ouvertes.fr/tel-00162228.
Повний текст джерелаBrahimi, Belynda. "Proposition d’une approche intégrée basée sur les réseaux de Petri de Haut Niveau pour simuler et évaluer les systèmes contrôlés en réseau." Thesis, Nancy 1, 2007. http://www.theses.fr/2007NAN10095/document.
Повний текст джерелаThe Networked Control Systems (NCS) used in collaborative, and distributed applications are based both on identification of application requirements named Quality of Control (QoC), and on performance evaluation of network to obtain the required Quality of Service (QoS). The pluridisciplinary aspect of NCS needs the knowledge of many domains such as information theory, robotics, sensors and networks. In general, two approaches are investigated in NCS: the first one deals with the compensation of the network perturbations by using control theory (control over network). The second one adapts the network performances according to the application needs (control of network). The objective of this thesis is to propose an integrated modelling environment to represent globally the NCS behaviour by using the High Level Petri Nets (HLPN) formalism. This work considers NCS based on switched Ethernet architectures. Such communication architecture is modelled with HLPN and is evaluated according to different scheduling mechanisms and traffic load. After that, NCS model based on HLPN is proposed. This model integrates the Ethernet switch model and applicative environment of NCS: controller, process… Finally, the strategies to control the network in order to adapt the QoS according to the QoC required by the application are proposed. These strategies are achieved using priority static and Weighted Round Robin policies. The obtained results show that the scheduling mechanisms enable to improve the performance of communication system and then to improve the application performances
Evangelista, Sami. "Méthodes et outils de vérification pour les réseaux de Petri de haut niveau : Application à la vérification de programmes Ada concurrents." Paris, CNAM, 2006. http://www.theses.fr/2006CNAM0543.
Повний текст джерелаThis thesis enters in the frame of the automatic verification of concurrent software based on an intermediary formal language, colored Petri nets. We particularly endeavor to define, or adapt, methods which aim at tackling the state explosion induced by an exhaustive exploration of the state space. We work at two levels : at a structural level, by defining some automatic automatic abstraction rules of the model, and at a semantic level, by reducing the reachabiblity graph of the system. In order to validate the practical interest of the proposed techniques we implemented them in two tools: Helena a model checker for high level Petri nets and Quasar, a platform for the verification of concurrent Ada software
Brahimi, Belynda. "Proposition d'une approche intégrée basée sur les réseaux de Petri de haut niveau pour simuler et évaluer les systèmes contrôlés en réseau." Phd thesis, Université Henri Poincaré - Nancy I, 2007. http://tel.archives-ouvertes.fr/tel-00200431.
Повний текст джерелаBiletska, Krystyna. "Estimation en temps réel des flux origines-destinations dans un carrefour à feux par fusion de données multicapteurs." Compiègne, 2010. http://www.theses.fr/2010COMP1893.
Повний текст джерелаThe quality of the information about origins and destinations (OD) of vehicles in a junction influences the performance of many road transport systems. The period of its update determines the temporal scale of working of these systems. We are interested in the problem of reconstituting of the OD of vehicles crossing a junction, at each traffic light cycle, using the traffic light states and traffic measurements from video sensors. Traffic measurements, provided every second, are the vehicle counts made on each entrance and exit of the junction and the number of vehicles stopped at each inner section of the junction. Thses real date are subject to imperfections. The only existent method, named ORIDI, which is capable of resolving this problem doesn’t take into account the data imperfection. We propose a new method modelling the date imprecision by the theory of fuzzy subsets. It can be applied to any type of junction and is independent of the type of traffic light strategy. The method estimates OD flows from the vehicle conservation law represented by an underdetermined system of equations constructed in a dynamic way at each traffic light cycle using to the fuzzy a-timed Petri nets. A unique solution is found thanks to eight different methods which introduce estimate in the form of point, interval or fuzzy set. Our study shows that the crisp methods are accurate like ORIDI, but more robust when one of the video sensors is broken down. The interval and fuzzy methods, being less accurate than ORIDI, try to guarantee that the solution includes the true value