Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP

This paper presents a method of formally specifying, refining and verifying concurrent systems which uses the object-oriented state-based specification language Object-Z together with the process algebra CSP. Object-Z provides a convenient way of modelling complex data structures needed to define the component processes of such systems, and CSP enables the concise specification of process interactions. The basis of the integration is a semantics of Object-Z classes identical to that of CSP processes. This allows classes specified in Object-Z to he used directly within the CSP part of the specification. In addition to specification, we also discuss refinement and verification in this model. The common semantic basis enables a unified method of refinement to be used, based upon CSP refinement. To enable state-based techniques to be used fur the Object-Z components of a specification we develop state-based refinement relations which are sound and complete with respect to CSP refinement. In addition, a verification method for static and dynamic properties is presented. The method allows us to verify properties of the CSP system specification in terms of its component Object-Z classes by using the laws of the the CSP operators together with the logic for Object-Z.

Model specification tests in nonparametric stochastic regression models

In this paper, we consider testing for additivity in a class of nonparametric stochastic regression models. Two test statistics are constructed and their asymptotic distributions are established. We also conduct a small sample study for one of the test statistics through a simulated example. (C) 2002 Elsevier Science (USA).

On the specification of a component repository

The lack of a commonly accepted de nition of a software component, the proliferation of competing `standards' and component frameworks, is here to stay, raising the fundamental question in component-based development of how to cope in practice with heterogeneity. This paper reports on the design of a Component Repository aimed to give at least a partial answer to the above question. The repository was fully speci ed in Vdm and a working prototype is currently being used in an industrial environment

Staphylococcus aureus na boca e no nariz de indivíduos sãos: verificação de identidade entre as cepas isoladas

Material colhido do nariz e da boca (saliva e raspado lingual, isoladamente) de 130 indivíduos clinicamente sadios, permitiu caracterizar 47 (36,15%) deles como portadores de S. aureus, sendo 21 portadores exclusivamente bucais e 31 exclusivamente nasais. Tendo sido constatado que o nariz e a boca albergam cepas de diferentes fagotipos, foi verificado que a colheita simultânea de material de dois nichos distintos (saliva e língua, nariz e língua e nariz e saliva) proporcionava a determinação de maior número de portadores. Foi recomendado que, na detecção de portadores de S. aureus, os isolamentos devem ser feitos a partir de materiais colhidos simultaneamente das áreas nasal e bucal (saliva ou língua).

Observação sobre o padrão fágico de cepas de Staphylococcus aureus isoladas da boca e do nariz de indivíduos sãos

Foram analisadas 68 cepas de Staphylococcus aureus isoladas da boca (saliva e língua) e nariz de portadores assintomáticos que albergavam essa bactéria nos três nichos, simultaneamente. Embora os três nichos apresentassem equivalência quanto ao percentual de isolamentos, foi constatado que as cepas isoladas do nariz diferiam, quanto ao seu padrão fágico, principalmente daquelas isoladas da língua. No primeiro caso, as cepas apresentaram-se mais sensíveis aos fagos do grupo I enquanto que, as isoladas do segundo nicho, foram mais sensíveis aos fagos do grupo III. Considerando estas observações é recomendável, quando da detecção de portadores de Staphylococcus aureus, a pesquisa dessa bactéria em material colhido do nariz e da boca, simultaneamente.

Plano de Comunicação SOS Animal – Grupo de Socorro Animal de Portugal

Dissertação apresentada à Escola Superior de Comunicação Social para obtenção de grau de mestre em Publicidade e Marketing.

Specification of software architecture reconfiguration

In the past years, Software Architecture has attracted increased attention by academia and industry as the unifying concept to structure the design of complex systems. One particular research area deals with the possibility of reconfiguring architectures to adapt the systems they describe to new requirements. Reconfiguration amounts to adding and removing components and connections, and may have to occur without stopping the execution of the system being reconfigured. This work contributes to the formal description of such a process. Taking as a premise that a single formalism hardly ever satisfies all requirements in every situation, we present three approaches, each one with its own assumptions about the systems it can be applied to and with different advantages and disadvantages. Each approach is based on work of other researchers and has the aesthetic concern of changing as little as possible the original formalism, keeping its spirit. The first approach shows how a given reconfiguration can be specified in the same manner as the system it is applied to and in a way to be efficiently executed. The second approach explores the Chemical Abstract Machine, a formalism for rewriting multisets of terms, to describe architectures, computations, and reconfigurations in a uniform way. The last approach uses a UNITY-like parallel programming design language to describe computations, represents architectures by diagrams in the sense of Category Theory, and specifies reconfigurations by graph transformation rules.

Model driven development implementation of a control systems user interfaces specification tool

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Engenharia Informática

Adaption of the Creative Commons approach and the roaming concept to spatial data infrastructures (SDI)

Dissertation submitted in partial fulfilment of the requirements for the Degree of Master of Science in Geospatial Technologies

A contribution to the e-framework: a specification of a programming exercise evaluation service

This work is a contribution to the e-Framework, arguably the most prominent e-learning framework today, and consists of the definition of a service for the automatic evaluation of programming exercises. This evaluation domain differs from trivial evaluations modelled by languages such as the IMS Question & Test Interoperability (QTI) specification. Complex evaluation domains justify the development of specialized evaluators that participate in several business processes. These business processes can combine other type of systems such as Programming Contest Management Systems, Learning Management Systems, Integrated Development Environments and Learning Object Repositories where programming exercises are stored as Learning Objects. This contribution describes the implementation approaches used, more precisely, behaviours & requests, use & interactions, applicable standards, interface definition and usage scenarios.

Multilingual ontology specification: a collaborative approach

19-22 June 2012 Madrid, Spain

Hox genes control the specification of global vertebral domains

Dissertação apresentada para obtenção do grau de doutor em Biologia pelo Instituto de Tecnologia Química e Biológica da Universidade Nova de Lisboa

Adding SOS Core & transactional profiles support to a web thin client

Dissertation submitted in partial fulfillment of the requirements for the Degree of Master of Science in Geospatial Technologies.

Specification of a partial replication protocol with TLA+

Nowadays, data available and used by companies is growing very fast creating the need to use and manage this data in the most efficient way. To this end, data is replicated overmultiple datacenters and use different replication protocols, according to their needs, like more availability or stronger consistency level. The costs associated with full data replication can be very high, and most of the times, full replication is not needed since information can be logically partitioned. Another problem, is that by using datacenters to store and process information clients become heavily dependent on them. We propose a partial replication protocol called ParTree, which replicates data to clients, and organizes clients in a hierarchy, using communication between them to propagate information. This solution addresses some of these problems, namely by supporting partial data replication and offline execution mode. Given the complexity of the protocol, the use of formal verification is crucial to ensure the protocol two correctness properties: causal consistency and preservation of data. The use of TLA+ language and tools to formally specificity and verify the proposed protocol are also described.