This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.

In order to generate substantial market impact, mobile applications must be able to run on multiple platforms. Hence, software engineers face a multitude of technologies and system versions resulting in static variability. Furthermore, due to the dependence on sensors and connectivity, mobile software has to adapt its behavior accordingly at runtime resulting in dynamic variability. However, software engineers need to assure quality of a mobile application even with this large amount of variability—in our approach by the use of model-based testing (i.e., the generation of test cases from models). Recent concepts of test metamodels cannot efficiently handle dynamic variability. To overcome this problem, we propose a process for creating black-box test models based on dynamic feature Petri nets, which allow the description of configuration-dependent behavior and reconfiguration. We use feature models to define variability in the system under test. Furthermore, we illustrate our approach by introducing an example translator application.

Companies strive to improve their business processes in order to remain competitive. Process mining aims to infer meaningful insights from process-related data and attracted the attention of practitioners, tool-vendors, and researchers in recent years. Traditionally, event logs are assumed to describe the as-is situation. But this is not necessarily the case in environments where logging may be compromised due to manual logging. For example, hospital staff may need to manually enter information regarding the patient’s treatment. As a result, events or timestamps may be missing or incorrect. In this paper, we make use of process knowledge captured in process models, and provide a method to repair missing events in the logs. This way, we facilitate analysis of incomplete logs. We realize the repair by combining stochastic Petri nets, alignments, and Bayesian networks. We evaluate the results using both synthetic data and real event data from a Dutch hospital. / Unternehmen optimieren ihre Geschäftsprozesse laufend um im kompetitiven Umfeld zu bestehen. Das Ziel von Process Mining ist es, bedeutende Erkenntnisse aus prozessrelevanten Daten zu extrahieren. In den letzten Jahren sorgte Process Mining bei Experten, Werkzeugherstellern und Forschern zunehmend für Aufsehen. Traditionell wird dabei angenommen, dass Ereignisprotokolle die tatsächliche Ist-Situation widerspiegeln. Dies ist jedoch nicht unbedingt der Fall, wenn prozessrelevante Ereignisse manuell erfasst werden. Ein Beispiel hierfür findet sich im Krankenhaus, in dem das Personal Behandlungen meist manuell dokumentiert. Vergessene oder fehlerhafte Einträge in Ereignisprotokollen sind in solchen Fällen nicht auszuschließen. In diesem technischen Bericht wird eine Methode vorgestellt, die das Wissen aus Prozessmodellen und historischen Daten nutzt um fehlende Einträge in Ereignisprotokollen zu reparieren. Somit wird die Analyse unvollständiger Ereignisprotokolle erleichtert. Die Reparatur erfolgt mit einer Kombination aus stochastischen Petri Netzen, Alignments und Bayes'schen Netzen. Die Ergebnisse werden mit synthetischen Daten und echten Daten eines holländischen Krankenhauses evaluiert.

Petri nets are a simple formalism for modelling concurrent computation. This formalism has been proposed as a promising tool to describe and analyse biochemical networks. In this thesis, we explore the structural properties of Petri nets as a mean to provide information about the biochemical system evolution and its dynamics, especially when kinetic data are missing, making simulations impossible. In particular, we consider the structural properties of siphons and traps. We show that these structures entail a family of particular stability properties which can be characterized by a fragment of CTL over infinite state structures. Mixed integer linear programs have been proposed and a state-of-the-art algorithm from the Petri net community has been described later to compute minimal sets of siphons and traps in Petri nets. We present a simple boolean model capturing these notions and compare SAT and CLP methods for enumerating the set of all minimal siphons and traps of a Petri net. Our methods are applied to a benchmark composed of the 403 models from the biomodels.net repository. We analyse why these programs perform so well on even very large biological models. We show that, in networks with bounded tree-width, the existence of a minimal siphon containing a given set of places can be decided in a linear time, and the Siphon-Trap property as well. Moreover, we consider two other Petri net structural properties: place and transition invariants. We present a simple method to extract minimal semi-positive invariants of a Petri net as a constraint satisfaction problem on finite domains using constraint programming with symmetry detection and breaking. This allows us to generalize well-known results about the steady-state analysis of symbolic Ordinary Differential Equations systems corresponding to biochemical reactions by taking into account the structure of the reaction network. The study of the underlying Petri net, initially introduced for metabolic flux analysis, provides classes of reaction systems for which the symbolic computation of steady states is possible.

This study evaluated Department of Foreign Language Education students&amp / #65533 / perceptions on technology competence in regard to National Educational Technology Standards for Teachers (NETS-T) developed by International Society for Technology in Education (ISTE), in Middle East Technical University, in Ankara, Turkey. The NETS-T&amp / #65533 / s six sub standards -technology operations and concepts / planning and designing learning environments and experiences / teaching, learning, and the curriculum / assessment and evaluation / productivity and professional practice / social, ethical, legal, and human issues- were investigated in the study. 383 students participated in the study. 103 of them were freshmen, 98 of them were sophomores, 96 of them were juniors, and 86 of them were seniors. Besides, 96 of them were males, while 287 of them were females. This study was designed as a cross-sectional survey study. In order to collect the data, a survey, consisted of 44 Likert type, five point scale items, was developed by the researcher. The study results show that except for &amp / #65533 / technology operations and concepts&amp / #65533 / for which male students&amp / #65533 / perceptions were higher than female students&amp / #65533 / perceptions there was no significant difference between male and female students. There was no significant difference in &amp / #65533 / technology operations and concepts&amp / #65533 / across grade levels. There were no significant differences between freshmen&amp / #65533 / s and sophomores&amp / #65533 / perceptions for all of the sub-standards. In general, juniors&amp / #65533 / perceptions on the competence of NETS-T were higher than freshmen&amp / #65533 / s and sophomores&amp / #65533 / perceptions, and seniors&amp / #65533 / perceptions were higher than all of the other grade levels&amp / #65533 / perceptions. As a result, the findings of the study indicated that students&amp / #65533 / perceptions related with their competencies in the NETS_T needs to be increased.

Over the past decade, the ubiquity of business processes and their need for ongoing management in the same manner as other corporate assets has been recognized through the establishment of a dedicated research area: Business Process Management (or BPM). There are a wide range of potential software technologies on which a BPM o®ering can be founded. Although there is signi¯cant variation between these alternatives, they all share one common factor { their execution occurs on the basis of a business process model { and consequently, this ¯eld of technologies can be termed Process-Aware Information Systems (or PAIS). This thesis develops a conceptual foundation for PAIS based on the results of a detailed examination of contemporary o®erings including work°ow and case han- dling systems, business process modelling languages and web service composition languages. This foundation is based on 126 patterns that identify recurrent core constructs in the control-°ow, data and resource perspectives of PAIS. These patterns have been used to evaluate some of the leading systems and business process modelling languages. It also proposes a generic graphical language for de¯ning exception handling strategies that span these perspectives. On the basis of these insights, a comprehensive reference language { newYAWL { is developed for business process modelling and enactment. This language is formally de¯ned and an abstract syntax and operational semantics are provided for it. An assessment of its capabilities is provided through a comprehensive patterns-based analysis which allows direct comparison of its functionality with other PAIS. newYAWL serves as a reference language and many of the ideas embodied within it are also applicable to existing languages and systems. The ultimate goal of both the patterns and newYAWL is to improve the support and applicability of PAIS.

Denial-of-service attacks (DoS) and distributed denial-of-service attacks (DDoS) attempt to temporarily disrupt users or computer resources to cause service un- availability to legitimate users in the internetworking system. The most common type of DoS attack occurs when adversaries °ood a large amount of bogus data to interfere or disrupt the service on the server. The attack can be either a single-source attack, which originates at only one host, or a multi-source attack, in which multiple hosts coordinate to °ood a large number of packets to the server. Cryptographic mechanisms in authentication schemes are an example ap- proach to help the server to validate malicious tra±c. Since authentication in key establishment protocols requires the veri¯er to spend some resources before successfully detecting the bogus messages, adversaries might be able to exploit this °aw to mount an attack to overwhelm the server resources. The attacker is able to perform this kind of attack because many key establishment protocols incorporate strong authentication at the beginning phase before they can iden- tify the attacks. This is an example of DoS threats in most key establishment protocols because they have been implemented to support con¯dentiality and data integrity, but do not carefully consider other security objectives, such as availability. The main objective of this research is to design denial-of-service resistant mechanisms in key establishment protocols. In particular, we focus on the design of cryptographic protocols related to key establishment protocols that implement client puzzles to protect the server against resource exhaustion attacks. Another objective is to extend formal analysis techniques to include DoS- resistance. Basically, the formal analysis approach is used not only to analyse and verify the security of a cryptographic scheme carefully but also to help in the design stage of new protocols with a high level of security guarantee. In this research, we focus on an analysis technique of Meadows' cost-based framework, and we implement DoS-resistant model using Coloured Petri Nets. Meadows' cost-based framework is directly proposed to assess denial-of-service vulnerabil- ities in the cryptographic protocols using mathematical proof, while Coloured Petri Nets is used to model and verify the communication protocols using inter- active simulations. In addition, Coloured Petri Nets are able to help the protocol designer to clarify and reduce some inconsistency of the protocol speci¯cation. Therefore, the second objective of this research is to explore vulnerabilities in existing DoS-resistant protocols, as well as extend a formal analysis approach to our new framework for improving DoS-resistance and evaluating the performance of the new proposed mechanism. In summary, the speci¯c outcomes of this research include following results; 1. A taxonomy of denial-of-service resistant strategies and techniques used in key establishment protocols; 2. A critical analysis of existing DoS-resistant key exchange and key estab- lishment protocols; 3. An implementation of Meadows's cost-based framework using Coloured Petri Nets for modelling and evaluating DoS-resistant protocols; and 4. A development of new e±cient and practical DoS-resistant mechanisms to improve the resistance to denial-of-service attacks in key establishment protocols.

This thesis investigates a method for tackling the verification of parametric systems, systems whose behaviour may depend on the value of one or more parameters. The range of allowable values for such parameters may, in general, be large or unknown. This results in a large number of instances of a system that require verification, one instance for each allowable combination of parameter values. When one or more parameters are unbounded, the family of systems that require verification becomes infinite. Computer protocols are one example of such parametric systems. They may have parameters such as the maximum sequence number or the maximum number of retransmissions. Traditional protocol verification approaches usually only analyse and verify properties of a parametric system for a small range of parameter values. It is impossible to verify in this way every concrete instance of an infinite family of systems. Also, the number of reachable states tends to increase dramatically with increasing parameter values, and thus the well known state explosion phenomenon also limits the range of parameters for which the system can be analysed. In this thesis, we concentrate on the parametric verification of the Stop-and-Wait Protocol (SWP), an elementary flow control protocol. We have used Coloured Petri Nets (CPNs) to model the SWP, operating over an in-order but lossy medium, with two unbounded parameters: the maximum sequence number; and the maximum number of retransmissions. A novel method has been used for symbolically representing the parametric reachability graph of our parametric SWP CPN model. This parametric reachability graph captures exactly the infinite family of reachability graphs resulting from the infinite family of SWP CPNs. The parametric reachability graph is represented symbolically as a set of closed-form algebraic expressions for the nodes and arcs of the reachability graph, expressed in terms of the two parameters. By analysing the reachability graphs of the SWP CPN model for small parameter values, structural regularities in the reachability graphs were identified and exploited to develop the appropriate algebraic expressions for the parametric reachability graph. These expressions can be analysed and manipulated directly, thus the properties that are verified from these expressions are verified for all instances of the system. Several properties of the SWP that are able to be verified directly from the parametric reachability graph have been identified. These include a proof of the size of the parametric reachability graph in terms of both parameters, absence of deadlocks (undesired terminal states), absence of livelocks (undesirable cycles of behaviour from which the protocol cannot escape), absence of dead transitions (actions that can never occur) and the upper bounds on the content of the underlying communication channel. These are verified from the algebraic expressions and thus hold for all parameter values. Significantly, language analysis is also carried out on the parametric SWP. The parametric reachability graph is translated into a parametric Finite State Automaton (FSA), capturing symbolically the infinite set of protocol languages (i.e. sequences of user observable events) by means of similar algebraic expressions to those of the parametric reachability graph. Standard FSA reduction techniques were applied in a symbolic fashion directly to the parametric FSA, firstly to obtain a deterministic representation of the parametric FSA, then to obtain an equivalent minimised FSA. It was found that the determinisation procedure removed the effect of the maximum number of retransmissions parameter, and the minimisation procedure removed the effect of the maximum sequence number parameter. Conformance of all instances of the SWP over both parameters to its desired service language is proved. The development of algebraic expressions to represent the infinite class of Stop-and-Wait Protocols, and the verification of properties (including language analysis) directly from these algebraic expressions, has demonstrated the potential of this method for the verification of more general parametric systems. This thesis provides a significant contribution toward the development of a general parametric verification methodology.

O que fazem profissionais de educação numa produção televisiva? Nesta pesquisa, por meio de 'conversas' com praticantespensantes que atuam em produção de TV, e no uso de outros documentos (programas editados, argumentos, textos e roteiros), busco responder a essa pergunta e compreender as redes de conhecimentos e significações relativas aos espaçostempos de ação desses profissionais, entendidos como entre-lugares de educação e comunicação. A pesquisa, na perspectiva dos estudos com os cotidianos, se articula ao GRPESQ Currículo, redes educativas e imagens, do Laboratório Educação e Imagem/ProPEd/UERJ, e busca apoio em conversas/narrativas com/de professores que trabalharam/trabalham em televisão em especial, no programa Salto para o Futuro integrando a equipe de educação da TV Escola (MEC), ou atuando como consultores de séries temáticas. Sobre o assunto, também foram ouvidos responsáveis pela assessoria pedagógica dos canais Encuentro e Pakapaka, na Argentina, em doutorado-sanduíche, com o apoio da Capes. Como fundamentação teórica, além de pesquisas com os cotidianos, a partir de textos de Michel de Certeau, de Nilda Alves e de Inês Barbosa de Oliveira, dos quais emergem algumas das noções que permeiam essa investigação, ressalto a contribuição de autores da sociologia, como Pierre Bourdieu e Boaventura de Sousa Santos e, ainda, de represe ntantes dos chamados estudos culturais, entre eles Jesús Martín-Barbero, Nestor Canclini, Stuart Hall, Homi Bhabha entre outros. A questão do outro, da alteridade, que permeia a tese, em sua tessitura com narrativas e imagens, busca inspiração também nos escritos e em conversas com Carlos Skliar e nos textos de Jorge Larrosa. As conclusões possíveis destacam a importância das ações desses profissionais (professores) nesses espaçostempos televisivos. / What do professionals in education do in a television production? This research is an attempt to answer this question not only through conversations with the practitioners engaged in television production but also through sources such as edited programmes, arguments , texts and scripts. In doing so, I intend to understand the net of knowledge and meanings related to the so called space-times of action (here understood as an in-between place belonging to both education and communication fields) of these professionals. This work, under the perspective of everyday life studies, is aligned with the research group entitled Curriculum, educational networks and images, from the Education and Image Laboratory of the post graduation program in Education (ProPEd) of the University of Rio de Janeiro State (UERJ). It concentrates in talks with and narratives of educators who worked and have been working either as members of TV Escola which belongs to the Ministry of Education (MEC) or consultants of a particular educational television program entitled Salto para o Futuro. The ones responsible for the pedagogical consultancy of the channels Encuentro and Pakapaka from Argentina have also been interviewed thanks to a doctorate program supported by Capes. The theoretical framework is based on the writings of Michel de Certeau, Nilda Alves and Ines Barbosa de Oliveira; besides them, the contributions of the sociological thinkers Pierre Bourdieu and Boaventura de Souza Santos as well as some representatives of cultural studies such as Jesús Martín Barbero, Nestor Canclini, Stuart Hall, Homi Bhabha, among others, have also been used. Issues about the other and alterity have found inspiration in Carlos Skliar and Jorge Larrosas texts. The possible conclusions made highlight the relevance of the actions of these professionals (teachers) in this space-time television environment

This study is inserted in the Research Line of Professional Formation, Knowledge and Development in the Post Graduation Program in Education at UFSM (Federal University of Santa Maria RS Brazil). This research works from virtual meetings of teachers formation, involving 10 professors from the Administration Course Systems Analysis at FSG (Faculdade da Serra Gaúcha Caxias do Sul RS Brazil). These meetings were organized in five scenarios, each one of them with a question as a guideline. The goal is to identify how these professors construct their shared pedagogical knowledge, through a virtual interactive net for professional development (RADEP Academic Net for Professional Development). The main question in this research is: how professors construct shared pedagogical knowledge in virtual RADEP? The research is based in the theory of teachers formation and development, shared pedagogical knowledge, collaborative nets and new ways on how to learn how to be a teacher/professor. The approach, of a qualitative point of view, works with content analysis to capture the new emergent from teachers shared experiences. To come up these goals, the study brings up some reflections for the professors on the necessary knowledge for a pedagogical action, sharing experiences and aiming solutions for educative actions. Having as context nowadays technology, it is verified how a virtual environment may provide appropriation and expansion of pedagogical knowledge and, at the same time, the possibility for the professors to be mediators and mediated in a collaborative process in Superior Education. Though, RADEP is seen as an informational instrument that may provide shared pedagogical knowledge construction. Findings indicate that this kind of knowledge involves, systemically, several categories: pedagogical anguish, passivity related to formation, resistance in sharing knowledge, self-development and transformation. / O presente estudo está inserido na Linha de Pesquisa: Formação, Saberes e Desenvolvimento Profissional do Programa de Pós-Graduação em Educação da UFSM. A pesquisa trabalha a partir das reuniões virtuais de formação docente, envolvendo 10 professores do curso de Administração - Análise de Sistemas da FSG. Estas reuniões organizam-se em cinco cenários orientados, cada um, por uma questão norteadora. O objetivo é identificar como se dá a construção do conhecimento pedagógico compartilhado por esses docentes, via rede interativa virtual para o desenvolvimento profissional. (RADEP - Rede Acadêmica de Desenvolvimento Profissional). O problema da pesquisa é: Como os professores do ensino superior constroem conhecimentos pedagógicos compartilhados na RADEP virtual? A pesquisa utiliza como aportes teóricos: formação e desenvolvimento profissional docente, conhecimento pedagógico compartilhado, redes colaborativas e novas modalidades de aprender a ser professor. A abordagem, de cunho qualitativo, trabalha com a análise de conteúdo para capturar o novo emergente das experiências compartilhadas pelos professores. Para atingir esses objetivos, o estudo proporciona aos docentes reflexões sobre os saberes necessários ao exercício pedagógico, compartilhando experiências e buscando soluções para as práticas educativas. Tendo por contexto as tecnologias atuais, verifica-se como um ambiente virtual proporciona a apropriação e expansão dos conhecimentos pedagógicos e, ao mesmo tempo, a possibilidade dos professores serem mediadores e mediados dentro de um processo de colaboração na Educação Superior. Assim a RADEP é vista como um instrumento informacional que pode proporcionar a construção de conhecimentos pedagógicos compartilhados. Os achados indicam que este tipo de conhecimento envolve, de forma sistêmica, diversas categorias explicativas: angústia pedagógica; passividade frente à formação; resistência ao compartilhamento; auto-desenvolvimento e transformação.