In the context of Service-Oriented Systems (SOS), services represent loosely coupled discrete units that can be created, invoked, composed and decomposed upon a client request. In such a setting, where complex systems are composed out of services based on the client request, ensuring the expected level of Quality-of-Service (QoS) becomes a difficult task. In systems built on service-oriented principles, the formal specification of both functional and extra-functional system behavior, service availability, compatibility and interoperability between different services and systems have become important issues. To be compliant with the new features, the REMES language has been extended towards SOS with new constructs that have been given formal semantics. In this thesis, we propose transformation rules, definitions and techniques for transforming these new constructs into Timed Automata (TA) counterparts to facilitate the formal analysis. Also, we present an extension to an existing REMES SOS IDE toolset for performing an automated transformation of the REMES SOS models into the TA framework suitable for the formal analysis with the UPPAAL model-checker. The contribution from our work is on two fronts: a) define transformation rules for all of the constructs specific for the REMES SOS modeling and b) prototype implementation of the transformation rules as an extension add-on to the already existing IDE for modeling SOS to perform the automated transformation. The benefit of performing an automated transformation of the REMES SOS models in TA is twofold. First, by automating the transformation process, the process of validation of the models becomes faster. Second, we considerably reduce the influence from the human factor in the entire process, and at the same time lower the risks of introducing errors into the systems in the phase of creating the formal model. Additional benefit from the automated process is that the SOS designer does not have to be a verification expert in order to be able to verify the modeled system.

In this thesis we contribute to the Progress IDE, an integrated development enviroment for real-time embedded systems and more precisely to the REMES toolchain, a set of tools to enabling construction and analysis of embedded system behavior models. The contribution aims to facilitate the formal analysis of behavioral models, so that certain extra-functional properties might be verified during early stages of development. Previous work in the field proposes use of the Priced Timed Automata framework for verification of such properties. The thesis outlines the main points where the current toolchain should be extended in order to allow formal analysis of modeled components. Result of the work is a prototype, which minimizes the manual efforts of system designer by model to model transformations and provides seamless integration with existing tools for formal analysis.

In this thesis we contribute to the Progress IDE, an integrated development enviroment for real-time embedded systems and more precisely to the REMES toolchain, a set of tools to enabling construction and analysis of embedded system behavior models. The contribution aims to facilitate the formal analysis of behavioral models, so that certain extra-functional properties might be verified during early stages of development. Previous work in the field proposes use of the Priced Timed Automata framework for verification of such properties. The thesis outlines the main points where the current toolchain should be extended in order to allow formal analysis of modeled components. Result of the work is a prototype, which minimizes the manual efforts of system designer by model to model transformations and provides seamless integration with existing tools for formal analysis.

In the context of building software systems, Service-oriented Systems (SOS) have become one of the major research topics in the past few years. In SOS, services are basic functional units that can be created, invoked, composed, and if needed deleted on-the-fly. Since these software systems are composed of different services there is no easy way to assure the Quality of Service (QoS), therefore, formal specification of both functional and extra-functional system behaviour, compatibility, and interoperability between different services have become important issues. As a way to address this issues, resource-aware timing behavioural language REMES was chosen to be extended towards service-oriented paradigm with service specific information, such as type, capacity, time-to-serve, etc., as well as Boolean predicate constraints on control flow guarantees. In this thesis we present a design framework that provides a graphical user interface for behaviour modelling of services based on REMES language. NetBeans Visual Library API is used to display editable service diagrams with support for graph-oriented models. A textual dynamic service composition language was implemented, together with means to automatically verify service composition correctness. We ensure also an automated traceability between service specification interfaces, where both modelling levels are combined in an efficient tool for designing SOS.

Cette thèse présente des techniques d'optimisation et d'approximation rationnelle ayant des applications en synthèse et identification de systèmes passifs. La première partie décrit un problème de Zolotarev : on cherche à maximiser sur une famille d'intervalles l'infimum du module d'une fonction rationnelle de degré donné, tout en contraignant son module à ne pas dépasser 1 sur une autre famille d'intervalles. On s'intéresse dans un premier temps à l'existence et à la caractérisation des solutions d'un tel problème. Deux algorithmes, de type Remes et correction différentielle, sont ensuite présentés et étudiés. Le lien avec la synthèse de filtres hyperfréquences est détaillé. La théorie présentée permet en fait le calcul de fonctions de filtrage, multibandes ou monobandes, respectant un gabarit fixé. Celle-ci a été appliquée à la conception de plusieurs filtres hyperfréquences multibandes dont les réponses théoriques et les mesures sont données. La deuxième partie concerne l'approximation rationnelle Schur d'une fonction Schur. Une fonction Schur est une fonction analytique dans le disque unité bornée par 1 en module. On étudie tout d'abord l'algorithme de Schur multipoints, qui fournit un paramétrage des fonctions strictement Schur. Le lien avec les fonctions rationnelles orthogonales, obtenu grâce à un théorème de type Geronimus, est ensuite présenté. Celui-ci permet alors d'établir certaines propriétés d'approximation dans le cas peu étudié où les points d'interpolation tendent vers le bord du disque. En particulier, une convergence en métrique de Poincaré est obtenue grâce à une extension d'un théorème de type Szego. Une étude numérique sur l'approximation rationnelle Schur à degré fixé est aussi réalisée.