Šiuo metu egzistuoja įvairiausių sudėtingų sistemų imitacinių modelių kūrimo technologijų ir priemonių. Šiame darbe aiškinama, kaip imitacinis modelis gali būti integruojamas į verslo valdymo sistemą. Taip pat įvertinama, kad verlo valdymo sistemos gali būti paskirstytos atskiruose kompanijose ar kompiutersiuose. Šiame darbe bus išanalizuota koncepcija, kaip apjungti atskirus imitacinius modelius. Išanalizuota modelių integravimo į informacinę sistemą technologija. Pateikiami gamybos ir paskirstymo imitacinių modelių matematiniai aprašai, naudojant DEVS(Discrete Event Simulation) ir PLA(Piece-Linear Aggregates) specifikacijų metodus. / At present, a large number of modeling and simulation techniques and tools have been developed to deal with complex business systems. In this paper, we concentrate on scenario illustrating, how simulation models can be integrated in to business management system. Different infrastructure forms are possible, because services may be implemented on single machine or distributed throughout several companies’ networks. In this paper a concept will be analyzed - how to combine different simulation models. The technology for involvement of simulation models in to information systems will be created. Also the problem of simulation model transformation in to program code will be solved. For model formalization we can use a method of Piece-Linear Aggregates (PLA) that belongs to the class of time automata model. PLA method is close to Discrete Event Simulation (DEVS) formalism, which is used to create wide purpose simulation models.

Formalios specifikacijos – tai matematinis programinės ar techninės įrangos aprašymas, kurį galima naudoti sistemos realizacijai. Formalių specifikacijų naudojimas dar negarantuoja specifikacijos teisingumo. Tam naudojami formalaus verifikavimo metodai. Šiame dokumente aptariami formalių specifikacijų validavimo metodai. Du populiaraiausi formalių specifikacijų validavimo metodai yra pasiekiamų būsenų grafo analizė bei invarianto tikrinimas. Pasiekiamų būsenų grafo analizę sudaro pasiekiamų būsenų grafo generavimas ir analizė. Grafo analizės metu ieškoma aklaviečių, uždarų ciklų, nepasiekiamų būsenų, atliekamas būsenų koordinačių apribojimų tikrinimas bei invarianto tikrinimas. Tradiciniai pasiekiamų būsenų grafo sudarymo algoritmai grafo sudarymui naudoja sistemos būsenų eilę. Kiekviena išanalizuota būsena įrašoma į pasiekiamų būsenų grafą. Dokumente aptariamas lygiagretaus programavimo naudojimas būsenų grafo generavimui, kuris analizuoja ir generuoja sistemos būsenas naudodamas lygiagrečias gijas. Eksperimentų su vienkanale aptarnavimo sistema metu nustatyta, kad lygiagretaus algoritmo naudojimas šio uždavinio metu leidžia pagerinti sistemos veikimą iki 35%, priklausomai nuo būsenų skaičiaus. / Arguably the most important task in creation of software is user requirement specification. Accurate requirement specification allows avoidance of errors in late stages of software development. This is extremely important in critical systems, where even vague error can cause great financial losses or even human victims. One of the methods used for precise user requirement specification is use of formal specifications. Formal specification is a mathematical method for describing of software or hardware, which might be suitable for system realization. Nevertheless, the construction of formal specifications does not guarantee the correctness of specification. For this reason formal specification validation is necessary. In this paper methods of formal specification validation are discussed. Two most popular methods of formal specification validation are reachable state graph analysis and invariant checking. Reachable state graph analysis consists of graph generation and graph analysis. Graphs can be analyzed for dead-ends, closed loops, state reach ability checking, coordinate restriction checking or invariant checking. Traditional reachable graph generation algorithm uses unanalyzed states queue to produce reachable state graph. Each step single state is analyzed and depending on results new vertex or edge is added to state graph. An improvement to the algorithm to consider is usage of parallel programming to process multiple states simultaneously. This allows increasing the... [to full text]

Sistemas de Informação de Escritórios são tipos particulares de sistemas de informação. São sistemas sócio-técnicos, muito complexos, com grande influência humana. O tempo tem grande importância no tratamento das informações, tanto na representação de informações temporais explícitas como em restrições de ordem temporal e em características que são alteradas com a evolução da aplicação. Neste trabalho é apresentado um modelo de dados para ser utilizado como método de especificação de requisitos de sistemas de informação de escritórios. 0 desenvolvimento de especificações é uma tarefa bastante complexa, devendo possibilitar a representação de todas as características da aplicação, tanto as estáticas como as comportamentais. A especificação de uma aplicação geralmente é muito extensa, sendo dispendido um tempo considerável em sua elaboração. Um aspecto importante no desenvolvimento de especificações é a verificação da corretude destas, devido a complexidade que apresentam. Uma maneira de gerar especificações mais corretas e em menor espaço de tempo é através da reutilização de especificações anteriormente construídas e já validadas através de implementações. Neste trabalho optou-se por utilizar um modelo de dados orientado a objetos para especificar os sistemas de informação de escritórios. A utilização do paradigma de orientação a objetos na modelagem permite a definição de uma biblioteca de classes de objetos, classes estas identificadas em diversas especificações realizadas em um determinado domínio de aplicação. As classes constantes desta biblioteca podem ser reutilizadas de maneira bastante eficiente em especificações posteriores. A representação das características dinâmicas de uma aplicação, tais como a evolução dos objetos dentro do escritório, requer a possibilidade de representação de propriedades temporais. O modelo de dados utilizado na especificação deve permitir a representação de aspectos temporais tanto para definição de dados definidos em um domínio temporal como para representar a evolução dos valores assumidos pelos objetos durante sua existência. A possibilidade de representação dos aspectos temporais é um dos principais pontos desenvolvidos na elaboração do modelo de dados apresentado neste trabalho. O modelo apresentado denomina-se TF-ORM (Temporal Fuctionality in Objects with Roles Model), sendo uma extensão do modelo F-ORM (Functionality in Objects with Roles Model) [DEA 91a,b,c]. Foram incorporadas a este modelo os necessários aspectos temporais e foram ampliadas características básicas para captar melhor as particularidades do domínio de sistemas de informação de escritórios, principalmente no que à concerne representação de alguma parcela de trabalho humano. O modelo resultante, TF-ORM, um modelo de dados orientado a objetos, temporal, que utiliza o conceito de papéis para representar os diferentes comportamentos de um objeto. A possibilidade de recuperação de informações de um banco de dados que implemente o modelo de dados proposto foi também considerada. Neste trabalho é apresentada uma linguagem de recuperação de informações (linguagem de consulta) para o modelo de dados TF-ORM. Especial atenção é dada as consultas temporais. Como no modelo proposto são armazenados tanto o tempo de transação como o de validade, a linguagem de recuperação pode ser utilizada para recuperar informações referentes ao estado atual do banco de dados (informações atualmente válidas), a respeito de estados passados e futuros (informações válidas no passado e que serão válidas em estados futuros, de acordo com o atual conhecimento dos dados) e referentes a histórias passadas do banco de dados (informações que se acreditava como válidas em algum momento do passado). É apresentado em estudo de caso completo com o objetivo de validar o modelo de dados proposto e sua eficiência na especificação deste tipo de sistema de informação. O trabalho apresenta ainda a descrição de um ambiente de apoio a especificações que faz use de uma biblioteca de classes. Através deste ambiente, a especificação de uma aplicação é construída gradualmente, estando disponíveis opções de listagem das partes já definidas e de informações da biblioteca de classes para serem reutilizadas. As especificações geradas através deste ambiente apresentam pouca possibilidade de erro, uma vez que são efetuados vários procedimentos de verificação das informações fornecidas. / Office Information Systems constitute special kinds of information systems - very complex socio-technical systems, with large human influence. Time is very important in the information representation, not only for explicit temporal information but also for restrictions on temporal ordering of activities to be executed and to record the temporal evolution of property values. In this work a data model to be used as a requirement specification method for office infoimations systems is presented. Specification development is a complex task. All the possible characteristics of an application, static and behavioral, shall be represented. An applications' specification is usually not a trivial task, and a big amount of time is used to develop it. Specifications are usually very complex and the possibility of verifying the correctness is an important aspect to be considered. The reuse of specifications is a way to obtain a better rate of correctness spending less time, using parts of specifications that were already validated through previous implementations. An object-oriented data model is used in this work to specify office information systems. The use of the object-oriented paradigm allows the definition of a class library containing classes identified in several specifications constructed in a specific application domain. The reuse of classes of such a library in new specifications gives efficiency to the process. To represent the dynamic characteristics of an application, such as the documents evolution within the office, it is necessary to be able to represent temporal properties. The data model used in the specification shall allow the representation of these temporal aspects not only to model data defined in a temporal domain but also to represent the objects values evolution during an objects existence. The representaion of temporal aspects is one of the main issues developed in the data model defined in this work. The data model is called TF-ORM (Temporal Fuctionality in Objects with Roles Model), and is an extention to the F-ORM (Functionality in Objects with Roles Model) model [DEA 91 a,b,c]. To this model the necessary temporal aspects were added and the basic characteristics were enlarged to better capture the particular aspects of the office habilitation systems domain, specially concerning the representation of some parts of human work. The resulting model. TF-ORM, is an object-oriented temporal data model and uses the concept of roles to represent an objects different behaviors. The possibility of retrieving information from a database specified through this data model is also considered and a query language for the TF-ORM data model is presented. Special attention is given to the retrieval of temporal information. The TFORM data model stores both the transaction and the valid time associated to dynamic properties and allows the retrieving of information fettering the databases' actual state (actually valid information), information refering the databases' past and future states (valid information in the past and information that will be valid in the future according to the actual data knowledge) and information about the databases' past history (information that was believed to be true in some moment in the past). A complete case study is presented to validate the TF-ORM data model and its efficiency as a specification method for office information systems. An environment to support specifications using TF-ORM is described. This environment uses a class library. The use of this environment allows stepwise construction of a specification, with the access to listings of the already defined parts and to the information of the class library to be reused. The contructed specifications present a small rate of errors, due to several verification procedures embedded in the environment.

Sistemas de Informação de Escritórios são tipos particulares de sistemas de informação. São sistemas sócio-técnicos, muito complexos, com grande influência humana. O tempo tem grande importância no tratamento das informações, tanto na representação de informações temporais explícitas como em restrições de ordem temporal e em características que são alteradas com a evolução da aplicação. Neste trabalho é apresentado um modelo de dados para ser utilizado como método de especificação de requisitos de sistemas de informação de escritórios. 0 desenvolvimento de especificações é uma tarefa bastante complexa, devendo possibilitar a representação de todas as características da aplicação, tanto as estáticas como as comportamentais. A especificação de uma aplicação geralmente é muito extensa, sendo dispendido um tempo considerável em sua elaboração. Um aspecto importante no desenvolvimento de especificações é a verificação da corretude destas, devido a complexidade que apresentam. Uma maneira de gerar especificações mais corretas e em menor espaço de tempo é através da reutilização de especificações anteriormente construídas e já validadas através de implementações. Neste trabalho optou-se por utilizar um modelo de dados orientado a objetos para especificar os sistemas de informação de escritórios. A utilização do paradigma de orientação a objetos na modelagem permite a definição de uma biblioteca de classes de objetos, classes estas identificadas em diversas especificações realizadas em um determinado domínio de aplicação. As classes constantes desta biblioteca podem ser reutilizadas de maneira bastante eficiente em especificações posteriores. A representação das características dinâmicas de uma aplicação, tais como a evolução dos objetos dentro do escritório, requer a possibilidade de representação de propriedades temporais. O modelo de dados utilizado na especificação deve permitir a representação de aspectos temporais tanto para definição de dados definidos em um domínio temporal como para representar a evolução dos valores assumidos pelos objetos durante sua existência. A possibilidade de representação dos aspectos temporais é um dos principais pontos desenvolvidos na elaboração do modelo de dados apresentado neste trabalho. O modelo apresentado denomina-se TF-ORM (Temporal Fuctionality in Objects with Roles Model), sendo uma extensão do modelo F-ORM (Functionality in Objects with Roles Model) [DEA 91a,b,c]. Foram incorporadas a este modelo os necessários aspectos temporais e foram ampliadas características básicas para captar melhor as particularidades do domínio de sistemas de informação de escritórios, principalmente no que à concerne representação de alguma parcela de trabalho humano. O modelo resultante, TF-ORM, um modelo de dados orientado a objetos, temporal, que utiliza o conceito de papéis para representar os diferentes comportamentos de um objeto. A possibilidade de recuperação de informações de um banco de dados que implemente o modelo de dados proposto foi também considerada. Neste trabalho é apresentada uma linguagem de recuperação de informações (linguagem de consulta) para o modelo de dados TF-ORM. Especial atenção é dada as consultas temporais. Como no modelo proposto são armazenados tanto o tempo de transação como o de validade, a linguagem de recuperação pode ser utilizada para recuperar informações referentes ao estado atual do banco de dados (informações atualmente válidas), a respeito de estados passados e futuros (informações válidas no passado e que serão válidas em estados futuros, de acordo com o atual conhecimento dos dados) e referentes a histórias passadas do banco de dados (informações que se acreditava como válidas em algum momento do passado). É apresentado em estudo de caso completo com o objetivo de validar o modelo de dados proposto e sua eficiência na especificação deste tipo de sistema de informação. O trabalho apresenta ainda a descrição de um ambiente de apoio a especificações que faz use de uma biblioteca de classes. Através deste ambiente, a especificação de uma aplicação é construída gradualmente, estando disponíveis opções de listagem das partes já definidas e de informações da biblioteca de classes para serem reutilizadas. As especificações geradas através deste ambiente apresentam pouca possibilidade de erro, uma vez que são efetuados vários procedimentos de verificação das informações fornecidas. / Office Information Systems constitute special kinds of information systems - very complex socio-technical systems, with large human influence. Time is very important in the information representation, not only for explicit temporal information but also for restrictions on temporal ordering of activities to be executed and to record the temporal evolution of property values. In this work a data model to be used as a requirement specification method for office infoimations systems is presented. Specification development is a complex task. All the possible characteristics of an application, static and behavioral, shall be represented. An applications' specification is usually not a trivial task, and a big amount of time is used to develop it. Specifications are usually very complex and the possibility of verifying the correctness is an important aspect to be considered. The reuse of specifications is a way to obtain a better rate of correctness spending less time, using parts of specifications that were already validated through previous implementations. An object-oriented data model is used in this work to specify office information systems. The use of the object-oriented paradigm allows the definition of a class library containing classes identified in several specifications constructed in a specific application domain. The reuse of classes of such a library in new specifications gives efficiency to the process. To represent the dynamic characteristics of an application, such as the documents evolution within the office, it is necessary to be able to represent temporal properties. The data model used in the specification shall allow the representation of these temporal aspects not only to model data defined in a temporal domain but also to represent the objects values evolution during an objects existence. The representaion of temporal aspects is one of the main issues developed in the data model defined in this work. The data model is called TF-ORM (Temporal Fuctionality in Objects with Roles Model), and is an extention to the F-ORM (Functionality in Objects with Roles Model) model [DEA 91 a,b,c]. To this model the necessary temporal aspects were added and the basic characteristics were enlarged to better capture the particular aspects of the office habilitation systems domain, specially concerning the representation of some parts of human work. The resulting model. TF-ORM, is an object-oriented temporal data model and uses the concept of roles to represent an objects different behaviors. The possibility of retrieving information from a database specified through this data model is also considered and a query language for the TF-ORM data model is presented. Special attention is given to the retrieval of temporal information. The TFORM data model stores both the transaction and the valid time associated to dynamic properties and allows the retrieving of information fettering the databases' actual state (actually valid information), information refering the databases' past and future states (valid information in the past and information that will be valid in the future according to the actual data knowledge) and information about the databases' past history (information that was believed to be true in some moment in the past). A complete case study is presented to validate the TF-ORM data model and its efficiency as a specification method for office information systems. An environment to support specifications using TF-ORM is described. This environment uses a class library. The use of this environment allows stepwise construction of a specification, with the access to listings of the already defined parts and to the information of the class library to be reused. The contructed specifications present a small rate of errors, due to several verification procedures embedded in the environment.

Sistemas de Informação de Escritórios são tipos particulares de sistemas de informação. São sistemas sócio-técnicos, muito complexos, com grande influência humana. O tempo tem grande importância no tratamento das informações, tanto na representação de informações temporais explícitas como em restrições de ordem temporal e em características que são alteradas com a evolução da aplicação. Neste trabalho é apresentado um modelo de dados para ser utilizado como método de especificação de requisitos de sistemas de informação de escritórios. 0 desenvolvimento de especificações é uma tarefa bastante complexa, devendo possibilitar a representação de todas as características da aplicação, tanto as estáticas como as comportamentais. A especificação de uma aplicação geralmente é muito extensa, sendo dispendido um tempo considerável em sua elaboração. Um aspecto importante no desenvolvimento de especificações é a verificação da corretude destas, devido a complexidade que apresentam. Uma maneira de gerar especificações mais corretas e em menor espaço de tempo é através da reutilização de especificações anteriormente construídas e já validadas através de implementações. Neste trabalho optou-se por utilizar um modelo de dados orientado a objetos para especificar os sistemas de informação de escritórios. A utilização do paradigma de orientação a objetos na modelagem permite a definição de uma biblioteca de classes de objetos, classes estas identificadas em diversas especificações realizadas em um determinado domínio de aplicação. As classes constantes desta biblioteca podem ser reutilizadas de maneira bastante eficiente em especificações posteriores. A representação das características dinâmicas de uma aplicação, tais como a evolução dos objetos dentro do escritório, requer a possibilidade de representação de propriedades temporais. O modelo de dados utilizado na especificação deve permitir a representação de aspectos temporais tanto para definição de dados definidos em um domínio temporal como para representar a evolução dos valores assumidos pelos objetos durante sua existência. A possibilidade de representação dos aspectos temporais é um dos principais pontos desenvolvidos na elaboração do modelo de dados apresentado neste trabalho. O modelo apresentado denomina-se TF-ORM (Temporal Fuctionality in Objects with Roles Model), sendo uma extensão do modelo F-ORM (Functionality in Objects with Roles Model) [DEA 91a,b,c]. Foram incorporadas a este modelo os necessários aspectos temporais e foram ampliadas características básicas para captar melhor as particularidades do domínio de sistemas de informação de escritórios, principalmente no que à concerne representação de alguma parcela de trabalho humano. O modelo resultante, TF-ORM, um modelo de dados orientado a objetos, temporal, que utiliza o conceito de papéis para representar os diferentes comportamentos de um objeto. A possibilidade de recuperação de informações de um banco de dados que implemente o modelo de dados proposto foi também considerada. Neste trabalho é apresentada uma linguagem de recuperação de informações (linguagem de consulta) para o modelo de dados TF-ORM. Especial atenção é dada as consultas temporais. Como no modelo proposto são armazenados tanto o tempo de transação como o de validade, a linguagem de recuperação pode ser utilizada para recuperar informações referentes ao estado atual do banco de dados (informações atualmente válidas), a respeito de estados passados e futuros (informações válidas no passado e que serão válidas em estados futuros, de acordo com o atual conhecimento dos dados) e referentes a histórias passadas do banco de dados (informações que se acreditava como válidas em algum momento do passado). É apresentado em estudo de caso completo com o objetivo de validar o modelo de dados proposto e sua eficiência na especificação deste tipo de sistema de informação. O trabalho apresenta ainda a descrição de um ambiente de apoio a especificações que faz use de uma biblioteca de classes. Através deste ambiente, a especificação de uma aplicação é construída gradualmente, estando disponíveis opções de listagem das partes já definidas e de informações da biblioteca de classes para serem reutilizadas. As especificações geradas através deste ambiente apresentam pouca possibilidade de erro, uma vez que são efetuados vários procedimentos de verificação das informações fornecidas. / Office Information Systems constitute special kinds of information systems - very complex socio-technical systems, with large human influence. Time is very important in the information representation, not only for explicit temporal information but also for restrictions on temporal ordering of activities to be executed and to record the temporal evolution of property values. In this work a data model to be used as a requirement specification method for office infoimations systems is presented. Specification development is a complex task. All the possible characteristics of an application, static and behavioral, shall be represented. An applications' specification is usually not a trivial task, and a big amount of time is used to develop it. Specifications are usually very complex and the possibility of verifying the correctness is an important aspect to be considered. The reuse of specifications is a way to obtain a better rate of correctness spending less time, using parts of specifications that were already validated through previous implementations. An object-oriented data model is used in this work to specify office information systems. The use of the object-oriented paradigm allows the definition of a class library containing classes identified in several specifications constructed in a specific application domain. The reuse of classes of such a library in new specifications gives efficiency to the process. To represent the dynamic characteristics of an application, such as the documents evolution within the office, it is necessary to be able to represent temporal properties. The data model used in the specification shall allow the representation of these temporal aspects not only to model data defined in a temporal domain but also to represent the objects values evolution during an objects existence. The representaion of temporal aspects is one of the main issues developed in the data model defined in this work. The data model is called TF-ORM (Temporal Fuctionality in Objects with Roles Model), and is an extention to the F-ORM (Functionality in Objects with Roles Model) model [DEA 91 a,b,c]. To this model the necessary temporal aspects were added and the basic characteristics were enlarged to better capture the particular aspects of the office habilitation systems domain, specially concerning the representation of some parts of human work. The resulting model. TF-ORM, is an object-oriented temporal data model and uses the concept of roles to represent an objects different behaviors. The possibility of retrieving information from a database specified through this data model is also considered and a query language for the TF-ORM data model is presented. Special attention is given to the retrieval of temporal information. The TFORM data model stores both the transaction and the valid time associated to dynamic properties and allows the retrieving of information fettering the databases' actual state (actually valid information), information refering the databases' past and future states (valid information in the past and information that will be valid in the future according to the actual data knowledge) and information about the databases' past history (information that was believed to be true in some moment in the past). A complete case study is presented to validate the TF-ORM data model and its efficiency as a specification method for office information systems. An environment to support specifications using TF-ORM is described. This environment uses a class library. The use of this environment allows stepwise construction of a specification, with the access to listings of the already defined parts and to the information of the class library to be reused. The contructed specifications present a small rate of errors, due to several verification procedures embedded in the environment.

Ce travail appartient au domaine de la simulation numérique sur des plates-formes d'exécution distribuées hétérogènes telles que des grilles de calcul. Ce type de plate-forme se caractérise par des possibles changements de condition d'exécution et par une probabilité importante de défaillance de certains composants. Une application qui s'exécute dans un tel environnement se doit d'être adaptable à son contexte d'exécution et tolérante aux pannes. Face à la complexité croissante de la mise en place de cas de calcul sur des grilles de calcul, nous proposons une plateforme logicielle pour la résolution de cas de calcul numérique dans un environnement distribué hétérogène. Nos travaux apportent une solution qui se base sur un système d'agents mobiles, ce qui permet à une application de s'adapter au changement de son environnement d'exécution. Dans un premier temps, nous utilisons le langage pi calcul d'ordre supérieur pour spécifier une « ferme de travailleurs » capable de participer à la résolution de tout type de cas de calcul. Ensuite, nous énonçons des propriétés qui caractérisent le bon fonctionnement de ce système avec une logique temporelle TCTL. Pour cela, nous souhaitons modéliser notre système à l'aide d'automates temporisés à partir des termes définis par la spécification formelle en pi calcul. Dans ce but, nous définissons une transformation de termes écrits en pi calcul en automates temporisés. Les propriétés sont alors vérifiées avec l'outil UppAal. Pour valider ce travail de modélisation, nous avons réalisé le framework MCA (pour Mobile Computing Architecture). Celui-ci propose un ensemble d'outils facilitant la mise en place de composants sur un environnement distribué hétérogène dans le but d'effectuer la résolution de cas de calcul. La librairie avec laquelle sont développés ces composants, qu'ils soient mobiles ou non, est implantée en Java et se base les technologies Jini et JavaSpaces. Enfin, nous réalisons l'évaluation du framework MCA en procédant à la résolution de trois cas de calcul différents. Chacune de ces expériences, réalisées sur une grappe de 20 noeuds, nous permet de montrer les caractéristiques essentielles de notre framework : une simplicité de programmation, un faible surcoût en temps d'exécution sans l'activation de la tolérance aux pannes et une tolérance aux pannes efficace / This work belongs to the domain of numerical simulation on heterogeneous distributed platforms such as grids. This type of platform is characterized by possible changes in execution conditions and a significant probability of some components failure. An application running in such an environment must be adaptable to its execution context and fault tolerant. Facing the growing complexity of implementing computation cases on grid computing, we propose a software platform which solves numerical computation cases in a distributed heterogeneous environment. Our work provides a solution based on a mobile agent system, which allows an application to adapt to change in its execution environment. At first, we use the higher-order pi calculus language to specify a « farm of workers » able to take part in solving any type of computation case. Then we set the properties that characterize the system's correct execution with a temporal logic TCTL. In order to do this, we perform a temporal modeling system based on terms defined by the formal specification in pi calculus. To achieve this transformation, we define a translation of terms written in pi calculus into timed automata. The properties are verified with the UppAal tool. To validate this modeling work, we develop the MCA (for Mobile Computing Architecture) framework. It offers a set of tools which facilitate the implementation of distributed heterogeneous components in order to solve computation cases. These components, mobile or not, are developed with a library written in Java and which uses Jini and JavaSpaces technologies. Finally, our framework is evaluated through the resolution of three different computation cases. Each of these experiments, performed on a 20 node cluster allow us to highlight our framework's main characteristics : programming simplicity, low overhead in execution time without the fault tolerance activation and efficient fault tolerance

Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.

Neste trabalho é apresentado um método de refinamento para especificações de sistemas embarcados, baseado na linguagem de especificação gráfica UML-RT e na linguagem de especificação formal CSP-OZ. A linguagem UML-RT é utilizada para descrever a arquitetura de sistemas de tempo real distribuídos e esses mapeados para uma especificação formal através de CSP-OZ. A linguagem de especificação formal CSP-OZ é a combinação da linguagem orientada a objetos Object-Z e a algebra de processos CSP, que descreve o comportamento de processos concorrentes. O método de refinamento proposto é baseado na integração de dois métodos: o de bi-simulação, para refinar a parte comportamental da especificação descrita por CSP; e o de equivalência de especificações, para refinar as estruturas de dados descritas por Object-Z, permitindo assim que características de orientação a objetos possam ser utilizadas. Com o método proposto é possível refinar especificações e, conseqüentemente, verificá-las com sua implementação. O desenvolvimento desse método é rigoroso, incluindo a definição formal para um metamodelo da UML-RT. Um exemplo detalhado é apresentado no final deste trabalho. / In this work, a method of refinement of embedded systems specifications based on the graphical specification language UML-RT and the formal specification CSP-OZ is introduced. The UML-RT is used to model real time distributed architecture systems and these are mapped onto formal specifications using CSP-OZ. The CSP-OZ formal specification language is a combination of the state-based object oriented language Object-Z and the CSP process algebra that describes behavioral models of concurrent processes. The rationale of the proposed refinement method is twofold, the use of bisimulation to refine the behavioral part and the specification matching algorithm to refine the state-based part, supporting object-oriented characteristics. Using this result, an equivalence between the specification-matching algorithm and simulation rules is showed. Using the proposed method it is possible to refine CSP-OZ specifications and verify them against their implementations. The development of the proposed refinement method is rigorous, including a formal definition for a UML-RT metamodel. A detailed study case is given at the end of this work.

Made available in DSpace on 2014-12-17T15:47:56Z (GMT). No. of bitstreams: 1 DiegoHOS_DISSERT.pdf: 2899752 bytes, checksum: d3160b774efd6749eced9bb34d4a74cf (MD5) Previous issue date: 2011-08-31 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / Using formal methods, the developer can increase software s trustiness and correctness. Furthermore, the developer can concentrate in the functional requirements of the software. However, there are many resistance in adopting this software development approach. The main reason is the scarcity of adequate, easy to use, and useful tools. Developers typically write code and test it. These tests usually consist of executing the program and checking its output against its requirements. This, however, is not always an exhaustive discipline. On the other side, using formal methods one might be able to investigate the system s properties further. Unfortunately, specification languages do not always have tools like animators or simulators, and sometimes there are no friendly Graphical User Interfaces. On the other hand, specification languages usually have a compiler which normally generates a Labeled Transition System (LTS). This work proposes an application that provides graphical animation for formal specifications using the LTS as input. The application initially supports the languages B, CSP, and Z. However, using a LTS in a specified XML format, it is possible to animate further languages. Additionally, the tool provides traces visualization, the choices the user did, in a graphical tree. The intention is to improve the comprehension of a specification by providing information about errors and animating it, as the developers do for programming languages, such as Java and C++. / Usando m?todos formais, o desenvolvedor pode aumentar a confiabilidade e corretude do software. Al?m disso, o desenvolvedor pode concentrar-se mais nos requisitos funcionais. Por?m h? muita resist?ncia em se adotar essa abordagem de desenvolvimento de software. A raz?o principal e a escassez de suporte ferramental adequado, ?til e de f?cil utiliza??o. Os desenvolvedores normalmente escrevem o c?digo e o testam. Estes testes geralmente consistem em checar se as sa?das est?o de acordo com os requisitos. Isto, contudo, nem sempre e poss?vel de maneira exaustiva. Por outro lado, usando M?todos Formais um desenvolvedor e capaz de investigar profundamente as propriedades do sistema. Infelizmente, linguagens de especifica??o formal nem sempre possuem ferramentas como animador ou simulador e ?s vezes n?o h? interfaces gr?ficas amig?veis. Por?m, algumas dessas ferramentas possuem um compilador, que gera um Sistema de Transi??es Rotuladas (LTS). A proposta deste trabalho ? desenvolver um aplicativo que fornece anima??o gr?fica para especifica??es formais usando o LTS como entrada. O aplicativo inicialmente suporta as as linguagens B, CSP e Z. Usando o LTS em um formato XML especificado ? poss?vel animar outras linguagens formais. Adicionalmente a ferramenta disponibiliza visualiza??o de traces, escolhas feitas pelo usu?rio, em um formato de ?rvore gr?fica. A inten??o ? melhorar a compreens?o de uma especifica??o, fornecendo informa??es sobre erros e animando-a, como os desenvolvedores fazem com linguagens de programa??o como Java e C++.