A especificação abstrata de tipos de dados, a hoje um dos conceitos mais importantes, aceitos e compreendidos da Ciência da Computação, que permite descrever as principais entidades de um sistema baseado em computador através das propriedades que tais entidades devem satisfazer. Isto a feito usando métodos e linguagens algébricos, onde as propriedades são definidas na forma de axiomas (equações). Por outro lado, a tecnologia chamada de Orientada a Objetos (00), foi se transformando em uma disciplina amadurecida para projetos e implementações de aplicações de software. Atualmente esta tecnologia inclui muitas metodologias e muitas linguagens que abrangem todo o processo de desenvolvimento de sistemas, porem, a maioria delas são influenciadas pela implementação de tais sistemas, isto e, os conceitos básicos 00 de classe, objeto e herança são definidos em fungi° da linguagem de implementação a ser usada. Alem disso, notamos que nos últimos anos esta sendo desenvolvida muita pesquisa sobre uma geração de computadores que envolvem massivamente arquiteturas paralelas (computação concorrente), bem como sobre sistemas de comunicação de dados e engenharia (descrição) de protocolos. O objetivo principal desta tese a dar uma resposta a estes três assuntos integrando três conceitos básicos da Engenharia de Software: Especificação Algébrica, Orientação a Objetos e Especificação de Processos e Concorrência, em uma Única abordagem expressa através de uma Linguagem de Especificação Formal, chamada LOP. Esta linguagem a de natureza algébrica, com destaque para a semântica baseada em teorias em lógica de primeira ordem e na construção incremental de especificações baseada em bibliotecas. / The abstract specification of data types, one of the most important concepts accepted and understood of the Computer Science, allows to describe the the main entities of a based-computer system through the properties that these entities should be to satisfy. This is made using algebraic methods and languages, where the properties are defined as axioms (equations). By other hand, the technology called Object-Oriented (00), it has been transformed in a mature discipline for Design and Implementations of software applications. At present, this technology include many methodologies and many languages for the totality of the system development process. But the majority are influenced by the implementation of such systems, i.e., the basic concepts 00 of class, object and inheritance are defined in accordance with the programming language to be used. Moreover, we noted that the last years are being developed many research on a computer generation that involve massively parallel architectures (concurrent computing) as well as on data communication systems and protocol engineering (description). The main objective of this thesis is to give an answer to these three subjects integrating three basic concepts of Software Engineering: Algebraic Specification, Object Orientation and Processes and Concurrency specification, in an unique approach expressed through a language of formal specification, called LOP. This language has algebraic nature with prominence to the semantics based on theories in first-order logic with equality and the incremental construction of library-based specifications.

A especificação abstrata de tipos de dados, a hoje um dos conceitos mais importantes, aceitos e compreendidos da Ciência da Computação, que permite descrever as principais entidades de um sistema baseado em computador através das propriedades que tais entidades devem satisfazer. Isto a feito usando métodos e linguagens algébricos, onde as propriedades são definidas na forma de axiomas (equações). Por outro lado, a tecnologia chamada de Orientada a Objetos (00), foi se transformando em uma disciplina amadurecida para projetos e implementações de aplicações de software. Atualmente esta tecnologia inclui muitas metodologias e muitas linguagens que abrangem todo o processo de desenvolvimento de sistemas, porem, a maioria delas são influenciadas pela implementação de tais sistemas, isto e, os conceitos básicos 00 de classe, objeto e herança são definidos em fungi° da linguagem de implementação a ser usada. Alem disso, notamos que nos últimos anos esta sendo desenvolvida muita pesquisa sobre uma geração de computadores que envolvem massivamente arquiteturas paralelas (computação concorrente), bem como sobre sistemas de comunicação de dados e engenharia (descrição) de protocolos. O objetivo principal desta tese a dar uma resposta a estes três assuntos integrando três conceitos básicos da Engenharia de Software: Especificação Algébrica, Orientação a Objetos e Especificação de Processos e Concorrência, em uma Única abordagem expressa através de uma Linguagem de Especificação Formal, chamada LOP. Esta linguagem a de natureza algébrica, com destaque para a semântica baseada em teorias em lógica de primeira ordem e na construção incremental de especificações baseada em bibliotecas. / The abstract specification of data types, one of the most important concepts accepted and understood of the Computer Science, allows to describe the the main entities of a based-computer system through the properties that these entities should be to satisfy. This is made using algebraic methods and languages, where the properties are defined as axioms (equations). By other hand, the technology called Object-Oriented (00), it has been transformed in a mature discipline for Design and Implementations of software applications. At present, this technology include many methodologies and many languages for the totality of the system development process. But the majority are influenced by the implementation of such systems, i.e., the basic concepts 00 of class, object and inheritance are defined in accordance with the programming language to be used. Moreover, we noted that the last years are being developed many research on a computer generation that involve massively parallel architectures (concurrent computing) as well as on data communication systems and protocol engineering (description). The main objective of this thesis is to give an answer to these three subjects integrating three basic concepts of Software Engineering: Algebraic Specification, Object Orientation and Processes and Concurrency specification, in an unique approach expressed through a language of formal specification, called LOP. This language has algebraic nature with prominence to the semantics based on theories in first-order logic with equality and the incremental construction of library-based specifications.

In this thesis, we develop and evaluate a formal model and contracting framework for data-centric Web services. The central component of our framework is a formal specification of a common Create-Read-Update-Delete (CRUD) data store. We show how this model can be used in the formal specification and verification of both basic and transactional Web service compositions. We demonstrate through both formal proofs and empirical evaluations that our proposed framework significantly decreases ambiguity about a service, enhances its reuse, and facilitates detection of errors in service-based implementations. Web Services are reusable software components that make use of standardized interfaces to enable loosely-coupled business-to-business and customer-to-business interactions over the Web. In such environments, service consumers depend heavily on the service interface specification to discover, invoke, and synthesize services over the Web. Data-centric Web services are services whose behavior is determined by their interactions with a repository of stored data. A major challenge in this domain is interpreting the data that must be marshaled between consumer and producer systems. While the Web Services Description Language (WSDL) is currently the de facto standard for Web services, it only specifies a service operation in terms of its syntactical inputs and outputs; it does not provide a means for specifying the underlying data model, nor does it specify how a service invocation affects the data. The lack of data specification potentially leads to erroneous use of the service by a consumer. In this work, we propose a formal contract for data-centric Web services. The goal is to formally and unambiguously specify the service behavior in terms of its underlying data model and data interactions. We address the specification of a single service, a flow of services interacting with a single data store, and also the specification of distributed transactions involving multiple Web services interacting with different autonomous data stores. We use the proposed formal contract to decrease ambiguity about a service behavior, to fully verify a composition of services, and to guarantee correctness and data integrity properties within a transactional composition of services. / Ph. D.

The use of third-party components is helpful while writing complex software systems, but it can be difficult to debug software that interacts with third-party components. To address this problem, a mechanism for determining if one is using the component correctly would be beneficial. Reading component documentation may or may not help, depending on its clarity and precision. A formally specified contract for that component would be better, and would also allow run-time contract verification via assertions. The client of the component could enable these assertions during development and debugging, and then disable them for the final production release to increase performance. This thesis presents nContract, a tool that provides configurable run-time contract verification without requiring component recompilation or source code access. nContract allows component developers to formally specify .NET components using attributes. This contract information is retrieved from the compiled component's metadata and a subclass is generated for each formally specified type. All members of the component's interface are overridden and contract assertions are wrapped around calls to the base class. As long as the component client uses a factory to create instances of the component's types, the decision of whether or not to create assertion-checked or unchecked objects can be deferred until run-time. / Master of Science

Despite advancements in requirements generation models, methods and tools, low quality requirements are still being produced. One potential avenue for addressing this problem is to provide the requirements engineer with an interactive environment that leads (or guides) him/her through a structured set of integrated activities that foster "good" quality requirements. While that is our ultimate goal, a necessary first step in developing such an environment is to create a formal specification mechanism for characterizing the structure, process flow and activities inherent to the requirements generation process. In turn, such specifications can serve as a basis for developing an interactive environment supporting requirements engineering. Reflecting the above need, we have developed a markup language, the Requirements Generation Markup Language (RGML), which can be used to characterize a requirements generation process. The RGML can describe process structure, flow of control, and individual activities. Within activities, the RGML supports the characterization of application instantiation, the use of templates and the production of artifacts. The RGML can also describe temporal control within a process as well as conditional expressions that control if and when various activity scenarios will be executed. The language is expressively powerful, yet flexible in its characterization capabilities, and thereby, provides the capability to describe a wide spectrum of different requirements generation processes. / Master of Science

La sécurité des systèmes d'information devient un enjeu préoccupant pour les organisations tant publiques que privées, car de tels systèmes sont pour la plupart universellement accessibles à partir de navigateurs Web. Parmi tous les aspects liés à la sécurité des systèmes d'information, c'est celui de la sécurité fonctionnelle qui est étudié dans cette thèse sous l'angle de la mise en œuvre de politiques de contrôle d'accès dans une architecture orientée services. L'élément de base de la solution proposée est un modèle générique qui introduit les concepts essentiels pour la conception de gestionnaires d'exécution de politiques de contrôle d'accès et qui établit une séparation nette entre le système d'information et les mécanismes de contrôle d'accès. L'instanciation de ce modèle conduit à un cadre d'applications qui comporte, entre autres, un filtre de contrôle d'accès dynamique. Cette thèse présente également deux méthodes systématiques d'implémentation de ce filtre à partir de politiques écrites en ASTD, une notation graphique formelle basée sur les statecharts augmentés d'opérateurs d'une algèbre de processus. La notation ASTD est plus expressive que la norme RBAC et ses extensions, la solution actuellement privilégiée dans l'industrie. La première méthode repose sur une transformation de politiques de contrôle d'accès, instanciées à partir de patrons de base exprimés en ASTD, en des processus BPEL. La deuxième méthode est basée sur une interprétation de spécifications ASTD par des processus BPEL. Dans les deux cas, les processus BPEL s'exécutent dans un moteur d'exécution BPEL et interagissent avec le système d'information. Ces deux méthodes permettent une implémentation automatique d'un cadre d'applications à partir de la spécification de départ. Finalement, un prototype a été réalisé pour chacune des deux méthodes afin de montrer leur faisabilité au niveau fonctionnel et de comparer leurs performances au niveau système / Nowadays information systems are, more than ever, available through Web browsers. Therefore, they become vulnerable against attack, which has made security an important issue for public and private organizations. This thesis examines in depth one aspect of information system security, namely functional security through access-control policy enforcement, when such systems are implemented in a service-oriented architecture framework. The foundation of the proposed solution is a generic model that introduces essential concepts to design enforcement managers for access-control policies and clearly separates responsibilities between the information system and access control mechanisms. Instantiation of this model results in a general framework, which encompasses many components including a dynamic access-control filter. This thesis also presents two systematic implementation methods for the dynamic access-control filter from policies expressed in ASTD, a formal and graphical notation based on statecharts enriched with process algebra operators. The ASTD notation is more expressive than the RBAC standard and its extensions, the widely used solution in software engineering. The first method is based on the transformation of access-control policies, instantiated from ASTD patterns, into BPEL processes. The second method is based on the interpretation of ASTD specifications by BPEL processes. In these two cases, the BPEL processes are deployed and executed in a BPEL engine, and interact with the information system. Both methods allow for automatic implementation of an enforcement framework from the initial specification. Finally, prototypes have been developed to illustrate both methods and show their feasibility at the functional level and their performance

No description available.

This paper considers four approaches to ordinal predictors in linear regression to evaluate how these contrast with respect to predictive accuracy. The two most typical treatments, namely, dummy coding and classic linear regression on assigned level scores are compared with two improved methods; penalized smoothed coefficients and a generalized additive model with cubic splines. A simulation study is conducted to assess all on the basis of predictive performance. Our results show that the dummy based methods surpass the numeric at low sample sizes. Although, as sample size increases, differences between the methods diminish. Tendencies of overfitting are identified among the dummy methods. We conclude by stating that the choice of method not only ought to be context driven, but done in the light of all characteristics.

Spatial interaction models represent a class of models that are used for modeling origin destination flow data. The interest in such models is motivated by the need to understand and explain the flows of tangible entities such as persons or commodities or intangible ones such as capital, information or knowledge between regions. The focus here is on the log-normal version of the model. In this context, we consider spatial econometric specifications that can be used to accommodate two types of dependence scenarios, one involving endogenous interaction and the other exogenous interaction. These model specifications replace the conventional assumption of independence between origin-destination-flows with formal approaches that allow for two different types of spatial dependence in flow magnitudes. (authors' abstract) / Series: Working Papers in Regional Science

O constante aumento da velocidade de processamento, devido principalmente à utilização de um número cada vez maior de processadores, tem propiciado grandes avanços no projeto e na construção de sistemas computacionais paralelos. Entretanto o desempenho de muitas aplicações é afetado pela latência das operações de Entrada e Saída de dados. Para solucionar esse problema, sistemas de arquivos paralelos, que oferecem acesso paralelo aos dados armazenados em diversos discos, vêm sendo desenvolvidos. O desenvolvimento desses sistemas complexos pode ser beneficiado pela adoção de Técnicas de Descrição Formal (TDFs), durante as fases de projeto e especificação dos mesmos, as quais podem ser aliadas a técnicas de implementação durante as demais fases. Neste sentido, este projeto propõe uma abordagem baseada em frameworks e na TDF Extended State Transition Language (Estelle), para a especificação formal, validação, implementação e teste de sistemas dessa categoria. Um framework conceitual que descreve um sistema funcional é apresentado, e dois estudos de caso são desenvolvidos dando origem a dois sistemas de arquivos derivados do framework. Uma metodologia para a validação, que usa ferramentas de simulação, é apresentada. Um dos estudos de caso é implementado semi-automaticamente, a partir de sua especificação formal Estelle, e comparações de desempenho com o mesmo sistema implementado manualmente são realizadas. / The constant increase of processing speed, mainly due to the use of a large number of processors, has allowed an improvement in the design and building of parallel computation systems. However, the performance of several types of applications is affected by the latency originated from Input/Output operations on data. In order to solve this problem parallel file systems, which allow parallel access to the data stored on a set of discs, have been developed. The design of such complex systems can benefit from the adoption of implementation techniques allied with Formal Description Techniques (FDTs). Aimed to introduce the use of FDTs in the development cycle of distributed parallel file systems, this work proposes an approach, based on framework and the FDT Extended State Transition Language (Estelle), for the formal specification, validation, implementation and testing of systems belonging to this domain. A conceptual framework that describes a basic functional system is presented, and two case studies are developed from it. A methodology for Estelle specification validation that makes use of simulation tools is also proposed in this work. One of the systems, developed as a case study, is semi-automatically implemented from its Estelle formal specification, and performance comparisons with a hand-coded implementation of the same system are done.