A tool for a formal pattern modeling language

This paper presents a formal but practical approach for defining and using design patterns. Initially we formalize the concepts commonly used in defining design patterns using Object-Z. We also formalize consistency constraints that must be satisfied when a pattern is deployed in a design model. Then we implement the pattern modeling language and its consistency constraints using an existing modeling framework, EMF, and incorporate the implementation as plug-ins to the Eclipse modeling environment. While the language is defined formally in terms of Object-Z definitions, the language is implemented in a practical environment. Using the plug-ins, users can develop precise pattern descriptions without knowing the underlying formalism, and can use the tool to check the validity of the pattern descriptions and pattern usage in design models. In this work, formalism brings precision to the pattern language definition and its implementation brings practicability to our pattern-based modeling approach.

A patttern based model evolution approach

In this paper, we present a framework for pattern-based model evolution approaches in the MDA context. In the framework, users define patterns using a pattern modeling language that is designed to describe software design patterns, and they can use the patterns as rules to evolve their model. In the framework, design model evolution takes place via two steps. The first step is a binding process of selecting a pattern and defining where and how to apply the pattern in the model. The second step is an automatic model transformation that actually evolves the model according to the binding information and the pattern rule. The pattern modeling language is defined in terms of a MOF-based role metamodel, and implemented using an existing modeling framework, EMF, and incorporated as a plugin to the Eclipse modeling environment. The model evolution process is also implemented as an Eclipse plugin. With these two plugins, we provide an integrated framework where defining and validating patterns, and model evolution based on patterns can take place in a single modeling environment.

Verifying metamodel coverage of model transformations

Since the object management group (OMG) commenced its model driven architecture (MDA) initiative, there has been considerable activity proposing and building automatic model transformation systems to help implement the MDA concept. Much less attention has been given to the need to ensure that model transformations generate the intended results. This paper explores one aspect of validation and verification for MDA: coverage of the source and/or target metamodels by a set of model transformations. The paper defines the property of metamodel coverage and some corresponding algorithms. This property helps the user assess which parts of a source (or target) metamodel are referenced by a given model transformation set. Some results are presented from a prototype implementation that is built on the eclipse modeling framework (EMF).

Satellite laser ranging and the ETALON Geodetic satellites

The technique of Satellite Laser Ranging is today a mature, important tool with applications in many area of geodynamics, geodesy and satellite dynamics. A global network of some 40 stations regularly obtains range observations with sub-cm precision to more than twelve orbiting spacecraft. At such levels of precision it is important to minimise potential sources of range bias in the observations, and part of the thesis is a study of subtle effects caused by the extended nature of the arrays of retro-reflectors on the satellites. We develop models that give a precise correction of the range measurements to the centres of mass of the geodetic satellites Lageos and Etalon, appropriate to a variety of different ranging systems, and use the Etalon values, which were not determined during pre-launch tests, in an extended orbital analysis. We have fitted continuous 2.5 year orbits to range observations of the Etalons from the global network of stations, and analysed the results by mapping the range residuals from these orbits into equivalent corrections to orbital elements over short time intervals. From these residuals we have detected and studied large un-modelled along-track accelerations associated with periods during which the satellites are undergoing eclipse by the Earth's shadow. We also find that the eccentricity residuals are significantly different for the two satellites, with Etalon-2 undergoing a year-long eccentricity anomaly similar in character to that experienced at intervals by Lageos-1. The nodal residuals show that the satellites define a very stable reference frame for Earth rotation determination, with very little drift-off during the 2.5 year period. We show that an analysis of more than about eight years of tracking data would be required to derive a significant value for 2. The reference frame defined by the station coordinates derived from the analyses shows very good agreement with that of ITRF93.

The measurement properties of the menorrhagia multi-attribute quality-of-life scale:a psychometric analysis

Menorrhagia, or heavy menstrual bleeding (HMB), is a common gynaecological condition. As the aim of treatment is to improve women's wellbeing and quality of life (QoL), it is necessary to have effective ways to measure this. This study investigated the reliability and validity of the menorrhagia multi-attribute scale (MMAS), a menorrhagia-specific QoL instrument. Participants (n = 431) completed the MMAS and a battery of other tests as part of the baseline assessment of the ECLIPSE (Effectiveness and Cost-effectiveness of Levonorgestrel-containing Intrauterine system in Primary care against Standard trEatment for menorrhagia) trial. Analyses of their responses suggest that the MMAS has good measurement properties and is therefore an appropriate condition-specific instrument to measure the outcome of treatment for HMB. © 2011 The Authors BJOG An International Journal of Obstetrics and Gynaecology © 2011 RCOG.

Levonorgestrel intrauterine system versus medical therapy for menorrhagia

Background - Menorrhagia is a common problem, yet evidence to inform decisions about therapy is limited. In a pragmatic, multicenter, randomized trial, we compared the levonorgestrel-releasing intrauterine system (levonorgestrel-IUS) with usual medical treatment in women with menorrhagia who presented to their primary care providers. Methods - We randomly assigned 571 women with menorrhagia to treatment with levonorgestrel-IUS or usual medical treatment (tranexamic acid, mefenamic acid, combined estrogen–progestogen, or progesterone alone). The primary outcome was the patient-reported score on the Menorrhagia Multi-Attribute Scale (MMAS) (ranging from 0 to 100, with lower scores indicating greater severity), assessed over a 2-year period. Secondary outcomes included general quality-of-life and sexual-activity scores and surgical intervention. Results - MMAS scores improved from baseline to 6 months in both the levonorgestrel-IUS group and the usual-treatment group (mean increase, 32.7 and 21.4 points, respectively; P<0.001 for both comparisons). The improvements were maintained over a 2-year period but were significantly greater in the levonorgestrel-IUS group than in the usual-treatment group (mean between-group difference, 13.4 points; 95% confidence interval, 9.9 to 16.9; P<0.001). Improvements in all MMAS domains (practical difficulties, social life, family life, work and daily routine, psychological well-being, and physical health) were significantly greater in the levonorgestrel-IUS group than in the usual-treatment group, and this was also true for seven of the eight quality-of-life domains. At 2 years, more of the women were still using the levonorgestrel-IUS than were undergoing the usual medical treatment (64% vs. 38%, P<0.001). There were no significant between-group differences in the rates of surgical intervention or sexual-activity scores. There were no significant differences in serious adverse events between groups. Conclusions - In women with menorrhagia who presented to primary care providers, the levonorgestrel-IUS was more effective than usual medical treatment in reducing the effect of heavy menstrual bleeding on quality of life. (Funded by the National Institute of Health Research Health Technology Assessment Programme; ECLIPSE Controlled-Trials.com number, ISRCTN86566246.)

INFRAWEBS Axiom Editor – A Graphical Ontology-Driven Tool for Creating Complex Logical Expressions

The current INFRAWEBS European research project aims at developing ICT framework enabling software and service providers to generate and establish open and extensible development platforms for Web Service applications. One of the concrete project objectives is developing a full-life-cycle software toolset for creating and maintaining Semantic Web Services (SWSs) supporting specific applications based on Web Service Modelling Ontology (WSMO) framework. According to WSMO, functional and behavioural descriptions of a SWS may be represented by means of complex logical expressions (axioms). The paper describes a specialized userfriendly tool for constructing and editing such axioms – INFRAWEBS Axiom Editor. After discussing the main design principles of the Editor, its functional architecture is briefly presented. The tool is implemented in Eclipse Graphical Environment Framework and Eclipse Rich Client Platform.

UBVRI Photometric Analysis of the Solar-Type Eclipsing Binary TYC 3034-299-1

TYC 3034-0299-1 (CVn) is a magnetically active, contact binary, ROTSE variable. UBVRcIc light curves are presented along with a period study and a simultaneous UBVRI light curve solution. Our light curves show eclipse amplitudes of 0.72 and 0.62 mags (V) in the primary and secondary eclipses. Modeled results include a dark spot region, found at longitude 51°, a 24% Roche lobe fill-out, and a mass ratio of 0.48. A total eclipse is found to occur in the secondary eclipse making TYC 3034-0299-1 a W-type (less massive star is hotter) W UMa variable.

Modelagem e simulação da solubilidade de sais em sistemas aquosos com Monoetilenoglicol

Primary processing of natural gas platforms as Mexilhão Field (PMXL-1 ) in the Santos Basin, where monoethylene glycol (MEG) has been used to inhibit the formation of hydrates, present operational problems caused by salt scale in the recovery unit of MEG. Bibliographic search and data analysis of salt solubility in mixed solvents, namely water and MEG, indicate that experimental reports are available to a relatively restricted number of ionic species present in the produced water, such as NaCl and KCl. The aim of this study was to develop a method for calculating of salt solubilities in mixed solvent mixtures, in explantion, NaCl or KCl in aqueous mixtures of MEG. The method of calculating extend the Pitzer model, with the approach Lorimer, for aqueous systems containing a salt and another solvent (MEG). Python language in the Integrated Development Environment (IDE) Eclipse was used in the creation of the computational applications. The results indicate the feasibility of the proposed calculation method for a systematic series of salt (NaCl or KCl) solubility data in aqueous mixtures of MEG at various temperatures. Moreover, the application of the developed tool in Python has proven to be suitable for parameter estimation and simulation purposes

Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.