Refinement and variability techniques in model transformation of software requirements

Tese de Doutoramento em Tecnologias e Sistemas de Informação

Refinement in hybridised institutions

Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of reconfigurable systems, i.e., systems with reconfiguration mechanisms governing the dynamic evolution of their execution configurations in response to both external stimuli or internal performance measures. A formal representation of such systems is through transition structures whose states correspond to the different configurations they may adopt. Therefore, each node is endowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. This paper characterises equivalence and refinement for these sorts of models in a way which is independent of (or parametric on) whatever logic (propositional, equational, fuzzy, etc) is found appropriate to describe the local configurations. A Hennessy–Milner like theorem is proved for hybridised logics.

Aprendizagem baseada na resolução de problemas: uma experiência pedagógica com alunos de um Curso de Especialização Tecnológica

Relatório de estágio de mestrado em Ensino de Informática

Carbonation front progress in mortars containing fly ash considering the presence of chloride ions

The incorporation of fly ash (FA) in cementitious matrices have been frequently used in order to make the matrix more resistant to the action of chlorides. On the other hand, it is known that Ca (OH)2 existing in the matrix is partially consumed by the pozzolanic reactions, which facilitates the advancement of carbonation. Given that the combined action between carbonation and chloride penetration is a fact little known, we speculate about the behaviour of the matrix in this context. This study investigates the influence of the presence of chlorides on the carbonation in mortars with FA. Samples with 0% and 40% replacement of cement CEM I 42.5 R for FA were molded with water/binder 0.56 and 0.52 respectively. After 90 days of curing the specimens were subjected to cycles of immersion/drying for 56 days. Half of the samples was subjected to the following cycle: two days in a solution containing NaCl (concentration equal to 3.5 %); 12 days in the carbonation chamber (4% of CO2). The other half was: two days in water; 12 days in the carbonation chamber. Then, the development of carbonation was evaluated. The results indicate that the presence of chlorides influences the carbonation. The specimens submitted to the exclusive action of CO2 showed a greater depth of carbonation compared to that presented by the specimens subjected to combined action. This may be related to changes in properties of the matrix which may lead to further refinement of the pores and related to the presence of the salt that can lead to partial filling of the pores and the increase in moisture content.

Monitoring and analysis of queries in distributed databases

Dissertação de Mestrado em Engenharia Informática

Temporal analysis of CHAVE collection

Lecture Notes in Computer Science, 9309

Measuring university-to-work success: development of a new scale

Purpose – The purpose of this paper is to develop a subjective multidimensional measure of early career success during university-to-work transition. Design/methodology/approach – The construct of university-to-work success (UWS) was defined in terms of intrinsic and extrinsic career outcomes, and a three-stage study was conducted to create a new scale. Findings – A preliminary set of items was developed and tested by judges. Results showed the items had good content validity. Factor analyses indicated a four-factor structure and a second-order model with subscales to assess: career insertion and satisfaction, confidence in career future, income and financial independence, and adaptation to work. Third, the authors sought to confirm the hypothesized model examining the comparative fit of the scale and two alternative models. Results showed that fits for both the first- and second-order models were acceptable. Research limitations/implications – The proposed model has sound psychometric qualities, although the validated version of the scale was not able to incorporate all constructs envisaged by the initial theoretical model. Results indicated some direction for further refinement. Practical implications – The scale could be used as a tool for self-assessment or as an outcome measure to assess the efficacy of university-to-work programs in applied settings. Originality/value – This study provides a useful single measure to assess early career success during the university-to-work transition, and might facilitate testing of causal models which could help identify factors relevant for successful transition.

Urothelial bladder cancer progression: lessons learned from the bench

Urothelial bladder carcinoma (UBC) is an intricate malignancy with a variable natural history and clinical behavior. Despite developments in diagnosis/prognosis refinement and treatment modalities, the recurrence rate is high, and progression from non-muscle to muscle invasive UBC commonly leads to metastasis. Moreover, patients with muscle-invasive or extra-vesical disease often fail the standard chemotherapy treatment, and overall survival rates are poor. Thus, UBC remains a challenge in the oncology field, representing an ideal candidate for research on biomarkers that could identify patients at increased risk of recurrence, progression, and chemo-refractoriness. However, progress toward personalized medicine has been hampered by the unique genetic complexity of UBC. Recent genome-wide expression and sequencing studies have brought new insights into its molecular features, pathogenesis and clinical diversity, revealing a landscape where classical pathology is intersected by the novel and heterogeneous molecular groups. Hence, it seems plausible to postulate that only an integrated signature of prognostic/predictive biomarkers inherent in different cancer hallmarks will reach clinical validation. In this review, we have summarized ours and others' research into novel putative biomarkers of progression and chemoresistance that encompass several hallmarks of cancer: tumor neovascularization, invasion and metastasis, and energy metabolism reprogramming of the tumor microenvironment.

Efeito da adição de Zr no endurecimento de ligas Al-Sc

Dissertação de mestrado integrado em Engenharia de Materiais

On the verification of architectural reconfigurations

In a reconfigurable system, the response to contextual or internal change may trigger reconfiguration events which, on their turn, activate scripts that change the system׳s architecture at runtime. To be safe, however, such reconfigurations are expected to obey the fundamental principles originally specified by its architect. This paper introduces an approach to ensure that such principles are observed along reconfigurations by verifying them against concrete specifications in a suitable logic. Architectures, reconfiguration scripts, and principles are specified in Archery, an architectural description language with formal semantics. Principles are encoded as constraints, which become formulas of a two-layer graded hybrid logic, where the upper layer restricts reconfigurations, and the lower layer constrains the resulting configurations. Constraints are verified by translating them into logic formulas, which are interpreted over models derived from Archery specifications of architectures and reconfigurations. Suitable notions of bisimulation and refinement, to which the architect may resort to compare configurations, are given, and their relationship with modal validity is discussed.

Metaphorisms in programming

This paper introduces the metaphorism pattern of relational specification and addresses how specification following this pattern can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement proposed in this paper is a strategy known as change of virtual data structure. It gives sufficient conditions for such implementations to be calculated using relation algebra and illustrates the strategy with the derivation of quicksort as example.

Dificuldades de expansão da infografia interativa: um problema de produção e receção

Dissertação de mestrado em Media Interativos

Contributos dos ambientes digitais online para a aprendizagem em contexto de atividades de apoio extraescolar

Dissertação de mestrado em Ciências da Educação (área de especialização em Tecnologia Educativa)

BIOMedical search engine framework: lightweight and customized implementation of domain-specific biomedical search engines

The Smart Drug Search is publicly accessible at http://sing.ei.uvigo.es/sds/. The BIOMedical Search Engine Framework is freely available for non-commercial use at https://github.com/agjacome/biomsef

Object-oriented inheritance of statecharts for control applications

This paper discusses how object-oriented iuheritance can be re-interpreted if statecharts are used for modelling the dynamic behaviour of an object. The support of inheritance of statecharts allows the improvement of systems' development by easing the reutilization of parts of already developed euccessful systems, aad by promoting the iterative and continuous models' refinement advocated by the operatioaal approach. Statechart is the formalism used within UML to specify reactive state.based behaviours. This paper covers the use of statecharts within the modelling of embedded systems for industrial control applxications, where performance and memory usage are main concerns.