A Modelagem Orientada a Objetos (MOO) é o processo de construção de modelos de sistemas através da identificação e definição de um conjunto de objetos relacionados, que comportam-se e colaboram entre si conforme os requisitos estabelecidos para o sistema. Esta definição inclui os três aspectos ortogonais, ou dimensões, deste tipo de modelagem: a dimensão estrutural dos objetos, a dimensão dinâmica do comportamento e a dimensão funcional dos requisitos. Conforme a importância relativa dada a cada uma destas dimensões, podem ser definidas três estratégias possíveis para conduzir a MOO. Estas estratégias são as dirigidas por dados, por comportamento e por processos. A estratégia dirigida por processos já esta superada. Atualmente, a estratégia dirigida por dados domina na maioria das técnicas de MOO. A estratégia dirigida por comportamento propõe que a estrutura dos objetos em um sistema pode ser determinada a partir do comportamento externo e interno que o sistema deve apresentar. Esta idéia é interessante, porque permite introduzir tardiamente o encapsulamento na MOO. Conforme é argumentado neste trabalho, as vantagens atribuídas a orientação a objetos são de implementação, isto é, a decisão de orientar ou não a objetos é, na realidade, uma decisão de design. Ao introduzir o encapsulamento na modelagem inicial do sistema, ganha-se o benefício da continuidade estrutural ao custo de colocar a MOO mais perto do design. Neste contexto, este trabalho apresenta um processo de modelagem conceitual de sistemas do ponto de vista comportamental que introduz tardiamente o encapsulamento da orientação a objetos como primeiro passo de design. Em outras palavras, é proposta uma técnica de modelagem sob uma estratégia dirigida por comportamento (privilegiando, assim, o aspecto dinâmico dos sistemas) com o suficiente poder de expressão para, ao mesmo tempo, permitir a modelagem de sistemas de informação no nível conceitual e derivar dos modelos dinâmicos obtidos uma representação estrutural orientada a objetos. 0 sistema, na concepção desta proposta, é composto por um conjunto de processos concorrentes, cada um dos quais recebe um estimulo do ambiente, realiza um tratamento especifico sobre ele e gera para o ambiente uma resposta. Os estímulos externos são decompostos em conjuntos de eventos concorrentes tratados no interior do processo. As ações realizadas no interior do mesmo são compostas nas respostas geradas para o exterior. Os processos são modelados comportamentalmente, utilizando o formalismo proposto High-Level Statecharts (HLS). HLS é uma extensão dos statecharts de Harel. As principais extensões propostas são a introdução de estados "parametrizados" usando variáveis e a representação genérica de conjuntos de estados concorrentes e exclusivos. 0 modelo de processos e desintegrado em unidades de comportamento que tratam das mesmas variáveis. Estas unidades são integradas em um modelo de ciclos de vida para estas variáveis. Finalmente, apos a aplicação da técnica de modelagem conceitual, e obtido um modelo estrutural orientado a objetos. Este modelo e derivado utilizando unicamente informações contidas nos modelos dinâmicos gerados no processo da técnica proposta. No modelo estrutural são identificadas classes, objetos, atributos, associações estáticas, hierarquias de herança e operações. Todo o processo e exemplificado utilizando o problema padrão de preparação de congressos da IFIP. / Object-Oriented Modeling (OOM) is the process of construction of systems models, through an identification and definition of a set of relating objects. These objects have a collaborative behavior according to the system requirements previously defined. This definition includes three modeling aspects or dimensions: object structural dimension, behavior dynamic dimension and requirements functional dimension. Depending on a relative importance of each dimension, three possible strategies to drive OOM are defined. The strategies are: data-driven, behavior-driven and process-driven. Process-driven strategy is obsolete. Nowadays, data-driven is the dominant strategy in the world of OOM techniques. Behavior-driven strategy suggests both internal and external system behaviors define its object structure. This idea is attractive because it allows a late encapsulation in the OOM. As explained in this work, the main advantage to use object-orientation is for implementation. So, to object-orient or not to object-orient is a design decision. If encapsulation is introduced in the very beginning of systems modeling, the structural continuity is achieved at the cost of pulling OOM closer to design. In this context, the work presents a process of systems conceptual modeling using a behavioral point of view. This process introduces object-oriented encapsulation lately as a first step in the design phase. In other words, this work is a proposal of a modeling technique under a behavior-driven strategy (focusing the dynamic aspect of the systems) with enough expression power to model information systems at conceptual level and, at the same time, to derive of an object-oriented structural representation from the dynamic models. As conceived in the proposal, a system is composed by a set of concurrent processes. Each process receives a stimuli from the environment, makes a specific treatment on it and generates a response to the environment. The external stimuli is decomposed into a set of concurrent events which are internally handled by the process. Actions internally performed by the process are composed into a response which is sent outside the process. Processes are behaviorally modeled using a proposed formalism called High-Level Statecharts (HLS). HLS is a extension of Harel's statecharts. The main extensions proposed are parameterized states using variables and generic representation of concurrent and exclusive sets of states. Process model is disintegrated into behavior units handling the same variables. The units are integrated into a life cycle model for these variables. Finally, after the modeling technique has been applied, an object-oriented structural model is obtained. This model is derived exclusively using information from the dynamic models constructed during the modeling process. Classes, objects, attributes, static associations, inheritance hierarchies and operations in the structural model are identified. Examples used in all the modeling process are taken from the standard problem of IFIP conference.

Avec l'avènement des systèmes intégrés complexes, la vérification par assertions(Assertion Based Verification ou ABV) s'est imposée comme une solution pour la vérification semi-formelle des circuits. L'ABV permet de valider qu'un circuit satisfait ou non une propriété(ou assertion). Des travaux antérieurs ont montré qu'il était possible de synthétiser ces propriétés sous la forme de moniteurs matériels. Ces derniers peuvent ainsi être embarqués à demeure sur un circuit afin qu'ils assurent une tâche de monitoring. Avec un objectif de surveillance et de sûreté, l'utilisation de tels moniteurs est un plus. Néanmoins, ces derniers sont aussi sensibles que les circuits surveillés à une dégradation environnementale(tension, température, vieillissement, …). Afin de réduire le risque de dysfonctionnement des moniteurs, initialement conçus comme des circuits synchrones, une variante asynchrone(quasi-insensible aux délais) est proposée dans cette thèse. Ces travaux s'inscrivent dans le cadre du projet ANR SFINCS(Thalès, Dolphin Integration, TIMA) et ont mené à la définition d'une méthode de synthèse de moniteurs asynchrones matériels tirant parti de la robustesse et de la modularité des implémentations asynchrones. Les études menées se focalisent en premier lieu sur la conception d'une bibliothèque de moniteurs élémentaires asynchrones et sur une méthode d'interconnexion ad hoc permettant de constituer des moniteurs complexes. Afin de garantir les bonnes propriétés de robustesse de ces moniteurs, une étude a été menée à l'aide de l'outil de vérification formelle RAT. Il a notamment été prouvé que la connexion d'un moniteur asynchrone avec un circuit synchrone(à surveiller) était un point particulièrement délicat car les hypothèses du circuit synchrone contraignent le moniteur asynchrone. Il a donc été proposé d'introduire un dispositif de contrôle de l'horloge du circuit synchrone, appelé « clock stretching », afin de relaxer les hypothèses temporelles synchrones qui sont appliquées à la partie asynchrone. / With the advent of complex integrated systems, the assertion based verification(ABV) has emerged as a solution for the semi-formal circuits verification. The ABV is used to validate that a circuit satisfies a property(or assertion). Previous work has shown that it is possible to synthesize these properties in the form of hardware monitors. These can then be embeddded permanantly on a circuit so that they provide monitoring task. With a goal of security and surveillance, the use of such monitors is a plus. Nevertheless, they are as sensitive as the monitored circuits to environmental degradation(voltage, temperature, age, ...). To reduce the risk of failure in monitors, originally designed as synchronous circuits, an asynchronous variant(quasi-delay insensitive) is proposed in this thesis. This work is part of the ANR project SFINCS(Thales, Dolphin Integration, TIMA) and led to the definition of a method for synthesizing asynchronous hardware monitors leveraging the robustness and modularity of asynchronous implementations. The studies focus primarily on the design of a library of basic asynchronous monitors and an ad hoc method of interconnection to build complex monitors. To ensure the robustness of these monitors, a study was conducted using formal verification tool RAT. In particular it was proved that the connection of an asynchronous monitor with a synchronous circuit(to watch) was particularly tricky because the timing assumptions of synchronous circuit impact the asynchronous monitor. It was therefore proposed to introduce a devicet, called "clock stretching", for controlling the clock of the synchronous circuit and relax synchronous timing assumptions that are applied to the asynchronous monitor.

Made available in DSpace on 2016-06-02T19:06:00Z (GMT). No. of bitstreams: 1 4702.pdf: 26018415 bytes, checksum: 9c97e5ddef6d5a00a930406e3383b476 (MD5) Previous issue date: 2012-09-19 / Financiadora de Estudos e Projetos / In the scenario of computational interfaces development, researches efforts aim to offer new ways of interaction that are closer to the natural way which humans interact with the real world. Amongst the diversity of interface modalities, the tabletop tangible interfaces make the link between physical objects and virtual objects, making possible to "grasp" the interface and interact with it physically, also counting on multitouch interactions. However, in the development process of this kind of interface, there is a lack of specification s model that supports, not only the physical objects interaction, but multitouch interactions as well, and that organizes and classifies the specification in a more agile manner, easier to document and implement. Thus, this work presents a new tabletop tangible user interface specification model, TTUI-SM, that classifies and organizes the interface element specification within many components. A diagramatic tool, TTUI-SMT, was developed based on this model, aiming to make the interface specification and development faster, easier and automatized. To validate the model and tool, two studycases were introduced and specified. An experiment was conducted to evaluate both model and tool, resulting in the comprovation, through questionnaires analysis, of the proposed benefits. / No cenário de desenvolvimento de interfaces computacionais, os avanços nas pesquisas buscam oferecer novas formas de interação que se aproximam da forma natural com que o homem interage com o mundo real. Dentre as diversas interfaces avançadas, as interfaces tangíveis de mesa (tabletop), promovem a ligação entre objetos físicos e objetos virtuais, possibilitando ao usuário interagir com objetos digitais por meio do ambiente físico, e também por meio de interações multitoques. Entretanto, o processo de desenvolvimento deste tipo de interface carece de um modelo de especificação que contemple, além das interações por meio de objetos, interações multitoques e que organize e classifique a especificação de uma maneira mais ágil e mais fácil de documentar e implementar. Assim, este trabalho apresenta um novo modelo de especificação de elementos de interface tangível de mesa, denominado TTUI-SM, que organiza a especificação de elementos de interface em diversos componentes. Uma ferramenta diagramática, o TTUI-SMT, baseada neste modelo de especificação, também foi desenvolvida visando agilizar, facilitar e automatizar o processo de especificação da interface e do seu desenvolvimento. Para validar o modelo e a ferramenta, dois estudos de caso foram introduzidos e especificados. Um experimento foi conduzido para avaliar o modelo e a ferramenta e, por meio de questionários, os benefícios propostos foram validados.

A Modelagem Orientada a Objetos (MOO) é o processo de construção de modelos de sistemas através da identificação e definição de um conjunto de objetos relacionados, que comportam-se e colaboram entre si conforme os requisitos estabelecidos para o sistema. Esta definição inclui os três aspectos ortogonais, ou dimensões, deste tipo de modelagem: a dimensão estrutural dos objetos, a dimensão dinâmica do comportamento e a dimensão funcional dos requisitos. Conforme a importância relativa dada a cada uma destas dimensões, podem ser definidas três estratégias possíveis para conduzir a MOO. Estas estratégias são as dirigidas por dados, por comportamento e por processos. A estratégia dirigida por processos já esta superada. Atualmente, a estratégia dirigida por dados domina na maioria das técnicas de MOO. A estratégia dirigida por comportamento propõe que a estrutura dos objetos em um sistema pode ser determinada a partir do comportamento externo e interno que o sistema deve apresentar. Esta idéia é interessante, porque permite introduzir tardiamente o encapsulamento na MOO. Conforme é argumentado neste trabalho, as vantagens atribuídas a orientação a objetos são de implementação, isto é, a decisão de orientar ou não a objetos é, na realidade, uma decisão de design. Ao introduzir o encapsulamento na modelagem inicial do sistema, ganha-se o benefício da continuidade estrutural ao custo de colocar a MOO mais perto do design. Neste contexto, este trabalho apresenta um processo de modelagem conceitual de sistemas do ponto de vista comportamental que introduz tardiamente o encapsulamento da orientação a objetos como primeiro passo de design. Em outras palavras, é proposta uma técnica de modelagem sob uma estratégia dirigida por comportamento (privilegiando, assim, o aspecto dinâmico dos sistemas) com o suficiente poder de expressão para, ao mesmo tempo, permitir a modelagem de sistemas de informação no nível conceitual e derivar dos modelos dinâmicos obtidos uma representação estrutural orientada a objetos. 0 sistema, na concepção desta proposta, é composto por um conjunto de processos concorrentes, cada um dos quais recebe um estimulo do ambiente, realiza um tratamento especifico sobre ele e gera para o ambiente uma resposta. Os estímulos externos são decompostos em conjuntos de eventos concorrentes tratados no interior do processo. As ações realizadas no interior do mesmo são compostas nas respostas geradas para o exterior. Os processos são modelados comportamentalmente, utilizando o formalismo proposto High-Level Statecharts (HLS). HLS é uma extensão dos statecharts de Harel. As principais extensões propostas são a introdução de estados "parametrizados" usando variáveis e a representação genérica de conjuntos de estados concorrentes e exclusivos. 0 modelo de processos e desintegrado em unidades de comportamento que tratam das mesmas variáveis. Estas unidades são integradas em um modelo de ciclos de vida para estas variáveis. Finalmente, apos a aplicação da técnica de modelagem conceitual, e obtido um modelo estrutural orientado a objetos. Este modelo e derivado utilizando unicamente informações contidas nos modelos dinâmicos gerados no processo da técnica proposta. No modelo estrutural são identificadas classes, objetos, atributos, associações estáticas, hierarquias de herança e operações. Todo o processo e exemplificado utilizando o problema padrão de preparação de congressos da IFIP. / Object-Oriented Modeling (OOM) is the process of construction of systems models, through an identification and definition of a set of relating objects. These objects have a collaborative behavior according to the system requirements previously defined. This definition includes three modeling aspects or dimensions: object structural dimension, behavior dynamic dimension and requirements functional dimension. Depending on a relative importance of each dimension, three possible strategies to drive OOM are defined. The strategies are: data-driven, behavior-driven and process-driven. Process-driven strategy is obsolete. Nowadays, data-driven is the dominant strategy in the world of OOM techniques. Behavior-driven strategy suggests both internal and external system behaviors define its object structure. This idea is attractive because it allows a late encapsulation in the OOM. As explained in this work, the main advantage to use object-orientation is for implementation. So, to object-orient or not to object-orient is a design decision. If encapsulation is introduced in the very beginning of systems modeling, the structural continuity is achieved at the cost of pulling OOM closer to design. In this context, the work presents a process of systems conceptual modeling using a behavioral point of view. This process introduces object-oriented encapsulation lately as a first step in the design phase. In other words, this work is a proposal of a modeling technique under a behavior-driven strategy (focusing the dynamic aspect of the systems) with enough expression power to model information systems at conceptual level and, at the same time, to derive of an object-oriented structural representation from the dynamic models. As conceived in the proposal, a system is composed by a set of concurrent processes. Each process receives a stimuli from the environment, makes a specific treatment on it and generates a response to the environment. The external stimuli is decomposed into a set of concurrent events which are internally handled by the process. Actions internally performed by the process are composed into a response which is sent outside the process. Processes are behaviorally modeled using a proposed formalism called High-Level Statecharts (HLS). HLS is a extension of Harel's statecharts. The main extensions proposed are parameterized states using variables and generic representation of concurrent and exclusive sets of states. Process model is disintegrated into behavior units handling the same variables. The units are integrated into a life cycle model for these variables. Finally, after the modeling technique has been applied, an object-oriented structural model is obtained. This model is derived exclusively using information from the dynamic models constructed during the modeling process. Classes, objects, attributes, static associations, inheritance hierarchies and operations in the structural model are identified. Examples used in all the modeling process are taken from the standard problem of IFIP conference.

The storage vendors have their own standards for the management of their storage resources but it creates interoperability issues on different storage products. With the recent advent of the new protocol named Storage Management Initiative-Specification (SMI-S), the Storage Networking Industry Association (SNIA) has taken a major step in order to make the storage management more effective and organized. SMI-S has replaced its predecessor Storage Network Management Protocol (SNMP) and it has been categorized as an ISO standard. The main objective of the SMI-S is to provide interoperability management of the heterogeneous storage vendor systems by unifying the Storage Area Network (SAN) management, hence making the dreams of the network managers come true. SMI-S is a guide to build systems using modules that ‘plug’ together. SMI-S compliant storage modules that use CIM ‘language’ and adhere to CIM schema interoperate in a system regardless of which vendor built them. SMI-S is object-oriented, any physical or abstract storage-related elements can be defined as a CIM object. SMI-S can unify the SAN management systems and it works well with the heterogeneous storage environment. SMI-S has offered a cross-platform, cross-vendor storage resource management. This thesis work discusses the use of SMI-S at Compuverde which is a storage solution provider, located in the heart of the Karlskrona, the southeastern part of Sweden. Compuverde was founded by Stefan Bernbo in Karlskrona,Sweden. Just like all others leading storage providers, Compuverde has also decided to deploy the Storage Management Initiative-Specification (SMI-S) to manage their Storage Area Network (SAN) and to achieve interoperability. This work was done to help Compuverde to deploy the SMI-S protocol for the management of the Storage Area Network (SAN) which, among many of its features, would create alerts/traps in case of a disk failure in the SAN. In this way, they would be able to keep the data of their clients, safe and secure and keep their reputation for being reliable in the storage industry. Since Compuverde regularly use Microsoft Windows and Microsoft have started to support SMI-S for storage provisioning in System Center 2012 Virtual Machine Manager (SCVMM), this work was done using the SCVMM 2012 and the Windows Server 2012.The SMI-S provider which was used for this work was QNAP TS- 469 Pro. / 0764354242

Cognitive radios require spectral occupancy information in a given location, to avoid any interference with the existing licensed users. This is achieved by spectrum sensing. Existing narrowband, serial spectrum sensors are spectrally inefficient and power hungry. Wideband spectrum sensing increases the number of probable fre-quency candidates for cognitive radio. Wideband RF systems cannot use analog to digital converters (ADCs) for spectrum sensing without increasing the sampling rate and power consumption. The use of ADCs is limited because of the dynamic range of the signals that need to be sampled and the frequency of operation. In this work, we have presented a CMOS based area efficient, dedicated and scalable wideband parallel/serial spectrum sensor for cognitive radio. The key contributions of the thesis are: 1. An injection locked oscillator cascade (ILOC) for parallel LO synthesis. An area-efficient, wideband RF frequency synthesizer, which simultaneously gen-erates multiple local oscillator (LO) signals, is designed. It is suitable for parallel wideband RF spectrum sensing in cognitive radios. The frequency synthesizer consists of an injection locked oscillator cascade where all the LO signals are derived from a single reference oscillator. The ILOC is implemented in a 130-nm technology with an active area of 0.017 mm2. It generates 4 uni-formly spaced LO carrier frequencies from 500 MHz to 2 GHz. 2. A wideband, parallel RF spectrum sensor for cognitive radios has been de-signed. This spectrum sensor is designed to detect RF occupancy from 250 MHz to 5.25 GHz by using an array of CMOS receivers with envelope detec-tors. A parallel LO synthesizer is implemented as an ILOC. The simulated sensitivity is around -25 dBm for 250 MHz wide bandwidth. 3. A mitigation technique for harmonic downconversion in wideband spectrum sensors. The downconversion of radio frequency (RF) components around the harmonics of the local oscillator (LO), and its impact on the accuracy of white space detection using integrated spectrum sensors, is (are) studied. We propose an algorithm to mitigate the impact of harmonic Down conversion by utilizing multiple parallel downconverters in the system architecture. The proposed algorithm is validated on a test-board using commercially avail-able integrated circuits (IC) and a test-chip implemented in a 130-nm CMOS technology. The measured data shows that the impact of the harmonic down-conversion is closely related to the LO characteristics, and that much of it can be mitigated by the proposed technique. 4. A wideband spectrum sensor for narrowband energy detection. A wideband spectrum sensing system for cognitive radio is designed and implemented in a 130-nm RF mixed-mode CMOS technology. The system employs an I-Q downconverter, a pair of complex filters and a pair of envelope detectors for energy detection. The spectrum sensor works from 250 MHz to 3.25 GHz. The design makes use of the band pass nature of the complex filter to achieve two objectives : i) Separation of upper sideband (USB) and lower sideband (LSB) around the local oscillator (LO) signal and ii) Resolution of smaller bands within a large detection bandwidth. The measured sensitivity is close to -45 dBm for a single tone test over a bandwidth of 40 MHz. The measured Image reject ratio (IRR) is close to 30 dB. The overall sensing bandwidth is 3.5 GHz and the overall wideband detection bandwidth is 250 MHz which is partitioned into 40 MHz narrowband chunks with 8 such overlapping chunks.

In angiosperms, specialized reproductive structures are borne in flowers to ensure their reproductive success. After the vegetative growth, plants undergo reproductive phase change to produce flowers. Floral meristems (FMs) are generated on the flanks of inflorescence and groups of specialized stem cells in the FM differentiate into four whorls of organs of a flower. In dicots, floral meristem successively gives rise to sepals, petals, stamens and carpels; after which it terminates. The fate of organs formed on FM is under the control of genetic regulators, key among which are members of MADS box transcription factor family. Their individual and combined act confers distinct identities to floral organs. Grass flowers are highly modified in structure. Rice flower, a model for grasses, is borne on a short branch called spikelet and they together from the basic structural units of the rice infloresences known as panicle. The outer whorl organs of a grass floret are bract-like structures known as lemma and palea to dicot sepals is highly dibated (see Chapter 1). In grass florets, petal homologs are a pair of highly reduced, fleshy bracts known as lodicules, while stamen and carpel homologs occupy the same position and share the same functions as their dicot counterparts. Aside from these distinct outer whorl organs, the florets are subtended by two pairs of bracts known as empty glumes and rudimentary glumes. The genetic regulators that control their unique identities and those that perform conserved functions are very intriguing and central questions in plant developmental biology. Using various contemporary and complementary technologies, we have analysed the molecular functions and downstream pathways of a MADS box transcription factor, OsMADSI during the rice floret meristem specification and organ development. Further by reverse genetics and overexpression studies, we have also functionally characterized two target genes of OsMADSI, OsETTINI and OsETTINI2 to understand their roles downstream to OsMADSI during the rice floret development.

La vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n'étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG (Vulnerability Test Generation, génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d'intrusions est généré. Cette méthode s'inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d'application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L'extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d'une instruction. Cette méthode nous a permis de tester différents mécanismes d'implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d'étude, la méthode proposée est générique et a été appliquée à d'autres cas d'études. / Verification of the resistance of attacks against embedded implementations of the Java Card bytecode verifiers is a complex task. Current methods are not sufficient, only the generation of manual testing is possible. To automate this process, we propose a method called VTG (Vulnerability Test Generation). Based on a formal representation of the functional behavior of the system under test, a set of intrusion test is generated. This method is based on techniques of mutation and model-based testing. Initially, the model is transferred according to rules that we have defined to represent potential attacks. The tests are then extracted from the mutant models. Two Event-B models have been proposed. The first represents the structural constraints of the Java Card application files. The VTG allows in seconds to generate hundreds of abstract tests. The second model is composed of 66 events to represent 61 Java Card instructions. The mutation is effected in a few seconds. Extraction tests to generate 223 test 45 min. Each test checks a precondition or a combination of preconditions of a statement. This method allowed us to test different implementations of mechanisms through Java Card bytecode verifier. Although developed for our case study, the proposed method is generic and has been applied to other case studies.

Les travaux développés dans cette thèse visent à assister le processus d’ingénierie des exigences temporelles pour les systèmes complexes à contraintes de temps. Nos contributions portent sur trois volets : la spécification des exigences, la modélisation du comportement et la vérification. Pour le volet spécification, une nouvelle classification des exigences temporelles les plus communément utilisées a été proposée. Ensuite, afin de cadrer l’utilisateur durant l’expression des exigences, une grammaire de spécification à base de motifs prédéfinis en langage naturel est développée. Les exigences générées sont syntaxiquement précises et correctes quand elles sont prises individuellement, néanmoins cela ne garantie pas la cohérence de l’ensemble des exigences exprimées. Ainsi, nous avons développé des mécanismes capables de détecter certains types d’incohérences entre les exigences temporelles. Pour le volet modélisation du comportement, nous avons proposé un algorithme de transformation des state-machine avec des annotations temporelles en des automates temporisés. L’idée étant de manipuler une notation assez intuitive et de générer automatiquement des modèles formels qui se prêtent à la vérification. Finalement, pour le volet vérification, nous avons adopté une technique de vérification à base d’observateurs et qui repose sur le model-checking. Concrètement, nous avons élaboré une base de patterns d’observation (ou observateurs) ; chacun des patterns développés est relatif à un type d’exigence temporelle dans la nouvelle classification. Ainsi, la vérification est réduite à une analyse d’accessibilité des états correspondants à la violation de l’exigence associée / The work developed in this thesis aims to assist the engineering process of temporal requirements for time-constrained complex systems. Our contributions concern three phases: the specification, the behaviour modelling and the verification. For the specification of temporal requirements, a new temporal properties typology taking into account all the common requirements one may meet when dealing with requirements specification, is introduced. Then, to facilitate the expression, we have proposed a structured English grammar. Nevertheless, even if each requirement taken individually is correct, we have no guarantee that a set of temporal properties one may express is consistent. Here we have proposed an algorithm based on graph theory techniques to check the consistency of temporal requirements sets. For the behaviour modelling, we have proposed an algorithm for transforming UML State Machine with time annotations into Timed Automata (TA). The idea is to allow the user manipulating a quite intuitive notation (UML SM diagramsduring the modelling phase and thereby, automatically generate formal models (TA) that could be used directly by the verification process. Finally, for the verification phase, we have adopted an observer-based technique. Actually, we have developed a repository of observation patterns where each pattern is relative to a particular temporal requirement class in our classification. Thereby, the verification process is reduced to a reachability analysis of the observers’ KO states relatives to the requirements’ violation

This thesis describes extensions to state machines in the Umple model-oriented programming language to offer queued state machines (QSM), pooled state machines (PSM) and handing of the arrival of unexpected events. These features allow for modeling the behavior of a system or protocol in a more accurate way in Umple because they enable detecting and fixing common design errors such as unspecified receptions. In addition, they simplify the communication between communicating state machines by allowing for asynchronous calls of events and passing of messages between state machines. Also, a pooled state machine (PSM) has been developed to provide a different policy of handling events that avoid unspecified receptions. This mechanism has similar semantics as a queued state machine, but it differs in the way of detecting unspecified receptions because it helps handling these errors. Another mechanism has been designed to use the keyword ‘unspecified’ in whatever state of a state machine the user wants to detect these errors. In this thesis, the test-driven development (TDD) process has been followed to first modify the Umple syntax to add ‘queued,’ ‘pooled,’ and ‘unspecified’ keywords to Umple state machine’s grammar; and second, to make a change to the Umple semantics in order to implement these extensions in Umple. Then, additional modifications have been made to allow for Java code generation from those types of state machines. Finally, more test cases have been written to ensure that these models are syntactically and semantically correct. In order to show the usefulness and usability of these new features, an example is shown as a case study that is modeled using the queued state machine (QSM) besides other small tests cases.