HLA-G polymorphism and transitional cell carcinoma of the bladder in a Brazilian population

The morphologic appearance and clinical behavior of the human urinary bladder papillary transitional cell carcinoma (TCC) probably result from a complex interaction between carcinogenic insults and host resistance during the patient`s life. While the main recognized risk factors are of environmental origin (e.g. smoking), relatively little information exists about the susceptibility to TCC development. The human leukocyte antigen G (HLA-G) molecule plays an important role in immune response regulation and has been implicated in the inhibition of the cytolytic function of natural killer and cytotoxic T cells. Several lines of evidence indicate that HLA-G polymorphisms influence the expression level and production of different HLA-G isoforms. The aim of this study was to explore a possible influence of the HLA-G polymorphism on the susceptibility to urinary bladder TCC development and progression in smokers and nonsmokers Brazilian subjects. The HLA-G locus was found to be associated with susceptibility to TCC development and progression. The G*0104 allelic group (specially the G*010404 allele) and the G*0103 allele were associated with a tobacco-dependent influence on TCC development. The G*0104 group was associated with progression to high-grade tumors, irrespective of smoking habit, while the G*0103 allele was associated to high-grade tumor only in smoking patients. Our results are an evidence that the HLA-G locus itself, or as part of an extended haplotype encompassing this chromosome region (particularly the HLA-A given the high linkage disequilibrium observed between them in this data series), may be associated with TCC susceptibility and tumor progression, suggesting a tobacco-dependent influence of these polymorphisms.

The Object Management Group Ontology Definition Metamodel

Report of a submission being made to a major international software engineering standards group, the Object Management Group which ties together OMG standards with World-Wide Web Consortium and International Standards Organization standards. Major industry bodies including IBM are collaborating, and the submission has the support of 24 companies. OMG, W3C and ISO standards strongly influence the industry, especially in combination. Colomb was a major contributor, responsible for 30% of the submission, and the primary author of the paper.

MDA-based re-engineering with Object-Z

This paper describes a practical application of MDA and reverse engineering based on a domain-specific modelling language. A well defined metamodel of a domain-specific language is useful for verification and validation of associated tools. We apply this approach to SIFA, a security analysis tool. SIFA has evolved as requirements have changed, and it has no metamodel. Hence, testing SIFA’s correctness is difficult. We introduce a formal metamodelling approach to develop a well-defined metamodel of the domain. Initially, we develop a domain model in EMF by reverse engineering the SIFA implementation. Then we transform EMF to Object-Z using model transformation. Finally, we complete the Object-Z model by specifying system behavior. The outcome is a well-defined metamodel that precisely describes the domain and the security properties that it analyses. It also provides a reliable basis for testing the current SIFA implementation and forward engineering its successor.

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.

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.