Structuring real-time Object-Z specifications

This paper presents a means of structuring specifications in real-time Object-Z: an integration of Object-Z with the timed refinement calculus. Incremental modification of classes using inheritance and composition of classes to form multi-component systems are examined. Two approaches to the latter are considered: using Object-Z's notion of object instantiation and introducing a parallel composition operator similar to those found in process algebras. The parallel composition operator approach is both more concise and allows more general modelling of concurrency. Its incorporation into the existing semantics of real-time Object-Z is presented.

Does Petrolisthes armatus (Anomura, Porcellanidae) form a Species Complex or Are We Dealing with Just One Widely Distributed Species?

Fernando L. Mantelatto, Leonardo G. Pileggi, Ivana Miranda, and Ingo S. Wehrtmann (2011) Does Petrolisthes armatus (Anomura, Porcellanidae) form a species complex or are we dealing with just one widely distributed species? Zoological Studies 50(3): 372-384. Petrolisthes armatus has the widest distribution known among members of the family Porcellanidae and is one of the most ubiquitous and locally abundant intertidal decapods along the Atlantic coast of the Americas. Considering its geographical distribution and morphological plasticity, several authors postulated the existence of a P. armatus species complex. In the present study we used genetic data from the mitochondrial 16S ribosomal gene to determine the genetic variability of P. armatus from selected locations within its eastern tropical Pacific and western Atlantic distributions. Our phylogenic analysis included 49 specimens represented by 26 species of the genus Petrolisthes and 16 specimens from 10 species and 4 related genera. Genetic distances estimated among the analyzed Petrolisthes species ranged from 2.6%-22.0%; varied between 0%-5.7% for 16S. Additionally, the revision of P. armatus specimens from Pacific Costa Rica and Brazilian Waters showed no geographically significant morphological variations among the analyzed specimens. Therefore, our morphological and genetic data do not support the hypothesis of a P. armatus complex within the specimens studied herein from the Americas, but convincingly confirm the monophyly and non-separateness of the members assigned as P. armatus. http://zoolstud.sinica.edu.tw/Journals/50.3/372.pdf

Approximate controllability of second-order distributed implicit functional systems

In this paper we study the approximate controllability of control systems with states and controls in Hilbert spaces, and described by a second-order semilinear abstract functional differential equation with infinite delay. Initially we establish a characterization for the approximate controllability of a second-order abstract linear system and, in the last section, we compare the approximate controllability of a semilinear abstract functional system with the approximate controllability of the associated linear system. (C) 2008 Elsevier Ltd. All rights reserved.

The Edinburgh-Cape Blue Object Survey - I. Description of the survey

The Edinburgh-Cape Blue Object Survey is a major survey to discover blue stellar objects brighter than B similar to 18 in the southern sky. It is planned to cover an area of sky of 10 000 deg(2) with \b\ > 30 degrees and delta < 0 degrees. The blue stellar objects are selected by automatic techniques from U and B pairs of UK Schmidt Telescope plates scanned with the COSMOS measuring machine. Follow-up photometry and spectroscopy are being obtained with the SAAO telescopes to classify objects brighter than B = 16.5. This paper describes the survey, the techniques used to extract the blue stellar objects, the photometric methods and accuracy, the spectroscopic classification, and the limits and completeness of the survey.

Atypical enteropathogenic Escherichia coli genomic background allows the acquisition of non-EPEC virulence factors

Atypical enteropathogenic Escherichia coli (aEPEC) has been associated with infantile diarrhea in many countries. The clonal structure of aEPEC is the object of active investigation but few works have dealt with its genetic relationship with other diarrheagenic E. coli (DEC). This study aimed to evaluate the genetic relationship of aEPEC with other DEC pathotypes. The phylogenetic relationships of DEC strains were evaluated by multilocus sequence typing. Genetic diversity was assessed by pulsed-field gel electrophoresis (PFGE). The phylogram showed that aEPEC strains were distributed in four major phylogenetic groups (A, B1, B2 and D). Cluster I ( group B1) contains the majority of the strains and other pathotypes [enteroaggregative, enterotoxigenic and enterohemorrhagic E. coli ( EHEC)]; cluster II ( group A) also contains enteroaggregative and diffusely adherent E. coli; cluster III ( group B2) has atypical and typical EPEC possessing H6 or H34 antigen; and cluster IV ( group D) contains aEPEC O55:H7 strains and EHEC O157:H7 strains. PFGE analysis confirmed that these strains encompass a great genetic diversity. These results indicate that aEPEC clonal groups have a particular genomic background - especially the strains of phylogenetic group B1 that probably made possible the acquisition and expression of virulence factors derived from non-EPEC pathotypes.

Concurreny based transition refinement for the verification of distributed algorithms

We suggest a new notion of behaviour preserving transition refinement based on partial order semantics. This notion is called transition refinement. We introduced transition refinement for elementary (low-level) Petri Nets earlier. For modelling and verifying complex distributed algorithms, high-level (Algebraic) Petri nets are usually used. In this paper, we define transition refinement for Algebraic Petri Nets. This notion is more powerful than transition refinement for elementary Petri nets because it corresponds to the simultaneous refinement of several transitions in an elementary Petri net. Transition refinement is particularly suitable for refinement steps that increase the degree of distribution of an algorithm, e.g. when synchronous communication is replaced by asynchronous message passing. We study how to prove that a replacement of a transition is a transition refinement.

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.