Modelagem e controle de execução são duas abordagens do gerenciamento de processos de negócio que, embora complementares, têm se desenvolvido independentemente. Por um lado, a modelagem é normalmente conduzida por especialistas de negócio e explora aspectos semânticos do processo. Por outro lado, o controle de execução estuda mecanismos consistentes e eficientes de implementação. Este trabalho apresenta um método algorítmico que relaciona modelagem e controle de execução, por meio da geração de expressões algébricas a partir de digrafos acíclicos. Por hipótese, assumimos que modelos de processos de negócio são formados por estruturas baseadas em grafos, e mecanismos de controle de execução são baseados na interpretação de expressões de álgebra de processos. Para a geração de expressões algébricas, esta tese apresenta as propriedades topológicas de digrafos série-paralelo e define um sistema de transformação baseado em redução de digrafos. Além disso, um algoritmo de identificação de digrafos série-paralelo e geração de expressões algébricas é apresentado. O texto também discute o tratamento de digrafos que não são série-paralelo e apresenta, para alguns desses casos, soluções baseadas em mudanças topológicas. Finalmente, o algoritmo é ilustrado com o estudo de caso de uma aplicação real. / Modeling and execution control are complementary approaches of business process management that have been developed independently. On one hand, modeling is usually performed by business specialists and explores semantical aspects of the business process. On other hand, execution control studies consistent and efficient mechanisms for implementation. This work presents an algorithmic method which joins modeling and execution control through algebraic expression generation from acyclic digraphs. By hypothesis, we assume that business process models are defined by graph structures, and execution control mechanisms are based on interpretation of process algebra expressions. For algebraic expression generation, this thesis presents the topological properties of series-parallel digraphs and defines a transformation system based on digraph reduction. Therefore, we present an algorithm for identification of series-parallel digraphs and generation of algebraic expressions. This work also discusses the treatment of non-series-parallel digraphs and presents solutions based on topological changing for some cases. Finally, the algorithm is illustrated with a case study based on a real system.

Der vierte Band der wissenschaftlichen Schriftenreihe Eingebettete Selbstorganisierende Systeme widmet sich der Entwicklung von Fehlermodellen für eingebettete, verteilte Multi – Prozessorsysteme. Diese werden zu einem hierarchischen Netzwerk zur Steuerung von Flugzeugen (Avionik) verbunden und mehr und mehr im Automotive Bereich eingesetzt. Hier gilt es höchste Sicherheitsstandards einzuhalten und maximale Verfügbarkeit zu garantieren. Herr Fischer integriert die Modellierung von möglichen Fehlern in den Entwurfsprozess. Auf Grundlage des π-Kalküls entwickelt Herr Fischer ein formales Fehlermodell, das eine einheitliche Modellierung von Fehlerfällen unterstützt. Dabei werden interessante Bezüge zur Bi-Simulation sowie zu Methoden des Modell Checkings hergestellt. Die theoretischen Ergebnisse werden an einem komplexen Beispiel anschaulich illustriert. So kann der Leser die Mächtigkeit des entwickelten Ansatzes nachvollziehen und wird motiviert, die entwickelte Methodik auf weitere Anwendungsfälle zu übertragen. / The 4th volume of the scientific series Eingebettete, selbstorganisierende Systeme (Embedded Self-Organized Systems) outlines the design of fault models for embedded distributed multi processor systems. These multi processor systems will be connected to a hierarchical network to control airplanes (avionics) and also be used more and more in the automotive area. Here it is essential to meet highest safety standards and to ensure the maximum of availability. Mr Fischer integrates the modelling of potential faults into the design process. Based on the pi-calculus, he develops a formal framework, which supports a standardised modelling of faults. Thereby, interesting connections to the Bi-Simulation as well as to methods of the Model checking are established. The theoretical results are depicted on a complex example. So it is possible for the reader to understand the complexity of this approach and is motivated to use the developed methodology in other applications. I am glad that Mr Fischer publishes his important research in this scientific series.

Orientador: Mauricio Ferreira Magalhães / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-08-08T01:16:08Z (GMT). No. of bitstreams: 1 Nader_MarcosVaninePortilhode_M.pdf: 1214383 bytes, checksum: 40e83a8be1c7e86e788d810a8799f6b8 (MD5) Previous issue date: 2006 / Resumo: Duas áreas importantes estão em desenvolvimento: Gerência de Processos de Negócios (Business Process Management) e Orquestração de Web Services (Web Services Orchestration). Ambas têm um objetivo que é integrar aplicações ou outros processos que tenham interfaces web services, usando o paradigma de processos de negócios. Uma linguagem que vem sendo difundida para essas aplicações é a BPEL (Business Process Execution Language). Este trabalho apresenta um framework aplicável à análise e verificação de processos de negócios escritos em BPEL através do uso de Pi-Calculus. Pi-Calculus é uma álgebra de processos que possui mecanismos formais para criação e ativação de processos que se comunicam através da troca de mensagens em canais, usando o modelo de rendezvous síncrono. Nesse framework, o processo BPEL é traduzido para um programa Pi-Calculus. Uma Máquina Virtual Pi-Calculus (MVP) recebe o programa Pi-Calculus e produz todas as reações possíveis, ou seja, gera todos os caminhos de execução que o programa pode seguir. A partir desse resultado, efetua-se a verificação de propriedades como: atendimento às especificações de mais alto nível, ordenação de eventos e ocorrência ou não de deadlocks. Em termos práticos, uma ferramenta desse tipo pode ser incorporada aos Sistemas de Gerência de Processos de Negócios (Business Process Management Systems - BPMS) para ampliar a cobertura de testes durante as fases de análise e implementação de um processo dentro do seu ciclo de vida. Nesses tipos de sistemas, a reparação de um erro durante a fase de execução é muito mais custosa que nos sistemas tradicionais / Abstract: Two important areas have been in development lately: Business Process Management and Web Service Orchestration. In both of them, the objective is to integrate applications with web services interface through business process paradigm. A number of languages have been proposed with consensus being formed around BPEL (Business Process Execution Language). This dissertation presents a framework for BPEL processes analysis and verification through Pi-Calculus. Pi-Calculus is a process algebra with formal mechanisms for processes creation and activation; these processes communicate sending and receiving messages through channels using the synchronous rendezvous model. In this framework, the BPEL process is translated to a Pi-Calculus program, A Pi-Calculus Virtual Machine (MVP) receives a Pi-calculus program and executes all possible reactions, that is, it generates all execution paths possible to be taken. With this result, the properties such as high-level specification accomplishment, events ordering and deadlock freedom are verified. In practical terms, a tool of this sort can be part of a Business Process Management System (BPMS) to broaden test coverage during the analysis and implementation phases within a process life cycle. In these kinds of systems, a repairing mistake during the execution phase is more complex than in traditional systems / Mestrado / Engenharia de Computação / Mestre em Engenharia Elétrica

Der vierte Band der wissenschaftlichen Schriftenreihe Eingebettete Selbstorganisierende Systeme widmet sich der Entwicklung von Fehlermodellen für eingebettete, verteilte Multi – Prozessorsysteme. Diese werden zu einem hierarchischen Netzwerk zur Steuerung von Flugzeugen (Avionik) verbunden und mehr und mehr im Automotive Bereich eingesetzt. Hier gilt es höchste Sicherheitsstandards einzuhalten und maximale Verfügbarkeit zu garantieren. Herr Fischer integriert die Modellierung von möglichen Fehlern in den Entwurfsprozess. Auf Grundlage des π-Kalküls entwickelt Herr Fischer ein formales Fehlermodell, das eine einheitliche Modellierung von Fehlerfällen unterstützt. Dabei werden interessante Bezüge zur Bi-Simulation sowie zu Methoden des Modell Checkings hergestellt. Die theoretischen Ergebnisse werden an einem komplexen Beispiel anschaulich illustriert. So kann der Leser die Mächtigkeit des entwickelten Ansatzes nachvollziehen und wird motiviert, die entwickelte Methodik auf weitere Anwendungsfälle zu übertragen. / The 4th volume of the scientific series Eingebettete, selbstorganisierende Systeme (Embedded Self-Organized Systems) outlines the design of fault models for embedded distributed multi processor systems. These multi processor systems will be connected to a hierarchical network to control airplanes (avionics) and also be used more and more in the automotive area. Here it is essential to meet highest safety standards and to ensure the maximum of availability. Mr Fischer integrates the modelling of potential faults into the design process. Based on the pi-calculus, he develops a formal framework, which supports a standardised modelling of faults. Thereby, interesting connections to the Bi-Simulation as well as to methods of the Model checking are established. The theoretical results are depicted on a complex example. So it is possible for the reader to understand the complexity of this approach and is motivated to use the developed methodology in other applications. I am glad that Mr Fischer publishes his important research in this scientific series.

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles. / We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a high-level formalism derived from the π-calculus, for considering stochastic, timed, deterministic or indeterministic behaviors. However, in the π-calculus, the basic communication primitive of systems is the synchronous point-to-point communication. However, mobile systems that use wireless networks, mostly communicate by local broadcast. Therefore, we first define the broadcast communication into the π-calculus, to better model the systems we study. We propose to use probabilistic and stochastic versions of the algebra we have defined to allow performance studies. We define a temporal version to consider time in the models. But the lack of tools for analyzing properties of models specified with π-calculus is a major obstacle to our work and its objectives. The definition of translation rules into the PRISM language allows us to translate our models in low-level models which can support model checking, namely discrete time, or continuous time Markov chains, timed automata, or probabilistic timed automata. We chose the PRISM model checker because, in our best knowledge, in its latest version, it is the only tool that supports the low-level formalisms that we have previously cited, and thus, makes it possible to realize complete performability studies. This approach allows us to overcome the lack of model checkers for our models. Subsequently, we apply these theoretical concepts to analyse performability of mobile wireless sensor networks.

Information flow properties are away of specifying security properties of systems ,dating back to the work of Goguen and Meseguer in the eighties. In this framework ,a system is modeled as having high-level (or confidential)events as well as low-level (or public) events, and a typical property requires that the high-level events should not “influence ”the occurrence of low-level events. In other words, the sequence of low-level events observed from a system execution should not reveal “too much” information about the high-level events that may have taken place. For example, the trace-based “non-inference” property states that for every trace produced by the system, its projection to low-level events must also be a possible trace of the system. For a system satisfying non-inference, a low-level adversary (who knows the language generated by the system) viewing only the low-level events in any execution cannot infer any in-formation about the occurrence of high-level events in that execution. Other well-known properties include separability, generalized non-interference, non-deducibility of outputs etc. These properties are trace-based. Similarly there is another class of properties based on the structure of the transition system called bisimulation-based information flow properties, defined by Focardiand Gorrieriin1995. In our thesis we study the problem of model-checking the well-known trace-based and bisimulation-based properties for some popular classes of infinite-state system models. We first consider trace-based properties. We define some language-theoretic operations that help to characterize language-inclusion in terms of satisfaction of these properties. This gives us a reduction of the language inclusion problem for a class of system models, say F, to the model-checking problem for F, whenever F, is effectively closed under these language-theoretic operations. We apply this result to show that the model-checking problem for Petri nets, push down systems and for some properties on deterministic push down systems is undecidable. We also consider the class of visibly pushdown systems and show that their model-checking problem is undecidable in general(for some properties).Then we show that for the restricted class of visibly pushdown systems in which all the high (confidential) event are internal, the model-checking problem becomes decidable. Similarly we show that the problem of model-checking bisimulation-based properties is undecidable for Petrinets, pushdown systems and process algebras. Next we consider the problem of detecting information leakage in programs. Here the programs are modeled to have low and high inputs and low outputs. The well known definition of“ non-interference” on programs says that in no execution should the low outputs depend on the high inputs. However this definition was shown to be too strong to be used in practice, with a simple(and considered to be safe)“password-checking” program failing it.“Abstract non-interference(ANI)”and its variants were proposed in the literature to generalize or weaken non-interference. We call these definitions qualitative refinements of non-interference. We study the problem of model-checking many classes of finite-data programs(variables taking values from a bounded domain)for these refinements. We give algorithms and show that this problem is in PSPACE for while, EXPTIME for recursive and EXPSPACE for asynchronous finite-data programs. We finally study different quantitative refinements of non-interference pro-posed in the literature. We first characterize these measures in terms of pre images. These characterizations potentially help designing analysis computing over and under approximations for these measures. Then we investigate the applicability of these measures on standard cryptographic functions.