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.

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.

Demo: Shield UI JavaScript Chart - A Flexible HTML5 Data Visualization Component

Shield UI’s advanced framework for creating rich charts and graphs is the first of a line of data visualization components, giving web developers the power for embedding rich graphics in their web projects with minimum effort. Built with HTML, CSS3 and packaged as a jQuery plugin, the library has full support for legacy and modern desktop web browsers, as well as the latest mobile devices.

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.

Dynamic fault tree analysis with PEWMA modeling of event rates and Bayesian updating of material balance parameters using MCMC

This research explores Bayesian updating as a tool for estimating parameters probabilistically by dynamic analysis of data sequences. Two distinct Bayesian updating methodologies are assessed. The first approach focuses on Bayesian updating of failure rates for primary events in fault trees. A Poisson Exponentially Moving Average (PEWMA) model is implemnented to carry out Bayesian updating of failure rates for individual primary events in the fault tree. To provide a basis for testing of the PEWMA model, a fault tree is developed based on the Texas City Refinery incident which occurred in 2005. A qualitative fault tree analysis is then carried out to obtain a logical expression for the top event. A dynamic Fault Tree analysis is carried out by evaluating the top event probability at each Bayesian updating step by Monte Carlo sampling from posterior failure rate distributions. It is demonstrated that PEWMA modeling is advantageous over conventional conjugate Poisson-Gamma updating techniques when failure data is collected over long time spans. The second approach focuses on Bayesian updating of parameters in non-linear forward models. Specifically, the technique is applied to the hydrocarbon material balance equation. In order to test the accuracy of the implemented Bayesian updating models, a synthetic data set is developed using the Eclipse reservoir simulator. Both structured grid and MCMC sampling based solution techniques are implemented and are shown to model the synthetic data set with good accuracy. Furthermore, a graphical analysis shows that the implemented MCMC model displays good convergence properties. A case study demonstrates that Likelihood variance affects the rate at which the posterior assimilates information from the measured data sequence. Error in the measured data significantly affects the accuracy of the posterior parameter distributions. Increasing the likelihood variance mitigates random measurement errors, but casuses the overall variance of the posterior to increase. Bayesian updating is shown to be advantageous over deterministic regression techniques as it allows for incorporation of prior belief and full modeling uncertainty over the parameter ranges. As such, the Bayesian approach to estimation of parameters in the material balance equation shows utility for incorporation into reservoir engineering workflows.

Un webservice per collegare il cittadino con la propria situazione debitoria

La tesi tratta di un web service capace di estrapolare i dati da un database Oracle utilizzato da un gestionale già esistente, per darli come output ad un portale da cui il cittadino si potrà collegare, visionandoli. Il gestionale si occupa della fase coattiva, ovvero quando un contribuente non paga una multa o una qualsiasi tassa; fino ad oggi non era possibile far vedere in via telematica i dati della situazione coattiva di un contribuente. Grazie al web service da me creato un portale potrà fare vedere i dati al contribuente tramite esso. Inoltre grazie a questo web service in futuro si potranno collegare anche con altri portali o app smartphone per dare ulteriori servizi al cittadino.

Alternative per la configurazione dell'infrastruttura di rete in piattaforme Openstack

In questo scritto si analizzeranno alcune alternative nella configurazione di rete della piattaforma di cloud computing open source OpenStack. Verrà mostrata un’ installazione in ambiente di laboratorio di un cluster completo basato sulla release Liberty di Openstack, per poi modificarne la componente dedicata al Networking in modo da sfruttare diversi plugin e diversi protocolli. Si osserverà il traffico generato all’interno e verso l’esterno del sistema Openstack in modo da avere un quadro generale del comportamento dell’infrastruttura.

tuProlog su piattaforma Android: reingegnerizzazione in ottica Modern UI e fruibilità "as a service"

Questa tesi si occupa principalmente della revisione grafica in ottica Modern UI dell'app tuProlog Android, nella prospettiva di renderlo in futuro disponibile anche in modalità as-a-service. Dopo una attenta analisi preliminare dell'architettura di tuProlog in generale e in particolare della struttura dell'app tuProlog preesistente e del relativo progetto in ambiente Eclipse, ci si è focalizzati sulla riprogettazione dell'app, dall'analisi dei requisiti - ivi incluso il nuovo strumento di sviluppo da utilizzare, Android Studio - alla successiva analisi e progettazione della nuova soluzione, seguita da implementazione e collaudo.