Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.

Convergence and divergence in global economy and social development : global perspectives on the contents of economic and soical development policy and its effects on rich and poor countries

The study of convergence and divergence in global economy and social development utilises comparative indicators to investigate the contents of economic and social development policy and their effects on the global samples that represent the rich industrial, semi-industrial and the poor developing nations. The study searchesfor answers to questions such as "what are the objectives of economic growth policies in globalisation under the imperatives of convergence and divergence, and how do these affect human well-being in consideration to the objectives of social policy in various nations?" The empirical verification of data utilises the concepts of the `logic of industrialism´ for comparative analysis that focuses mainly on identifying the levels of well-being in world nations after the Second World War. The perspectives of convergence and divergence in global economy and social development critically examine the stages of early development processes in global economy, distinguish the differences between economy and social development, illustrate the contents of economic and social development policies, their effects on rich and poor countries, and the nature of convergence and divergence in propelling economic growth and unequal social development in world nations. The measurement of convergence and divergence in global economy and social development utilised both economic and social data that were combined into an index that measures the precise levels of the effects of economic and social development policies on human well-being in the rich and poor nations. The task of finding policy solutions to resolve the controversies are reviewed through empirical investigations and the analyses of trends indicated within economic and social indicators and data. These revealed how the adoption of social policy measures in translating the gains from economic growth, towards promoting education, public health, and equity, generate social progress and longer life expectancy, higher economic growth, and sustain more stable macro economy for the nations. Social policy is concerned with the translation of benefits from objectives of global economic growth policies, to objectives of social development policy in nation states. Social policy, therefore, represents an open door whereby benefits of economic growth policies are linked with the broader objectives of social development policy, thereby enhancing the possibility of extending benefits from economic growth to all human being in every nation.

Suljetun jäähdytysvesiverkon mallinnus

Työssä selvitettiin Neste Oil Porvoon jalostamon tuotantolinja 2 jäähdytysvesiverkon tilaa. Jäähdytysvesiverkon hydraulinen malli päivitettiin ja verifioitiin painemittauksin. Mallia tarkennettiin säätöventtiilien mallinnuksen sekä virhelähteiden tarkastelun perusteella havaituin muutoksin. Mallin verifioinnissa havaittiin huomattavia eroja mallin ja mitattujen paineiden välillä. Tämä johti mallin tarkempaan tarkasteluun, sekä virhelähteiden ja niiden vaikutusten selvittämiseen. Putkivarusteiden mallinnusmenetelmiä, sekä mallinnusperiaatteita vertailtiin keskenään. Koska jäähdytysveden kokonaiskierto oli riittämätön, tarkasteltiin kolmea vaihtoehtoa riittävän kiertovesimäärän aikaansaamiseksi. Nykyisten kiertovesipumppujen rinnanoperointi, sekä riittävän suureksi skaalatun pumpun käyttö simuloitiin. Kolmantena tapauksena arvioitiin lämmönvaihdinkohtaisen kuristussuunnitelman vaikutus putkiston painehäviöön, sekä putkistolle sopiva kiertovesipumppu. Vaihtoehdoille laskettiin suuntaa-antavat investointi- ja käyttökustannukset. Tarkastelun perusteella riittävän suureksi skaalattu pumppu todettiin kannattavimmaksi pienen hintaeron, sekä luotettavamman jäähdytysvesikierron käyttövarmuuden vuoksi. Työssä onnistuttiin tuottamaan yleispätevää tietoa suljetun jäähdytysvesiverkon hydrauliseen mallinnukseen vaikuttavista tekijöistä, sekä niiden vaikutuksesta mallin tarkkuuteen. Selvityksen perusteella tarkasteltua mallia saatiin tarkemmaksi.

Sähköisten hankintamenettelyjen taloudelliset yritysvaikutukset

Pro gradu -tutkielmassa tutkitaan julkisissa hankinnoissa käyttöön otettavien uusien sähköisten menettelyjen, sähköisen huutokaupan ja dynaamisen hankintajärjestelmän, yritysvaikutuksia. Ydintutkimustehtävänä on tutkia, millaisia taloudellisia vaikutuksia sähköisillä menettelyillä tulee olemaan yrityksiin niiden tarjotessa palveluita tai tavaroita julkiselle sektorille ja mitkä ovat sähköisten menettelyjen käytön motiivit. Tutkielman teoriaosa on pohja empiiriselle tutkimukselle, jossa aineistona on käytetty suppeaa kyselytutkimusta, haastatteluja ja lisäksi materiaalia on tuotettu analysoimalla hallinnollisten kustannusten määrää sähköisissä hankintamenettelyissä. Yritysvaikutusten arvioinnissa tarkasteltiin sähköisten hankintamenettelyjen käytön motiiveja. Motiiveiksi tunnistettiin tehokkuuden tavoittelu, kustannussäästöt, ajankäytön ja henkilöresurssien käytön tehostaminen sekä avoimuus. Tutkimuksessa onnistuttiin todentamaan edellä mainittuja tekijöitä taloudellisilla malleilla. Määrälliset ja laadulliset tutkimustulokset osoittavat kokonaisuudessaan tuloksellisella tavalla sähköisten hankintamenettelyjen käytön motiiveita ja vaikutuksia yrityksiin. Sähköisillä hankintamenettelyillä voidaan perustellusti tehostaa hankintaprosessia ja saavuttaa kustannussäästöjä. Monia yleisiä yritysten julkisiin hankintoihin pääsyn esteinä pitämiä seikkoja voitaisiin vähentää tai poistaa käyttämällä sähköisiä hankintoja. Sähköistä huutokauppaa ja dynaamista hankintajärjestelmää koskevan lainsäädännön luodessa puitteet menettelyiden käytölle, tulee menettelyjen käyttöönoton motiivien ja kannustimien riittävyyttä seurata. Hallinnollisten kustannusten väheneminen ja muiden esteiden pieneneminen ei välttämättä synnytä pysyvää kannustinvaikutusta, vaan hankintaprosessia tulee pyrkiä sähköistämään kokonaisvaltaisesti myös muissa hankintalain mukaisissa hankintamenettelyissä ja kilpailuttamisen ulkopuolisissa hankinnan osa-alueissa kuten laskuttaminen, maksatus ja tilaus.

Defects in Persistent Luminescence Materials

Persistent luminescence materials can store energy from solar radiation or artificial lighting and release it over a period of several hours without a continuous excitation source. These materials are widely used to improve human safety in emergency and traffic signalization. They can also be utilized in novel applications including solar cells, medical diagnostics, radiation detectors and structural damage sensors. The development of these materials is currently based on methods based on trial and error. The tailoring of new materials is also hindered by the lack of knowledge on the role of their intrinsic and extrinsic lattice defects in the appropriate mechanisms. The goal of this work was to clarify the persistent luminescence mechanisms by combining ab initio density functional theory (DFT) calculations with selected experimental methods. The DFT approach enables a full control of both the nature of the defects and their locations in the host lattice. The materials studied in the present work, the distrontium magnesium disilicate (Sr₂MgSi₂O₇) and strontium aluminate (SrAl₂O₄) are among the most efficient persistent luminescence hosts when doped with divalent europium Eu²⁺ and co-doped with trivalent rare earth ions R³⁺ (R: Y, La-Nd, Sm, Gd-Lu). The polycrystalline materials were prepared with the solid state method and their structural and phase purity was confirmed by X-ray powder diffraction. Their local crystal structure was studied by high-resolution transmission electron microscopy. The crystal and electronic structure of the nondoped as well as Eu²⁺, R^2+/3+ and other defect containing materials were studied using DFT calculations. The experimental trap depths were obtained using thermoluminescence (TL) spectroscopy. The emission and excitation of Sr₂MgSi₂O₇:Eu²+,Dy³⁺ were also studied. Significant modifications in the local crystal structure due to the Eu²⁺ ion and lattice defects were found by the experimental and DFT methods. The charge compensation effects induced by the R³⁺ co-doping further increased the number of defects and distortions in the host lattice. As for the electronic structure of Sr₂MgSi₂O₇ and SrAl₂O₄, the experimental band gap energy of the host materials was well reproduced by the calculations. The DFT calculated Eu²⁺ and R^2+/3+ 4fn as well as 4f^n-15d¹ ground states in the Sr₂MgSi₂O₇ band structure provide an independent verification for an empirical model which is constructed using rather sparse experimental data for the R³⁺ and especially the R²⁺ ions. The intrinsic and defect induced electron traps were found to act together as energy storage sites contributing to the materials’ efficient persistent luminescence. The calculated trap energy range agreed with the trap structure of Sr₂MgSi₂O₇ obtained using TL measurements. More experimental studies should be carried out for SrAl₂O₄ to compare with the DFT calculations. The calculated and experimental results show that the electron traps created by both the rare earth ions and vacancies are modified due to the defect aggregation and charge compensation effects. The relationships between this modification and the energy storage properties of the solid state materials are discussed.

Effect of light intensity and growth substratum on plant development and production of secondary metabolites in Cordia curassavica (Jacq.) Roem. & Schult

Cordia curassavica (Jacq.) Roem. & Schult. (Boraginaceae), also referred to as Cordia verbenacea DC, has been traditionally used for medicinal purposes. This study was driven to verify the behavior of the species in similar conditions to its natural environment, such as high light intensity and sandbank soil, and in conditions of low light intensity and fertilized substratum (dystroferric red nitosoil plus earthworm humus). The growth of the plant, the income of leaf crude extracts and, in the alcoholic extract, the number of substances found in thin layer cromatography and the toxicity of the substratum was observed. The results indicated that the growth of the root biomass, stem and leaves in discharge or lower light intensity was similar, but smaller in sandbank soil than in fertilized soil. The relative income of extracts in ether of petroleum and alcohol was larger in high light intensity and fertilized substratum. The light intensity and the substratum type didn't affect the number of substances detected in the alcoholic extract or the toxicity of this extract. Stains corresponding to the rosmarinic acid were only evidenced in some samples of the alcoholic extract, not allowing the verification of the effect of the treatments about its production.

Bag-of-Features Approach to Unsupervised Visual Object Categorisation

The large and growing number of digital images is making manual image search laborious. Only a fraction of the images contain metadata that can be used to search for a particular type of image. Thus, the main research question of this thesis is whether it is possible to learn visual object categories directly from images. Computers process images as long lists of pixels that do not have a clear connection to high-level semantics which could be used in the image search. There are various methods introduced in the literature to extract low-level image features and also approaches to connect these low-level features with high-level semantics. One of these approaches is called Bag-of-Features which is studied in the thesis. In the Bag-of-Features approach, the images are described using a visual codebook. The codebook is built from the descriptions of the image patches using clustering. The images are described by matching descriptions of image patches with the visual codebook and computing the number of matches for each code. In this thesis, unsupervised visual object categorisation using the Bag-of-Features approach is studied. The goal is to find groups of similar images, e.g., images that contain an object from the same category. The standard Bag-of-Features approach is improved by using spatial information and visual saliency. It was found that the performance of the visual object categorisation can be improved by using spatial information of local features to verify the matches. However, this process is computationally heavy, and thus, the number of images must be limited in the spatial matching, for example, by using the Bag-of-Features method as in this study. Different approaches for saliency detection are studied and a new method based on the Hessian-Affine local feature detector is proposed. The new method achieves comparable results with current state-of-the-art. The visual object categorisation performance was improved by using foreground segmentation based on saliency information, especially when the background could be considered as clutter.

Nollapersoonalause suomessa ja virossa. Tutkimus kirjoitetun kielen aineistosta

The present study focuses on the zero person constructions both in Finnish and Estonian. In the zero person construction, there is no overt subject and the verb is in the 3rd person singular form: Fin. Tammikuussa voi hiihtää Etelä-Suomessakin. Est. Jaanuaris saab suusatada ka Lõuna-Soomes ‘In January one can ski even in South-Finland’. The meaning of the zero construction is usually considered generic and open. However, the zero may be interpreted as indexically open so that the reference can be construed from the context. This study demonstrates how the zero may be interpreted as referring to the speaker, the addressee, or anybody. The zero person construction in Finnish has been contrasted to the generic pronoun constructions in Indo-European languages. For example, the zero person is translated in English as you or one; in Swedish and German as man. The grammar and semantics of the Finnish zero person construction have been studied earlier to some extent. However, the differences and similarities between Finnish and Estonian, two closely related languages, have not been thoroughly studied before. The present doctoral thesis sheds light on the zero person construction, its use, functions, and interpretation both in Finnish and Estonian. The approach taken is contrastive. The data comes from magazine articles published in Finnish and translated into Estonian. The data consists of Finnish sentences with the zero person and their Estonian translations. In addition, the data includes literary fiction, and non-translated Estonian corpora texts as well. Estonian and Finnish are closely related and in principle the personal system of the two languages is almost identical, nevertheless, there are interesting differences. The present study shows that the zero person construction is not as common in Estonian as it is in Finnish. In my data, a typical sentence with the zero person in both languages is a generic statement which tells us what can or cannot be done. When making generic statements the two languages are relatively similar, especially when the zero person is used together with a modal verb. The modal verbs (eg. Fin. voida ‘can’, saada ‘may’, täytyä ‘must’; Est. võima ‘may’, saama ‘can’, tulema ’must’) are the most common verbs in both Finnish and Estonian zero person constructions. Significant differences appear when a non-modal verb is used. Overall, non-modal verbs are used less frequently in both languages. Verbs with relatively low agentivity or intentionality, such as perception verb nähdä in Finnish and nägema in Estonian, are used in the zero person clauses in both languages to certain extent. Verbs with more agentive and intentional properties are not used in the Estonian zero person clauses; in Finnish their use is restricted to specific context. The if–then-frame provides a suitable context for the zero person in Finnish, and the Finnish zero person may occur together with any kind of verb in conditional if-clause. Estonian if-clauses are not suitable contexts for zero person. There is usually a da-infinitive, a generic 2nd person singular or a passive form instead of the zero person in Estonian counterparts for Finnish if-clauses with zero person. The aim of this study was to analyze motivations for choosing the zero person in certain contexts. In Estonian, the use of the zero person constructions is more limited than in Finnish, and some of the constraints are grammatical. On the other hand, some of the constraints are motivated by the differences in actual language use. Contrasting the two languages reveals interesting differences and similarities between these two languages and shows how these languages may use similar means differently.

Production of a product similar to gelatin from chicken feet collagen

Chicken feet can be used as an alternative source of collagen for the development of new products. In this sense, the aim of this study was the production of a product similar to gelatin from collagen extracted from chicken feet and the evaluation of sensory quality. The products were produced in two distinct flavors, with grape flavor called GU and pineapple flavor called GA. Subsequently, we compared these formulations with gelatin of a trademark established in the market. We used in the verification of sensory acceptability of products a hedonic scale of 9 points and the availability of consuming the product by 30 untrained tasters. According to the results, all formulations showed good levels of acceptability, indicating the collagen from chicken feet as an alternative source of high quality in the production of gelatin.

Use of interactive performance optimization for identifying the ideal profile of swine finishing producers

The present research aimed to develop a modeling capable of identifying the ideal profile of swine finishing producers using the interactive performance optimization, which began by verifying qualitative the criteria considered most relevant to the decision-making, generating a closed structured diagnosis that covers the socioeconomic aspects about the activity, until the design of a mathematical model able to translate the data obtained in quantitative information. For the verification, it was proposed a practical study for a universe of 120 members of a cooperative in the state of Rio Grande do Sul, Brazil. The results showed that, from the application and the definition of the ideal profile, it was possible to verify that 82 producers are in the group of those who have obtained a "Good" performance, and to 44 the result is in the range between 86% to 90% from the ideal, which means that most have short or medium-term conditions to evolve their status for the considered "Very Good", where only 12.5% of the producers are currently.

Process approach in quality management - Case: ECO process development in EMS industry

The aim of the thesis was to study quality management with process approach and to find out how to utilize process management to improve quality. The operating environment of organizations has changed. Organizations are focusing on their core competences and networking with suppliers and customers to ensure more effective and efficient value creation for the end customer. Quality management is moving from inspection of the output to prevention of problems from occurring in the first place and management thinking is changing from functional approach to process approach. In the theoretical part of the thesis, it is studied how to define quality, how to achieve good quality, how to improve quality, and how to make sure the improvement goes on as never ending cycle. A selection of quality tools is introduced. Process approach to quality management is described and compared to functional approach, which is the traditional way to manage operations and quality. The customer focus is also studied, and it is presented, that to ensure long term customer commitment, organization needs to react to changing customer requirements and wishes by constantly improving the processes. In the experimental part the theories are tested in a process improvement business case. It is shown how to execute a process improvement project starting from defining the customer requirements, continuing to defining the process ownership, roles and responsibilities, boundaries, interfaces and the actual process activities. The control points and measures are determined for the process, as well as the feedback and corrective action process, to ensure continual improvement can be achieved and to enable verification that customer requirements are fulfilled.

Voimalaitoksen käytönaikaisen optimoinnin määrittely

Tässä diplomityössä määritellään biopolttoainetta käyttävän voimalaitoksen käytönaikainen tuotannon optimointimenetelmä. Määrittelytyö liittyy MW Powerin MultiPower CHP –voimalaitoskonseptin jatkokehitysprojektiin. Erilaisten olemassa olevien optimointitapojen joukosta valitaan tarkoitukseen sopiva, laitosmalliin ja kustannusfunktioon perustuva menetelmä, jonka tulokset viedään automaatiojärjestelmään PID-säätimien asetusarvojen muodossa. Prosessin mittaustulosten avulla lasketaan laitoksen energia- ja massataseet, joiden tuloksia käytetään seuraavan optimointihetken lähtötietoina. Optimoinnin kohdefunktio on kustannusfunktio, jonka termit ovat voimalaitoksen käytöstä aiheutuvia tuottoja ja kustannuksia. Prosessia optimoidaan säätimille annetut raja-arvot huomioiden niin, että kokonaiskate maksimoituu. Kun laitokselle kertyy käyttöikää ja historiadataa, voidaan prosessin optimointia nopeuttaa hakemalla tilastollisesti historiadatasta nykytilanteen olosuhteita vastaava hetki. Kyseisen historian hetken katetta verrataan kustannusfunktion optimoinnista saatuun katteeseen. Paremman katteen antavan menetelmän laskemat asetusarvot otetaan käyttöön prosessin ohjausta varten. Mikäli kustannusfunktion laskenta eikä historiadatan perusteella tehty haku anna paranevaa katetta, niiden laskemia asetusarvoja ei oteta käyttöön. Sen sijaan optimia aletaan hakea deterministisellä optimointialgoritmilla, joka hakee nykyhetken ympäristöstä paremman katteen antavia säätimien asetusarvoja. Säätöjärjestelmä on mahdollista toteuttaa myös tulevaisuutta ennustavana. Työn käytännön osuudessa voimalaitosmalli luodaan kahden eri mallinnusohjelman avulla, joista toisella kuvataan kattilan ja toisella voimalaitosprosessin toimintaa. Mallinnuksen tuloksena saatuja prosessiarvoja hyödynnetään lähtötietoina käyttökatteen laskennassa. Kate lasketaan kustannusfunktion perusteella. Tuotoista suurimmat liittyvät sähkön ja lämmön myyntiin sekä tuotantotukeen, ja suurimmat kustannukset liittyvät investoinnin takaisinmaksuun ja polttoaineen ostoon. Kustannusfunktiolle tehdään herkkyystarkastelu, jossa seurataan katteen muutosta prosessin teknisiä arvoja muutettaessa. Tuloksia vertaillaan referenssivoimalaitoksella suoritettujen verifiointimittausten tuloksiin, ja havaitaan, että tulokset eivät ole täysin yhteneviä. Erot johtuvat sekä mallinnuksen puutteista että mittausten lyhyehköistä tarkasteluajoista. Automatisoidun optimointijärjestelmän käytännön toteutusta alustetaan määrittelemällä käyttöön otettava optimointitapa, siihen liittyvät säätöpiirit ja tarvittavat lähtötiedot. Projektia tullaan jatkamaan järjestelmän ohjelmoinnilla, testauksella ja virityksellä todellisessa voimalaitosympäristössä ja myöhemmin ennustavan säädön toteuttamisella.

Virtuaalimallin hyödyntäminen harvesteripään tuotekehityksessä

Virtuaalimallinnuksella tarkoitetaan koneen simulointia, jossa huomioidaan koneen mekaniikka, toimilaitteet ja ohjausjärjestelmä. Työn tavoitteena oli luoda virtuaalimalli harvesteripäästä. Kyseinen virtuaalimalli sisälsi harvesteripään tärkeimmät mekaaniset osat, pituusmittalaitteen hydrauliikkapiirin ja tämän ohjauksen. Luodussa virtuaalimallissa huomioitiin myös harvesteripään ja puun väliset kontaktit. Lisäksi työssä tutkittiin mahdollista virtuaalimallinnuksen implementoimista osaksi yrityksen tuotekehitysprosessia. Työssä suoritettiin verifiointimittaukset pituusmittalaitteen hydrauliikkapiirille sekä virtuaalimallin hydrauliikkakomponentit parametrisoitiin. Mittauksista saatuja tuloksia verrattiin virtuaalimallista saatuihin tuloksiin. Työssä esitellään myös ehdotus kuinka virtuaalimallinnusta kannattaisi hyödyntää osana yrityksen tuotekehitysprosessia. Virtuaalimallin eri osa-alueilla saavutetut tulokset osoittavat, että virtuaalimallinuksen hyödyntäminen tuotekehitysprosessin aikana mahdollistaa harvesteripään toimintojen tarkastelun ennen prototyypin rakentamista ja testaamista. Lisäksi hydrauliikkapiirin parametrisoimisella pystytään tutkimaan parametrien vaikutusta kokonaisuuteen.

Is professional recognition in plastic surgery related to activity in research

OBJECTIVE: To evaluate the relation of medical research, with the participation of prominent plastic surgeon in Congress.METHODS: We reviewed the scientific programs of the last 3 Brazilian Congress of Surgery, were selected 21 Brazilian plástic surgeons invited to serve as panelists or speakers in roundtable sessions in the last 3 congresses (Group 1). We randomly selected and paired by other members (associates) of the Brazilian Society of Plastic Surgery, with no participation in congress as speaker (Group 2). We conducted a search for articles published in journals indexed in Medline, Lilacs and SciELO for all doctors selected during the entire academic career and the last 5 years from March 2007 until March 2012. We assessed the research activity through the simple counting of the number of publications in indexed journals for each professional. The number of publications groups was compared.RESULTS: articles produced throughout career: Group 1- 639 articles (average of 30.42 items each). Group 2- 79 articles (mean 3.95 articles each). Difference between medias: p <0.001.CONCLUSION: The results demonstrate that the Brazilian Society of Plastic Surgery seeking professionals with a greater number of publications and journals of higher impact. This approach encourages new members to pursue a higher qualification, and give security to congressmen, they can rely on the existence of a technical criterion in the choice of speakers.

Practical Framework for Monitoring the Performance of Agile IT Projects in an Output-Based Outsourcing Context

Over the past decade, organizations worldwide have begun to widely adopt agile software development practices, which offer greater flexibility to frequently changing business requirements, better cost effectiveness due to minimization of waste, faster time-to-market, and closer collaboration between business and IT. At the same time, IT services are continuing to be increasingly outsourced to third parties providing the organizations with the ability to focus on their core capabilities as well as to take advantage of better demand scalability, access to specialized skills, and cost benefits. An output-based pricing model, where the customers pay directly for the functionality that was delivered rather than the effort spent, is quickly becoming a new trend in IT outsourcing allowing to transfer the risk away from the customer while at the same time offering much better incentives for the supplier to optimize processes and improve efficiency, and consequently producing a true win-win outcome. Despite the widespread adoption of both agile practices and output-based outsourcing, there is little formal research available on how the two can be effectively combined in practice. Moreover, little practical guidance exists on how companies can measure the performance of their agile projects, which are being delivered in an output-based outsourced environment. This research attempted to shed light on this issue by developing a practical project monitoring framework which may be readily applied by organizations to monitor the performance of agile projects in an output-based outsourcing context, thus taking advantage of the combined benefits of such an arrangement Modified from action research approach, this research was divided into two cycles, each consisting of the Identification, Analysis, Verification, and Conclusion phases. During Cycle 1, a list of six Key Performance Indicators (KPIs) was proposed and accepted by the professionals in the studied multinational organization, which formed the core of the proposed framework and answered the first research sub-question of what needs to be measured. In Cycle 2, a more in-depth analysis was provided for each of the suggested Key Performance Indicators including the techniques for capturing, calculating, and evaluating the information provided by each KPI. In the course of Cycle 2, the second research sub-question was answered, clarifying how the data for each KPI needed to be measured, interpreted, and acted upon. Consequently, after two incremental research cycles, the primary research question was answered describing the practical framework that may be used for monitoring the performance of agile IT projects delivered in an output-based outsourcing context. This framework was evaluated by the professionals within the context of the studied organization and received positive feedback across all four evaluation criteria set forth in this research, including the low overhead of data collection, high value of provided information, ease of understandability of the metric dashboard, and high generalizability of the proposed framework.