Made available in DSpace on 2015-04-16T14:48:50Z (GMT). No. of bitstreams: 1 arquivototal.pdf: 480429 bytes, checksum: 856d2d298b1096278509b2c4243354d3 (MD5) Previous issue date: 2008-09-02 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / Brazil is currently experiencing the implementation of one of the largest governmental projects in the field of Information Technology IT, namely the project locally known by the acronym TISS Information Transfer in Complementary Health. The aforementioned project has been designed by the Federal Government through the ANS Agência Nacional de Saúde (National Health Agency), and aims to standardize and divulge information within that sector of the Government. Yet, in recent years, a number of important projects in the field of IT initiated in Brazil have been unsuccessful due to the lack of effective participation of relevant stakeholders. In that context, the present study examined the implementation of the TISS project in the João Pessoa City, state of Paraíba, through the vision of Medical Doctors - considered the main social actors in the process - due to their role as generators and disseminators of knowledge. A case-study was carried out with the participation of 18 doctors, members of João Pessoa´s supplementary health care system. Data were gathered through semi-structured interviews, and were qualitatively analyzed using the Grounded Theory. That methodological procedure permitted the extraction of the elements which served as a basis for the elaboration of a theoretical proposition. Although with limited discussion and training, interviewees readily identified the objectives of the TISS Project, as well as situation they perceived as unwanted in the implementation process. Lastly, interviewees evaluated the use of information technology, the issue of information systems security, and their level of participation in the TISS project. Through our study we hope to stimulate and assist both governmental institutions and professionals involved with the elaboration of IT projects. / Neste momento, estamos vivenciando, no Brasil, a implantação de um dos maiores projetos governamentais na área de Tecnologia da Informação - TI. Trata-se do Projeto TISS Transferência de Informações em Saúde Suplementar, elaborado pelo Governo Federal, através da Agência Nacional de Saúde Suplementar - ANS, com a finalidade de padronizar e acumular informações, nesse setor. Muitos projetos grandiosos na área de TI acabam por não terem o sucesso esperado, por não contarem com a participação efetiva, de todos os elementos que compõe o sistema. O presente trabalho teve por objetivo estudar a implantação deste projeto em João Pessoa-PB, sob a visão dos médicos, os principais atores deste processo, na medida em que são os grandes responsáveis pelo fornecimento e transmissão das informações. Para tanto, foi realizado um estudo de caso, com a participação de dezoito médicos, prestadores de serviços ao sistema de saúde suplementar, na cidade de João Pessoa-PB. Foram realizadas entrevistas semi-estruturadas, que foram analisadas, do ponto de vista qualitativo, utilizando-se a teoria fundamentada nos dados ( Grounded Theory ), para extração dos elementos que serviram de subsídio para elaboração de uma proposição teórica. Os entrevistados, apesar do pouco treinamento e discussão que tiveram, identificaram prontamente os objetivos do projeto, como também levantaram as situações indesejadas trazidas no processo de implantação da TISS. Finalmente, os entrevistados avaliaram a utilização da tecnologia da informação e a questão da segurança dos sistemas de informações e fizeram uma avaliação da adesão ao projeto. Espera-se que essas contribuições teóricas possam incentivar e subsidiar tanto as instituições governamentais quanto os profissionais que lidam com a elaboração de projetos em TI.

<p>Three issues will be elaborated and disussed in the proposed thesis. The first is<br />administration and control of data access rights in networks with XML data, with<br />emphasis on data security. The second is the administration and control of<br />access rights to data in computer networks with RDF data, with emphasis on<br />data privacy. The third is prevention of errors and memory leaks, as well as<br />communication errors, generated by programs written in Sing # language in the<br />presence of exceptions. For all three issues, there will be presented formal<br />models with corresponding type systems and showed the absence of undesired<br />behavior i.e. errors in networks or programs.</p> / <p>У тези су разматрана три проблема. Први је администрација и контрола<br />права приступа података у рачунарској мрежи са XML подацима, са<br />нагласком на безбедости посматраних података. Други је администрација и<br />котрола права приступа подацима у рачунарској мрежи са RDF подацима,<br />са нагласком на приватности посматраних података. Трећи је превенција<br />грешака и цурења меморије, као и грешака у комуникацији генерисаним<br />програмима написаних на језику Sing# у којима су присутни изузеци. За сва<br />три проблема биће предложени формални модели и одговарајући типски<br />системи помоћу којих се показује одсуство неповољних понашања тј.<br />грешака у мрежама односно програмима.</p> / <p>U tezi su razmatrana tri problema. Prvi je administracija i kontrola<br />prava pristupa podataka u računarskoj mreži sa XML podacima, sa<br />naglaskom na bezbedosti posmatranih podataka. Drugi je administracija i<br />kotrola prava pristupa podacima u računarskoj mreži sa RDF podacima,<br />sa naglaskom na privatnosti posmatranih podataka. Treći je prevencija<br />grešaka i curenja memorije, kao i grešaka u komunikaciji generisanim<br />programima napisanih na jeziku Sing# u kojima su prisutni izuzeci. Za sva<br />tri problema biće predloženi formalni modeli i odgovarajući tipski<br />sistemi pomoću kojih se pokazuje odsustvo nepovoljnih ponašanja tj.<br />grešaka u mrežama odnosno programima.</p>

<div><p>Internet of Things (IoT) systems running on Microcontrollers (MCUS) have become a prominent target of remote attacks. Although deployed in security and safety critical domains, such systems lack basic mitigations against control-flow hijacking attacks. Attacks against IoT systems already enabled malicious takeover of smartphones, vehicles, unmanned aerial vehicles, and industrial control systems.</p></div><div><p> </p><div><p>The thesis introduces a systemic analysis of previous defense mitigations to secure IoT systems. Building off this systematization, we identify two main issues in IoT systems security. First, efforts to protect IoT systems are hindered by the lack of realistic benchmarks and evaluation frameworks. Second, existing solutions to protect from control-flow hijacking on the return edge are either impractical or have limited security guarantees. This thesis addresses these issues using two approaches. </p></div><div><p> </p></div><div><p>First, we present BenchIoT, a benchmark suite of five realistic IoT applications and an evaluation framework that enables automated and extensible evaluation of 14 metrics covering security, performance, memory usage, and energy. BenchIoT enables evaluating and comparing security mechanisms. Using BenchIoT, we show that even if two security mechanisms have similarly modest runtime overhead, one can have undesired consequences on security such as a large portion of privileged user execution.</p></div><div><p> </p></div><div><p>Second, we introduce Return Address Integrity (RAI), a novel security mechanism to prevent all control-flow hijacking attacks targeting return edges, without requiring special hardware. We design and implement μRAI to enforce the RAI property. Our results show μRAI has a low runtime overhead of 0.1% on average, and therefore is a</p></div><div><p>practical solution for IoT systems. </p></div><div><p> </p></div><div><p>This thesis enables measuring the security IoT systems through standardized benchmarks and metrics. Using static analysis and runtime monitors, it prevents control-flow hijacking attacks on return edges with low runtime overhead. Combined, this thesis advances the state-of-the-art of protecting IoT systems and benchmarking its security.</p></div></div>

<div>The Internet-of-Things (IoT) is one of the fastest-growing technologies in computing, revolutionizing several application domains such as wearable computing, home automation, industrial manufacturing, <i>etc</i>. This rapid proliferation, however, has given rise to a plethora of new security and privacy concerns. For example, IoT devices frequently access sensitive and confidential information (<i>e.g.,</i> physiological signals), which has made them attractive targets for various security attacks. Moreover, with the hardware components in these systems sourced from manufacturers across the globe, instances of counterfeiting and piracy have increased steadily. Security mechanisms such as device authentication and key exchange are attractive options for alleviating these challenges.</div><div><br></div><div>In this dissertation, we address the challenge of enabling low-cost and low-overhead device authentication and key exchange in off-the-shelf embedded systems. The first part of the dissertation focuses on a hardware-intrinsic mechanism and proposes the design of two Physically Unclonable Functions (PUFs), which leverage the memory (DRAM, SRAM) in the system, thus, requiring minimal (or no) additional hardware for operation. Two lightweight authentication and error-correction techniques, which ensure robust operation under wide environmental and temporal variations, are also presented. Experimental results obtained from prototype implementations demonstrate the effectiveness of the design. The second part of the dissertation focuses on the application of these techniques in real-world systems through a new end-to-end authentication and key-exchange protocol in the context of an Implantable Medical Device (IMD) ecosystem. Prototype implementations exhibit an energy-efficient design that guards against security and privacy attacks, thereby making it suitable for resource-constrained devices such as IMDs.</div><div><br></div>

This thesis presents a body of work on the theme of millimetre-wave FMCW radar, for the purposes of security screening and remote sensing. First, the development of an optimised software radar signal processor will be outlined. Through use of threading and GPU acceleration, high data processing rates were achieved using standard PC hardware. The flexibility of this approach, compared to specialised hardware (e.g. DSP, FPGA etc…), allowed the processor to be rapidly adapted and has produced a significant performance increase in a number of advanced real-time radar systems. An efficient tracker was developed and was successfully deployed in live trials for the purpose of real-time wave detection in an autonomous boat control system. Automated radar operation and remote data telemetry functions were implemented in a terrain mapping radar to allow continuous monitoring of the Soufrière Hills volcano on the Caribbean island of Montserrat. This work concluded with the installation of the system 3 km from the volcano. Hardware modifications were made to enable coherent measurement in a number of existing radar systems, allowing phase sensitive measurements, including range-Doppler, to be performed. Sensitivity to displacements of less than 200 nm was demonstrated, which is limited by the phase noise of the system. Efficient compensation techniques are presented which correct for quadrature mixer imbalance, FMCW chirp non-linearity, and scanner drive distortions. In collaboration with the Home Office, two radar systems were evaluated for the stand-off detection of concealed objects. Automatic detection capability, based on polarimetric signatures, was developed using data gathered under controlled conditions. Algorithm performance was assessed through blind testing across a statistically significant number of subjects. A detailed analysis is presented, which evaluates the effect of clothing and object type on detection efficiency.

A criptografia de chave pública sem certificado (certificateless) é uma alternativa ao modelo convencional de criptografia assimétrica, pois a autenticação da chave pública ocorre implicitamente durante a execução dos protocolos, sem a necessidade de gerenciamento e distribuição de certificados digitais. Potencialmente reduz custos computacionais e o nível de segurança alcançado é maior quando comparado ao modelo baseado em identidade. Nesta tese de doutorado, modelos formais de segurança para acordo de chave com autenticação sem certificado são aprimorados visando dois objetivos paralelos: (1) aumentar o nível de confiança que usuários podem depositar na autoridade geradora de chaves secretas parciais e (2) viabilizar protocolos que sejam eficientes computacionalmente e com propriedades de segurança relevantes, dentre as quais se inclui resistência a ataques de adversários que têm total controle do canal de comunicação e que podem substituir chaves públicas de usuários por valores arbitrários. Para atestar que as melhorias efetuadas são praticáveis e possibilitam que os objetivos sejam alcançados, novos protocolos são propostos para o caso que envolve dois participantes na comunicação. Os protocolos são provados seguros, usando-se técnica de redução de problemas computacionais. / Certificateless public key cryptography is an alternative model to traditional asymmetric key cryptography, because the public key authentication occurs implicitly during a protocol run, with no need of digital certificates management and distribution. It has the potential to reduce computing costs, and it allows a higher security level than the one in the identity-based model. In this PhD thesis, formal security models for certificateless authenticated key agreement are improved with two independent objectives: (1) to increase the trust level for the partial secret key generating authority on which users rely, and (2) to enable computationally efficient protocols, with significant security properties, such as resistance against attacks from adversaries with full control of the communication channel, and from adversaries who are able to replace users\' public keys by any chosen value. In order to demonstrate that these improvements made are feasible and achieve the objectives, new protocols are proposed in the two-party case. These protocols are proved secure by using reduction techniques for provable security.

Preventing cyberterrorism is becoming a necessity for individuals, organizations, and governments. However, current policies focus on technical and managerial aspects without asking for experts and non-experts values and preferences for preventing cyberterrorism. This study employs value focused thinking and public value forum to bare strategic measures and alternatives for complex policy decisions for preventing cyberterrorism. The strategic measures and alternatives are per socio-technical process.

Text in English, with English, Afrikaans and Zulu summaries / This study was conducted owing to the protracted problem and challenges that unauthorised electrical connections pose to electricity utilities. This study sought to contribute to the combating of unauthorised electrical connections in KwaZulu-Natal, South Africa, which has never before been studied in this manner. Considerable revenue is stolen from utilities because of unauthorised electrical connections, by-passing of electrical meters and tampering with electricity networks. This contributes to public safety risks, fatalities, property damage and overloading of electrical networks. This in turn causes transformer and electricity network overload and power supply failure, prolonged unplanned power cuts, loss of jobs, food security risk, serious poor economic development, damaged electrical infrastructure, loss of revenue, electricity disruptions, electric shock, and the burning of dwellings. This leads to the interruption of supply to legal and compliant customers, all with disastrous effects. It is therefore difficult to manage the supply and demand of electricity under these circumstances, more especially in this period when South Africa faces a tight electricity supply. In this dissertation, the international and national perspectives reveal the nature and extent of unauthorised electrical connections. It was explored how unauthorised electrical connections are presently being combated and what specific security measures may be implemented to enhance the combating of unauthorised electrical connections. A case study design was used to investigate in greater detail the opinions, views, perceptions and experiences of the targeted interviewees using interviewing, site observation and case docket analysis. This design guided the use of specific sample groups, procedures and techniques used for data collection and analysis. The design and development of the different data collection instruments and the piloting of the instruments were implemented to ensure validity, reliability, accuracy and trustworthiness of the collected information. The study produced findings to assist electricity utilities to better manage this phenomenon. Recommendations were formulated to assist stakeholders to improve their roles in the combating of unauthorised electrical connections. / Hierdie studie is uitgevoer na aanleiding van die uitgerekte probleem en uitdagings van onwettige elektrisiteitsverbindings vir elektrisiteitsvoorsieners. Hierdie studie poog om by te dra om onwettige elektrisiteitsverbindings in KwaZulu-Natal, Suid-Afrika te beveg; dit is nog nooit tevore op hierdie wyse ondersoek nie. Beduidende inkomste word van diensmaatskappye gesteel as gevolg van onwettige elektrisiteitsverbindings, die wat elektriese meters omseil en met elektrisiteitsnetwerke peuter. Dit dra tot openbare veiligheidsrisiko's, fataliteite, skade aan eiendom, en oorlading van elektrisiteitsnetwerke by. Dit lei weer tot oorlading van transformators en elektrisiteitsnetwerke, gebrek aan kragvoorsiening, verlengde onbeplande kragonderbrekings, werksverlies, voedselsekuriteitrisiko, ernstige swak ekonomiese ontwikkeling, skade aan elektrisiteitinfrastruktuur, verlies aan inkomste, elektriese skok, en huise wat afbrand. Dit lei tot die onderbreking van voorsiening aan wetlike en inskiklike klante met rampspoedige gevolge. Dit is dus moeilik om voorsiening en vraag na elektrisiteit in hierdie omstandighede te bestuur, veral in hierdie tyd wat Suid-Afrika drukkende elektrisiteitvoorsiening beleef. In hierdie verhandeling onthul die internasionale en nasionale perspektiewe die aard en mate van onwettige elektrisiteitsverbindings. Dit was ondersoek hoe onwettige elektrisiteitsverbindings tans beveg word en watter spesifieke veiligheidsmaatreëls geïmplementeer kan word om die bevegting van onwettige elektrisiteitsverbindings te bevorder. Die gevallestudie-ontwerp is gebruik om die onderhoudgewers se menings, sienings, perspektiewe en ervarings in meer besonderhede te ondersoek deur onderhoude, waarnemings en saakdossierontledings te gebruik. Die ontwerp het die gebruik van spesifieke steekproefgroepe, prosedures en tegnieke wat vir dataversamelings en -ontleding gebruik is, gerig Die ontwerp en ontwikkeling van die verskillende dataversamelinginstrumente en die bestuur van die instrumente is geïmplementeer om geldigheid, betroubaarheid, akkuraatheid en geloofwaardigheid van die versamelde inligting te verseker. Die studie se bevindings help elektrisiteitsdienste om hierdie verskynsel beter te bestuur. Aanbevelings is geformuleer om belanghebbers te help om hul rolle te bevorder in die stryd om onwettige elektrisiteitsverbindings te beveg. / Ucwaningo lwenziwa ngenxa yokubona inkinga egxilile neqhubekela phambili kanye nezinselele ezibangelwa ukuzixhumela ama-connection kagesi (i-elektrisithi) maqondana nezinkampani zikagesi. Ucwaningo belufuna ukufaka esivivaneni kudaba lokuvimbela ukuzixhumela kogesi ngendlela engekho emthethweni eKwaZulu-Natali, eNingizimu Afrika, yona okungakaze kwenziwe ucwaningo ngayo ngale ndlela. Kunengeniso eliningi lemali entshontshwa ngale ndlela kwizinkampani noma izinhlangano zikagesi ngoba kunokuzixhomela ugesi okungekho emthethweni, ukungasetshenziswa kwamamitha ogesi, kanye nokuphazamisa ama-network kagesi. Lokhu kubangela izingozi nokungavikeleki kubantu bonke, ukulimala, ukulinyazwa nokonakala kwempahla noma iprophathi kanye nokuthi ama-network kagesi agxisheleke nokucindezeleka ngokweqile. Kanti futhi lokhu kubanga ukuthi ama-transformer kanye nama-network kagesi acindezeleke ngokweqile nokwenza ukuthi isaplayi kagesi ihluleke nokufeyila, lokhu okubangela ukuthi kube nama-power cuts noma ukucishwa kukagesi okungahleliwe, ukulahleka kwemisebenzi, ingozi yokuphazamiseka kokuvikeleka kokudla, ukuthi ukuthuthuka komnotho kuphazamiseke kakhulu, ukulahleka kwengeniso lemali, ukuphazamiseka kokuphakelwa kukagesi, ukulinyazwa kwabantu ngokubanjwa ugesi, kanye nokusha kwemizi eshiswa ugesi. Lokhu kuholela ekutheni kuphazamiseke isaplayi kagesi kumakhastama akhokha kahle nenza izinto ngokulandela umthetho, lokhu okubanga imiphumela yezinhlekelele ezimbi. Ngakho-ke kuba nzima ukubhekana kanye nezinto zesaplayi kanye nokudingeka kukagesi ngaphansi kwalezi simo, ikakhulukazi lapho iNingizimu Afrika ibhekene nokuncipha noma izinga eliphansi lesaplayi kagesi. Kule dissertation isimo sikazwelonke kanye nesamazwe omhlaba, siveze inhlobo kanye nezinga lokuxhunyelwa kukagesi okungekho emthethweni. Kubuye kwabheka nokuthi ukuxhunyelwa kukagesi okungekho emthethweni kubhekwana kanye nokuvinjelwa kanjani, nokuthi yiziphi izindlela eziqondene ezisetshenziswayo zokuvikeleka ezingasetshenziswa ukuthuthukisa izinqubo zokuvimbela ukuxhunyelwa kukagesi nama-connection angekho emthethweni angavinjelwa kanjani . Kusetshenziswe idizayini ye-case study ukuphenyisisa ngokujulile imininingwane, imibono, izinqubo zokubheka isimo kanye nezipiliyoni zalabo obekuqondiswe kubo ama-interview ngesikhathi kwenziwa ama-interview, ukuyobheka ngamehlo esimo ezindaweni, kanye nokuhlaziya amadokhethi amacala ngokwenzekayo. Le dizayini yiyona eholele ekusetshenzisweni kwamasampuli amaqembu athize, izinqubo noma amaprosija athize kanye namathekniki athize asetshenzisiwe ekuqoqeni kwe-data kanye nohlaziyo lwayo. Idizayini nokwenziwa kwama-instrumenti okuqoqwa kwe-data ehlukene, kanye nokwenza ama-instrumenti okulinga noma e-piloting, kusetshenzisiwe ukuqinisekisa i-validity, ukuthembeka (reliability), ukuqondana ncamashi kwama-instrumenti (accuracy) kanye nokuqiniseka okubizwa ngokuthi yi-trustworthiness yolwazi noma i-infomeshini eqoqiwe. Ucwaningo, lukhiphe imiphumela yokusiza izinkampani noma izinhlangano zikagesi ekuphatheni kangcono le nkinga noma ifenominoni (phenomenon) yenkinga. Kwenziwe izincomo zokusiza ababambe iqhaza (stakeholders) ukuthuthukisa indima yabo ekulwiseni ukuxhunyelwa kanye nama-connection kagesi angekho emthethweni. / Criminology and Security Science / M. Tech. (Security Management)

A criptografia de chave pública sem certificado (certificateless) é uma alternativa ao modelo convencional de criptografia assimétrica, pois a autenticação da chave pública ocorre implicitamente durante a execução dos protocolos, sem a necessidade de gerenciamento e distribuição de certificados digitais. Potencialmente reduz custos computacionais e o nível de segurança alcançado é maior quando comparado ao modelo baseado em identidade. Nesta tese de doutorado, modelos formais de segurança para acordo de chave com autenticação sem certificado são aprimorados visando dois objetivos paralelos: (1) aumentar o nível de confiança que usuários podem depositar na autoridade geradora de chaves secretas parciais e (2) viabilizar protocolos que sejam eficientes computacionalmente e com propriedades de segurança relevantes, dentre as quais se inclui resistência a ataques de adversários que têm total controle do canal de comunicação e que podem substituir chaves públicas de usuários por valores arbitrários. Para atestar que as melhorias efetuadas são praticáveis e possibilitam que os objetivos sejam alcançados, novos protocolos são propostos para o caso que envolve dois participantes na comunicação. Os protocolos são provados seguros, usando-se técnica de redução de problemas computacionais. / Certificateless public key cryptography is an alternative model to traditional asymmetric key cryptography, because the public key authentication occurs implicitly during a protocol run, with no need of digital certificates management and distribution. It has the potential to reduce computing costs, and it allows a higher security level than the one in the identity-based model. In this PhD thesis, formal security models for certificateless authenticated key agreement are improved with two independent objectives: (1) to increase the trust level for the partial secret key generating authority on which users rely, and (2) to enable computationally efficient protocols, with significant security properties, such as resistance against attacks from adversaries with full control of the communication channel, and from adversaries who are able to replace users\' public keys by any chosen value. In order to demonstrate that these improvements made are feasible and achieve the objectives, new protocols are proposed in the two-party case. These protocols are proved secure by using reduction techniques for provable security.

Ces cinquante dernières annéees, les ordinateurs ont occupé une place toujours plus importante dans notre vie quotidienne. On les retrouve aujourd’hui présents dans de nombreuses applications, sous forme de systèmes enfouis. Ces applications sont parfois critiques, dans la mesure où toute défaillance du système informatique peut avoir des conséquences catastrophiques, tant sur le plan humain que sur le plan économique. <p>Nous pensons par exemple aux systèmes informatiques qui contrôlent les appareils médicaux ou certains systèmes vitaux (comme les freins) des véhicules automobiles. <p>Afin d’assurer la correction de ces systèmes informatiques, différentes techniques de vérification Assistée par Ordinateur ont été proposées, durant les trois dernières <p>décennies principalement. Ces techniques reposent sur un principe commun: donner une description formelle tant du système que de la propriété qu’il doit respecter, et appliquer une méthode automatique pour prouver que le système respecte la propriété. <p>Parmi les principaux modèles aptes à décrire formellement des systèmes informatiques, la classe des systèmes de transition bien structurés [ACJT96, FS01] occupe une place importante, et ce, pour deux raisons essentielles. Tout d’abord, cette classe généralise plusieurs autres classes bien étudiées et utiles de modèles à espace <p>d’états infini, comme les réseaux de Petri [Pet62](et leurs extensions monotones [Cia94, FGRVB06]) ou les systèmes communiquant par canaux FIFO avec pertes [AJ93]. Ensuite, des problèmes intéressants peuvent être résolus algorithmiquement sur cette classe. Parmi ces problèmes, on trouve le probléme de couverture, auquel certaines propriétés intéressantes de sûreté peuvent être réduites. <p>Dans la première partie de cette thèse, nous nous intéressons au problème de couverture. Jusqu’à présent, le seul algorithme général (c’est-à-dire applicable à n’importe quel système bien structuré) pour résoudre ce problème était un algorithme dit en arrière [ACJT96] car il calcule itérativement tous les états potentiellement non-sûrs et vérifie si l’état initial du système en fait partie. Nous proposons Expand, Enlarge and Check, le premier algorithme en avant pour résoudre le problème de couverture, qui calcule les états potentiellement accessibles du système et vérifie si certains d’entre eux sont non-sûrs. Cette approche est plus efficace en pratique, comme le montrent nos expériences. Nous présentons également des techniques permettant d’accroître l’efficacité de notre méthode dans le cas où nous analysons des réseaux de Petri (ou <p>une de leurs extensions monotones), ou bien des systèmes communiquant par canaux FIFO avec pertes. Enfin, nous nous intéressons au calcul de l’ensemble de couverture pour les réseaux de Petri, un objet mathématique permettant notamment de résoudre le problème de couverture. Nous étudions l’algorithme de Karp & Miller [KM69], une solution classique pour calculer cet ensemble. Nous montrons qu’une optimisation de cet algorithme présenté dans [Fin91] est fausse, et nous proposons une autre solution totalement neuve, et plus efficace que la solution de Karp & Miller. <p>Dans la seconde partie de la thèse, nous nous intéressons aux pouvoirs d’expression des systèmes bien structurés, tant en terme de mots infinis que de mots finis. Le pouvoir d’expression d’une classe de systèmes est, en quelque sorte, une mesure de la diversité des comportements que les modèles de cette classe peuvent représenter. En ce qui concerne les mots infinis, nous étudions les pouvoirs d’expression des réseaux de Petri et de deux de leurs extensions (les réseaux de Petri avec arcs non-bloquants et les réseaux de Petri avec arcs de transfert). Nous montrons qu’il existe une hiérarchie stricte entre ces différents pouvoirs d’expression. Nous obtenons également des résultats partiels concernant le pouvoir d’expression des réseaux de Petri avec arcs de réinitialisation. En ce qui concerne les mots finis, nous introduisons la classe des langages bien structurés, qui sont des langages acceptés par des systèmes de transition bien structurés étiquettés, où l’ensemble des états accepteurs est clos par le haut. Nous prouvons trois lemmes de pompage concernant ces langages. Ceux-ci nous permettent de réobtenir facilement des résultats classiques de la littérature, ainsi que plusieurs nouveaux résultats. En particulier, nous prouvons, comme dans le cas des mots infinis, qu’il existe une hiérarchie stricte entre les pouvoirs d’expression des extensions des réseaux de Petri considérées. / Doctorat en sciences, Spécialisation Informatique / info:eu-repo/semantics/nonPublished