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.

A comparison of low-storage strategies for spectral analysis in dissipative systems: filter diagonalisation in the Lanczos representation and harmonic inversion of the Chebychev-order-domain autocorrelation function

We compare the performance of two different low-storage filter diagonalisation (LSFD) strategies in the calculation of complex resonance energies of the HO2, radical. The first is carried out within a complex-symmetric Lanczos subspace representation [H. Zhang, S.C. Smith, Phys. Chem. Chem. Phys. 3 (2001) 2281]. The second involves harmonic inversion of a real autocorrelation function obtained via a damped Chebychev recursion [V.A. Mandelshtam, H.S. Taylor, J. Chem. Phys. 107 (1997) 6756]. We find that while the Chebychev approach has the advantage of utilizing real algebra in the time-consuming process of generating the vector recursion, the Lanczos, method (using complex vectors) requires fewer iterations, especially for low-energy part of the spectrum. The overall efficiency in calculating resonances for these two methods is comparable for this challenging system. (C) 2001 Elsevier Science B.V. All rights reserved.

Monocular and binocular distance cues: insights from visual form agnosia I (of III)

The human nervous system constructs a Euclidean representation of near (personal) space by combining multiple sources of information (cues). We investigated the cues used for the representation of personal space in a patient with visual form agnosia (DF). Our results indicated that DF relies predominantly on binocular vergence information when determining the distance of a target despite the presence of other (retinal) cues. Notably, DF was able to construct an Euclidean representation of personal space from vergence alone. This finding supports previous assertions that vergence provides the nervous system with veridical information for the construction of personal space. The results from the current study, together with those of others, suggest that: (i) the ventral stream is responsible for extracting depth and distance information from monocular retinal cues (i.e. from shading, texture, perspective) and (ii) the dorsal stream has access to binocular information (from horizontal image disparities and vergence). These results also indicate that DF was not able to use size information to gauge target distance, suggesting that intact temporal cortex is necessary for learned size to influence distance processing. Our findings further suggest that in neurologically intact humans, object information extracted in the ventral pathway is combined with the products of dorsal stream processing for guiding prehension. Finally, we studied the size-distance paradox in visual form agnosia in order to explore the cognitive use of size information. The results of this experiment were consistent with a previous suggestion that the paradox is a cognitive phenomenon.

Research commentary: Information systems and conceptual modeling - A research agenda

Within the information systems field, the task of conceptual modeling involves building a representation of selected phenomena in some domain. High-quality conceptual-modeling work is important because it facilitates early detection and correction of system development errors. It also plays an increasingly important role in activities like business process reengineering and documentation of best-practice data and process models in enterprise resource planning systems. Yet little research has been undertaken on many aspects of conceptual modeling. In this paper, we propose a framework to motivate research that addresses the following fundamental question: How can we model the world to better facilitate our developing, implementing, using, and maintaining more valuable information systems? The framework comprises four elements: conceptual-modeling grammars, conceptual-modeling methods, conceptual-modeling scripts, and conceptual-modeling contexts. We provide examples of the types of research that have already been undertaken on each element and illustrate research opportunities that exist.

Wavelet-based image segment representation

An efficient representation method for arbitrarily shaped image segments is proposed. This method includes a smart way to select wavelet basis to approximate the given image segment, with improved image quality and reduced computational load.

Expert system application on preliminary design of water retaining structures

Design of liquid retaining structures involves many decisions to be made by the designer based on rules of thumb, heuristics, judgment, code of practice and previous experience. Various design parameters to be chosen include configuration, material, loading, etc. A novice engineer may face many difficulties in the design process. Recent developments in artificial intelligence and emerging field of knowledge-based system (KBS) have made widespread applications in different fields. However, no attempt has been made to apply this intelligent system to the design of liquid retaining structures. The objective of this study is, thus, to develop a KBS that has the ability to assist engineers in the preliminary design of liquid retaining structures. Moreover, it can provide expert advice to the user in selection of design criteria, design parameters and optimum configuration based on minimum cost. The development of a prototype KBS for the design of liquid retaining structures (LIQUID), using blackboard architecture with hybrid knowledge representation techniques including production rule system and object-oriented approach, is presented in this paper. An expert system shell, Visual Rule Studio, is employed to facilitate the development of this prototype system. (C) 2002 Elsevier Science Ltd. All rights reserved.

Structural refinement of systems specified in object-z and CSP

This paper is concerned with methods for refinement of specifications written using a combination of Object-Z and CSP. Such a combination has proved to be a suitable vehicle for specifying complex systems which involve state and behaviour, and several proposals exist for integrating these two languages. The basis of the integration in this paper is a semantics of Object-Z classes identical to CSP processes. This allows classes specified in Object-Z to be combined using CSP operators. It has been shown that this semantic model allows state-based refinement relations to be used on the Object-Z components in an integrated Object-Z/CSP specification. However, the current refinement methodology does not allow the structure of a specification to be changed in a refinement, whereas a full methodology would, for example, allow concurrency to be introduced during the development life-cycle. In this paper, we tackle these concerns and discuss refinements of specifications written using Object-Z and CSP where we change the structure of the specification when performing the refinement. In particular, we develop a set of structural simulation rules which allow single components to be refined to more complex specifications involving CSP operators. The soundness of these rules is verified against the common semantic model and they are illustrated via a number of examples.

“Somos ensinados a pensar em sexo”: Representações Sociais de Masculinidades e de Amor em Travestis Homens Gays e Homens Heterossexuais

Estudos realizados no campo das masculinidades mostraram que a adesão e identificação de determinados grupos a um conjunto de regras e comportamentos que definem o ser homem implicava em adoecimento e submissão a um regime que supostamente lhes oferece vantagens e poder. Compreender como diferentes grupos constituem-se em relação à divisão social sexual torna-se relevante principalmente se considerarmos sujeitos que fogem ao padrão que define modos de ser homem e ser mulher. Esta tese objetivou investigar as representações sociais de masculinidades e de amor de sujeitos com identidades de gênero e orientações sexuais diversas, especificamente: identificar e analisar representações sociais de masculinidade e amor de travestis, homens gays e homens heterossexuais; apreender experiências de preconceito e discriminação vividas em função da identidade de gênero e orientações sexuais. A pesquisa foi realizada em duas etapas: entrevistas semiestruturadas com 21 travestis; aplicação de questionários com questões abertas e fechadas em 52 homens gays, 40 homens heterossexuais e 39 travestis. Os dados coletados na primeira etapa foram submetidos aos procedimentos da análise de conteúdo categorial temática. O tratamento dos dados coletados na segunda etapa foi realizado através do software ALCESTE. Os homens heterossexuais representam a masculinidade a partir de uma perspectiva evolutiva, ancorada no discurso biológico e científico que descarta as influências da cultura na constituição dos sexos e identidades de gênero. Nos homens gays encontramos aproximações das representações dos sujeitos ao modelo da masculinidade hegemônica fortemente identificada à imagem do homem heterossexual, bem como elementos que ora apresentam aproximações, ora distanciamentos desse padrão. As travestis também utilizam elementos da ideia de masculinidade hegemônica para construção desta representação, objetivando-a na construção do modelo do homem forte e viril, sobre o qual não se identificam mas direcionam seu desejo. Os três grupos representam o amor como elemento estranho à masculinidade, posto que este é objeto que pertence à feminilidade. O amor distancia-se da construção da representação social de masculinidade de homens heterossexuais, é elemento estranho e conflituoso às representações dos homens gays e valor que corresponde a uma ética para o grupo de travestis. Nesse contexto, as experiências de preconceito e discriminação pouco modificam a elaboração das representações de heterossexuais; influenciam fortemente a construção da imagem de homem e mulher por onde homens gays e travestis alimentam suas identificações. Concluímos apostando na defesa da emergência de práticas e identidades sexo-diversas como artifícios potentes à desestabilização do padrão da dominação masculina para determinação de sexos e identidades.

Metodologia de representação identitária do patrimônio territorial : a água como elemento de identidade em Linhares/ES

Apresenta primeiramente o conceito de desenvolvimento local autossustentável dentro do enfoque territorialista. Mostra também o conceito de patrimônio territorial e o de representação identitária do território como instrumento de preservação do patrimônio, neste caso o territorial. O enfoque territorialista é adotado como base teórica para a construção do roteiro metodológico de representação identitária do território com vistas à preservação do patrimônio tendo como objeto empírico o município de Linhares/ES, que passa por um processo de intenso desenvolvimento de seu território e que apresenta um rico patrimônio, no que diz respeito aos recursos naturais, em especial o hídrico. Nos últimos anos tem-se registrado um crescimento forte dos instrumentos disponíveis para a produção de imagens do território, neste caso o uso da tecnologia de Sistemas de Informações Geográficas. Por meio deste recurso, adotado na Escola Territorialista Italiana, representa-se o patrimônio que constitui o território municipal, tendo como produtos finais o Atlas do patrimônio territorial no município de Linhares/ES e o Roteiro metodológico de representação identitária do patrimônio territorial.