No description available.

Les applications temps réel, le plus souvent dédiées au contrôle de procédé, sont soumises à des contraintes temporelles strictes, destinées à garantir la sécurité et la cohérence du procédé contrôlé. Les applications temps réel étant des applications multi tâches, elles doivent être ordonnancées, le critère sine qua non de qualité de la stratégie d'ordonnancement étant la garantie du respect des contraintes temporelles. Ces applications sont de plus en plus souvent déployées sur des architectures multiprocesseurs. Le problème de l'ordonnancement doit donc être posé dans ce contexte, où de nombreux problèmes doivent encore être abordés. Notons tout d'abord que dans le cas multiprocesseur, il n'existe pas d'ordonnancement en ligne optimal dans le cas général, le problème de l'ordonnancement est NP-complet, et des anomalies d'ordonnancement apparaissent même lorsque l'on ne considère que des tâches indépendantes (une durée d'exécution plus courte que prévue peut provoquer une faute temporelle). Nous avons envisagé de prendre en compte la possibilité que des pannes matérielles surviennent. Nous avons étudié les mécanismes de reprise après la panne d'un processeur, dans le cas où l'application est ordonnancée par EDF, puis par un algorithme P-équitable. Ces mécanismes nécessitent de disposer d'un certain nombre de résultats généraux. Tout d'abord, nous avons étendu la définition de la P-équité à un contexte plus large que celui de la littérature, à savoir aux tâches à départs différés et à échéances contraintes, puis nous avons établi une condition suffisante d'ordonnançabilité dans ce contexte, dont nous avons étudié les performances à l'aide de simulations. Enfin, nous avons proposé un protocole efficace de gestion des flux apériodiques qui s'appuie sur une distribution P-équitable des temps creux. Cette répartition peut être obtenue soit en ordonnançant les tâches périodiques par une stratégie P-équitable quand le contexte le permet, soit via une analyse hors-ligne à base de réseaux de Petri. Nous avons proposé une technique d'extraction qui permet de forcer la répartition équitable des temps creux.

Distributed systems are shared by a large number of users that generate task-based workloads. The sharing of hardware and software by multiple workloads mandates the need for security mechanisms that protect the artifacts of individual tasks. Additionally, these systems must meet user-based performance expectations, a factor that must be addressed during the security service selection process. Current performance-based security service selection methodologies use flat GSPN models that suffer from exponential evaluation complexity as the model size increases. Due to this limitation, these methodologies cannot evaluate models representing the scale of current distributed systems. To address the evaluation complexity problem the hierarchical methodology presented in this report was designed to avoid the system size limitations of the current flat GSPN model-based methodologies. The methodology relies only on general performance models capable of modeling platform-independent systems designs. The refactoring methodology uses a divide-and-conquer approach to evaluate the entire system model. Using model-refactoring techniques the input model is modified into a hierarchy of subsystem models using abstraction to isolate performance measurement to component level. This technique further increases the effectiveness of the performance evaluation by avoiding the duplicate evaluation of identical components. Therefore increasing the number of alternate security service components results in a linear complexity growth of the entire system model. Thus, the limiting factor of the hierarchical methodology is the size of the largest component rather than the previous system size limitation. The experimental results show that the hierarchical model-based methodology is able to scale beyond system model sizes that can be evaluated using current flat GSPN-based performance evaluation methodologies. This scalability improvement implies that the hierarchical technique can evaluate models containing up to 50 individual components using the current GSPN tools. Thus the contribution of this hierarchical technique will continue to improve with subsequent advancements in GSPN model evaluation techniques.

Este trabalho de pesquisa propõe um Meta-algoritmo para o desenvolvimento de indicadores de qualidade amparados em modelos de referência e um método formal. O Meta-algoritmo proposto integra o modelo de referência de qualidade de software CMMI-DEV; o modelo GQ(I)M; e o método formal das Redes de Petri (RP) com o modelo de processo de desenvolvimento de software de uma empresa, no contexto de gestão de processos de software. O Meta-algoritmo proposto foi desenvolvido com o propósito de melhorar a qualidade e a eficiência da execução de projetos de desenvolvimento de sistemas de software, por meio de atividades de monitoramento e controle, mantendo a rastreabilidade dos elementos produzidos durante o seu ciclo de desenvolvimento. Baseando-se nestes modelos, concebeu-se o SI-CMMI. Um protótipo de sistema de informação, denominado CMMIAudit, foi concebido para implementar as características previstas e necessárias para a operacionalização do SI-CMMI no processo de monitoramento, controle e garantia da qualidade de software, além de viabilizar a implementação do processo de inspeção parametrizado pelos modelos. Um método heurístico para modelagem de Redes de Petri foi também desenvolvido para diminuir subjetividades durante o processo de modelagem da RP.

Finding integer solutions to linear equations has various real world applications. In the thesis, we investigate its application to the reachability analysis of Petri nets. Introduced by Petri in 1962, Petri net has been a powerful mathematical formalism for modeling, analyzing and designing discrete event systems. In the research community of Petri nets, finding a feasible path from the initial state to the target state in Petri net, known as reachability analysis, is probably one of the most important and challenging subjects. The reachability algebraic analysis is equivalent to finding the nonnegative integer solutions to a fundamental equation constructed from the Petri net. We apply our algorithm in this thesis to reachability analysis of Petri net by finding the nonnegative integer solutions to the fundamental equation. / Finding the optimal binary solution to a quadratic object function is known as the Binary Quadratic Programming problem (BQP), which has been studied extensively in the last three decades. In this thesis, by investigating geometric features of the ellipse contour of a concave quadratic function, we derive new upper and lower bounding methods for BQP. Integrating these new bounding schemes into a proposed solution algorithm of a branch-and-bound type, we propose an exact solution method in solving general BQP with promising preliminary computational results. Meanwhile, by investigating some special structures of the second order matrix and linear term in BQP, several polynomial time algorithms are discussed to solve some special cases of BQP. / In the realm of integer programming, finding integer solutions to linear equations is another important research direction. The problem is proved to be NP-Complete, and several algorithms have been proposed such as the algorithm based on linear Diophantine equations as well as the method based on Groebner bases. Unlike the traditional algorithms, the new efficient method we propose in this thesis is based on our results on zero duality gap and the cell enumeration of an arrangement of hyperplanes in discrete geometry. / Integer programming plays an important role in operations research and has a wide range of applications in various fields. There are a lot of research directions in the area of integer programming. In this thesis, two main topics will be investigated in details. One is to find the optimal binary solution to a quadratic object function, and the other is to find integer solutions to linear equations. / Gu, Shenshen. / Adviser: Wang Jun. / Source: Dissertation Abstracts International, Volume: 73-01, Section: B, page: . / Thesis (Ph.D.)--Chinese University of Hong Kong, 2009. / Includes bibliographical references (leaves 98-103). / Electronic reproduction. Hong Kong : Chinese University of Hong Kong, [2012] System requirements: Adobe Acrobat Reader. Available via World Wide Web. / Electronic reproduction. [Ann Arbor, MI] : ProQuest Information and Learning, [201-] System requirements: Adobe Acrobat Reader. Available via World Wide Web. / Abstract also in Chinese.

Cette thèse s'intéresse à la vérification de systèmes automatisables par model-checking. La question sous-jacente autour de laquelle se construit la contribution est la recherche d'un compromis entre différents objectifs potentiellement contradictoires : la décidabilité des systèmes à vérifier, l'expressivité des formalismes de modélisation, l'efficacité de la vérification, et la certification des outils utilisés. Dans ce but, on choisit de baser la modélisation sur des réseaux de Petri annotés par des langages de programmation réels. Cela implique la semi-décidabilité de la plupart des questions puisque la responsabilité de la terminaison est remise entre les mains du modélisateur (tout comme la terminaison des programmes est de la responsabilité du programmeur). Afin d'exploiter efficacement ces annotations, on choisit ensuite une approche de compilation de modèle qui permet de générer des programmes efficaces dans le langage des annotations, qui sont alors exécutées de la manière la plus efficace. De plus, la compilation est optimisée en tirant partie des spécificités de chaque modèle et nous utilisons l'approche de model-checking explicite qui autorise cette richesse d'annotations tout en facilitant le diagnostique et en restant compatible avec la simulation (les modèles compilés peuvent servir à de la simulation efficace). Enfin, pour combattre l'explosion combinatoire, nous utilisons des techniques de réductions de symétries qui permettent de réduire les temps d'exploration et l'espace mémoire nécessaire. / 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.

Tese de mestr.. Engenharia Mecânica. Faculdade de Engenharia. Universidade do Porto. 1998

Le trafic routier entraine de nombreux effets néfastes, dont la pollution, l'insécurité et la congestion. La plupart de méthodes développées, pour la régulation du trafic urbain au niveau des carrefours, cherche à réduire les temps d’attente et les longueurs des files d'attente. Ces méthodes se fixent principalement comme objectif l’optimisation des cycles de feu sur un horizon fini.Pour la description du trafic, nous adoptons une modélisation par les réseaux de Pétri Hybrides (RdPH), qui représente, simultanément, deux niveaux de représentation complémentaires : l'évolution continue des files d'attente et l'évolution discrète des feux tricolores. Ces deux niveaux sont, respectivement, articulés autour des réseaux de Pétri à vitesses variables et des réseaux de Pétri discrets temporisés.Nous élaborons en plus, une nouvelle stratégie pour résoudre le problème de la régulation du trafic urbain intervenant d'une manière adaptée au niveau des feux de signalisation. Nous cherchons à éviter, en premier lieu,la congestion et la sursaturation des files d'attente, qui ne doivent pas dépasser l'optimum des capacités des voies de l'intersection et, en second lieu, à réduire le temps d'évacuation des véhicules au niveau du carrefour et surtout les temps d'attente des conducteurs.Dans ce sens, un premier algorithme est élaboré pour calculer les longueurs des files d'attente, utilisant une approche qui se base sur la simplification de la modélisation d'un carrefour. Pour optimiser le temps moyen d’attente et le temps total d'évacuation sont, considérés et appliqués, avec succès, une heuristique de contrôle et une stratégie de régulation à feux fixe et à feux variables, suite à la détermination de la durée de feu vert correspondante à la situation de l'intersection en temps réel.Nous envisageons, de généraliser les résultats de nos travaux exploitant le modèle RdPH aux intersections plus complexes pour des situations réelles d'un réseau de carrefour. / Road traffic causes many adverse effects, including pollution, insecurity and congestion. Most of the developedmethods for regulation of urban traffic at crossroads, seeking to reduce wait times and lengths of queues. Thesemethods are mainly set objective optimization fire cycles over a finite horizon.To describe the composition of traffic, we opted for a traffic modeling by hybrid Petri nets, representingsimultaneously two complementary levels of representation: the continuing evolution of queues and discreetchanging traffic lights. These two levels are respectively articulated about Petri nets variable speed and discretetimed Petri nets.We chose, as well, for a new strategy to solve the problem of urban traffic control intervening in an appropriatemanner to the level of the signal lights. We sought to avoid first, congestion and the super saturation of queues,which must not exceed the optimum capacity of the intersection of routes studied and, second, to reduce theevacuation time of vehicles at the crossroads and especially waiting times for drivers.In this sense, a first algorithm is developed to calculate the lengths of queues, using a modeling simplificationapproach to a junction. To optimize the average waiting time and the total evacuation time are considered andapplied successfully by a heuristic control lights and a fixed control strategy and floating lights, following thedetermination of the duration of corresponding green light to the situation in real time intersectionWe plan to generalize the results of our work exploiting RDPH model to complex intersections for real situations of acrossroads network.

Thesis (M.S.)--University of Missouri--Rolla, 2007. / Vita. The entire thesis text is included in file. Title from title screen of thesis/dissertation PDF file (viewed November 30, 2007) Includes bibliographical references (p. 199-209).

La construction d'une application répartie fait en général intervenir une couche logicielle particulière, appelée intergiciel, qui prend en charge la transmission des données entre les différents noeuds de l'application. La conception d'applications pour les systèmes embarqués temps-réel implique la prise en compte de certaines contraintes spécifiques à ce domaine, que ce soit en terme fiabilité ou de dimensions à la fois temporelles et spatiales. Ces contraintes doivent notamment être respectées par l'intergiciel. L'objet de ces travaux est la description des applications temps-réel réparties embarquées en vue de configurer automatiquement l'intergiciel adéquat. L'étude se focalise sur la définition d'un processus de conception permettant d'intégrer les phases de description, de vérification et de génération de l'application complète. Pour cela, nous nous reposons sur le langage de description d'architecture AADL. Nous l'exploitons comme passerelle entre la phase de description de l'architecture applicative, les formalismes de vérification, la génération du code exécutable et la configuration de l'exécutif réparti. Nous montrons comment spécifier un exécutif pour AADL afin de produire automatiquement le code applicatif et l'intergiciel pour une application répartie. Nous montrons également comment exploiter ces spécifications pour produire un réseau de Petri afin d'étudier l'intégrité des flux d'exécution dans l'architecture. Afin de valider notre processus de conception, nous avons conçu et développé Ocarina, un compilateur pour AADL qui utilise l'intergiciel schizophrène PolyORB comme exécutif.