Multi-objective ant colony optimization for requirements selection

The selection of a set of requirements between all the requirements previously defined by customers is an important process, repeated at the beginning of each development step when an incremental or agile software development approach is adopted. The set of selected requirements will be developed during the actual iteration. This selection problem can be reformulated as a search problem, allowing its treatment with metaheuristic optimization techniques. This paper studies how to apply Ant Colony Optimization algorithms to select requirements. First, we describe this problem formally extending an earlier version of the problem, and introduce a method based on Ant Colony System to find a variety of efficient solutions. The performance achieved by the Ant Colony System is compared with that of Greedy Randomized Adaptive Search Procedure and Non-dominated Sorting Genetic Algorithm, by means of computational experiments carried out on two instances of the problem constructed from data provided by the experts.

JCML: A specification language for the runtime verification of Java Card programs

COSTA, Umberto Souza; MOREIRA, Anamaria Martins; MUSICANTE, Matin A.; SOUZA NETO, Plácido A. JCML: A specification language for the runtime verification of Java Card programs. Science of Computer Programming. [S.l]: [s.n], 2010.

Specification and Runtime Verification of Java Card Programs

COSTA, Umberto Souza da; MOREIRA, Anamaria Martins; MUSICANTE, Martin A. Specification and Runtime Verification of Java Card Programs. Electronic Notes in Theoretical Computer Science. [S.l:s.n], 2009.

Reuse and integration of specification logics: the hybridisation perspective

Hybridisation is a systematic process along which the characteristic features of hybrid logic, both at the syntactic and the semantic levels, are developed on top of an arbitrary logic framed as an institution. It also captures the construction of first-order encodings of such hybridised institutions into theories in first-order logic. The method was originally developed to build suitable logics for the specification of reconfigurable software systems on top of whatever logic is used to describe local requirements of each system’s configuration. Hybridisation has, however, a broader scope, providing a fresh example of yet another development in combining and reusing logics driven by a problem from Computer Science. This paper offers an overview of this method, proposes some new extensions, namely the introduction of full quantification leading to the specification of dynamic modalities, and exemplifies its potential through a didactical application. It is discussed how hybridisation can be successfully used in a formal specification course in which students progress from equational to hybrid specifications in a uniform setting, integrating paradigms, combining data and behaviour, and dealing appropriately with systems evolution and reconfiguration.

A functional specification and validation model for networks on chip in the ACL2 logic

International audience

Projeto de uma ferramenta específica para cravação de terminais elétricos

A necessidade contínua de incrementar a produtividade em todos os sectores leva a que sejam utilizados equipamentos cada vez mais sofisticados, permitindo novas técnicas de abordagem dos processos de fabrico, velocidades mais elevadas e maior precisão no produto final. No entanto, quase todos os equipamentos necessitam de ferramentas adequadas, que tirem partido efetivamente das potencialidades dos equipamentos disponíveis. A Engenharia tem aqui um papel extremamente importante, já que terá de conceber as ferramentas atendendo à satisfação de um elevado número de requisitos, que passam genericamente por tirar o máximo partido dos fatores tecnológicos proporcionados pelos equipamentos, cumprir com a cadência de produção necessária, assegurar a qualidade estipulada, garantir a segurança dos colaboradores que com ela trabalham e permitir uma fácil montagem e afinação, reduzindo assim os tempos de preparação e as possibilidades de fabrico de peças fora das especificações. Este trabalho foi desenvolvido em torno de uma necessidade real, tendo sido estipulados os requisitos necessários pelo cliente e tendo sido elaborado todo o projeto da ferramenta em torno desses mesmos requisitos. Foi efetuada uma otimização da ferramenta ainda na fase de anteprojeto, permitindo minimizar o seu custo e maximizar o seu rendimento e aptidão para o fim em vista. Os materiais foram cuidadosamente selecionados, tendo em vista a utilização de cada componente e a relação custo‐benefício. Foi ainda efetuada uma orçamentação da mesma, assim como um plano de instruções para a operação e manutenção da ferramenta. Deste modo, este trabalho é o resumo de grande parte do conhecimento adquirido, quer ao longo da vida académica, quer ao longo da experiência profissional.

Requirements for the use of virtual worlds in corporate training : perspectives from the post-mortem of a corporate e-learning provider approach of Second Life and OpenSimulator

Between 2009 and 2011, a joint academia-industry effort took place to integrate Second Life and OpenSimulator platforms into a corporate elearning provider’s learning management platform. The process involved managers and lead developers at the provider and an academic engineering research team. We performed content analysis on the documents produced in this process, seeking data on the corporate perspective of requirements for virtual world platforms to be usable in everyday practice. In this paper, we present the requirements found in the documents, and detail how they emerged and evolved throughout the process.

Improving photofermentative hydrogen production through metabolic engineering and DOE (Design of Experiments)

A l’heure actuelle, les biocarburants renouvelables et qui ne nuit pas à l'environnement sont à l'étude intensive en raison de l'augmentation des problèmes de santé et de la diminution des combustibles fossiles. H2 est l'un des candidats les plus prometteurs en raison de ses caractéristiques uniques, telles que la densité d'énergie élevée et la génération faible ou inexistante de polluants. Une façon attrayante pour produire la H2 est par les bactéries photosynthétiques qui peuvent capter l'énergie lumineuse pour actionner la production H2 avec leur système de nitrogénase. L'objectif principal de cette étude était d'améliorer le rendement de H2 des bactéries photosynthétiques pourpres non sulfureuses utilisant une combinaison de génie métabolique et le plan des expériences. Une hypothèse est que le rendement en H2 pourrait être améliorée par la redirection de flux de cycle du Calvin-Benson-Bassham envers du système de nitrogénase qui catalyse la réduction des protons en H2. Ainsi, un PRK, phosphoribulose kinase, mutant « knock-out » de Rhodobacter capsulatus JP91 a été créé. L’analyse de la croissance sur des différentes sources de carbone a montré que ce mutant ne peut croître qu’avec l’acétate, sans toutefois produire d' H2. Un mutant spontané, YL1, a été récupéré qui a retenu l'cbbP (codant pour PRK) mutation d'origine, mais qui avait acquis la capacité de se développer sur le glucose et produire H2. Une étude de la production H2 sous différents niveaux d'éclairage a montré que le rendement d’YL1 était de 20-40% supérieure à la souche type sauvage JP91. Cependant, il n'y avait pas d'amélioration notable du taux de production de H2. Une étude cinétique a montré que la croissance et la production d'hydrogène sont fortement liées avec des électrons à partir du glucose principalement dirigés vers la production de H2 et la formation de la biomasse. Sous des intensités lumineuses faibles à intermédiaires, la production d'acides organiques est importante, ce qui suggère une nouvelle amélioration additionnel du rendement H2 pourrait être possible grâce à l'optimisation des processus. Dans une série d'expériences associées, un autre mutant spontané, YL2, qui a un phénotype similaire à YL1, a été testé pour la croissance dans un milieu contenant de l'ammonium. Les résultats ont montré que YL2 ne peut croître que avec de l'acétate comme source de carbone, encore une fois, sans produire de H2. Une incubation prolongée dans les milieux qui ne supportent pas la croissance de YL2 a permis l'isolement de deux mutants spontanés secondaires intéressants, YL3 et YL4. L'analyse par empreint du pied Western a montré que les deux souches ont, dans une gamme de concentrations d'ammonium, l'expression constitutive de la nitrogénase. Les génomes d’YL2, YL3 et YL4 ont été séquencés afin de trouver les mutations responsables de ce phénomène. Fait intéressant, les mutations de nifA1 et nifA2 ont été trouvés dans les deux YL3 et YL4. Il est probable qu'un changement conformationnel de NifA modifie l'interaction protéine-protéine entre NifA et PII protéines (telles que GlnB ou GlnK), lui permettant d'échapper à la régulation par l'ammonium, et donc d'être capable d'activer la transcription de la nitrogénase en présence d'ammonium. On ignore comment le nitrogénase synthétisé est capable de maintenir son activité parce qu’en théorie, il devrait également être soumis à une régulation post-traductionnelle par ammonium. Une autre preuve pourrait être obtenue par l'étude du transcriptome d’YL3 et YL4. Une première étude sur la production d’ H2 par YL3 et YL4 ont montré qu'ils sont capables d’une beaucoup plus grande production d'hydrogène que JP91 en milieu d'ammonium, qui ouvre la porte pour les études futures avec ces souches en utilisant des déchets contenant de l'ammonium en tant que substrats. Enfin, le reformage biologique de l'éthanol à H2 avec la bactérie photosynthétique, Rhodopseudomonas palustris CGA009 a été examiné. La production d'éthanol avec fermentation utilisant des ressources renouvelables microbiennes a été traitée comme une technique mature. Cependant, la plupart des études du reformage de l'éthanol à H2 se sont concentrés sur le reformage chimique à la vapeur, ce qui nécessite généralement une haute charge énergetique et résultats dans les émissions de gaz toxiques. Ainsi le reformage biologique de l'éthanol à H2 avec des bactéries photosynthétiques, qui peuvent capturer la lumière pour répondre aux besoins énergétiques de cette réaction, semble d’être plus prometteuse. Une étude précédente a démontré la production d'hydrogène à partir d'éthanol, toutefois, le rendement ou la durée de cette réaction n'a pas été examiné. Une analyse RSM (méthode de surface de réponse) a été réalisée dans laquelle les concentrations de trois facteurs principaux, l'intensité lumineuse, de l'éthanol et du glutamate ont été variés. Nos résultats ont montré que près de 2 moles de H2 peuvent être obtenus à partir d'une mole d'éthanol, 33% de ce qui est théoriquement possible.

A Coopetition Space for Complex Product Specification

Part 3: Product-Service Systems

Climate change and irrigation water requirement at Jaguaribe river basin, semi-arid northeast of Brazil.

Summary: Climate change has a potential to impact rainfall, temperature and air humidity, which have relation to plant evapotranspiration and crop water requirement. The purpose of this research is to assess climate change impacts on irrigation water demand, based on future scenarios derived from the PRECIS (Providing Regional Climates for Impacts Studies), using boundary conditions of the HadCM3 submitted to a dynamic downscaling nested to the Hadley Centre regional circulation model HadRM3P. Monthly time series for average temperature and rainfall were generated for 1961-90 (baseline) and the future (2040). The reference evapotranspiration was estimated using monthly average temperature. Projected climate change impact on irrigation water demand demonstrated to be a result of evapotranspiration and rainfall trend. Impacts were mapped over the target region by using geostatistical methods. An increase of the average crop water needs was estimated to be 18.7% and 22.2% higher for 2040 A2 and B2 scenarios, respectively. Objective ? To analyze the climate change impacts on irrigation water requirements, using downscaling techniques of a climate change model, at the river basin scale. Method: The study area was delimited between 4º39?30? and 5º40?00? South and 37º35?30? and 38º27?00? West. The crop pattern in the target area was characterized, regarding type of irrigated crops, respective areas and cropping schedules, as well as the area and type of irrigation systems adopted. The PRECIS (Providing Regional Climates for Impacts Studies) system (Jones et al., 2004) was used for generating climate predictions for the target area, using the boundary conditions of the Hadley Centre model HadCM3 (Johns et al., 2003). The considered time scale of interest for climate change impacts evaluation was the year of 2040, representing the period of 2025 to 2055. The output data from the climate model was interpolated, considering latitude/longitude, by applying ordinary kriging tools available at a Geographic Information System, in order to produce thematic maps.

Methods for Modeling and Analyzing Concurrent Software

Concurrent software executes multiple threads or processes to achieve high performance. However, concurrency results in a huge number of different system behaviors that are difficult to test and verify. The aim of this dissertation is to develop new methods and tools for modeling and analyzing concurrent software systems at design and code levels. This dissertation consists of several related results. First, a formal model of Mondex, an electronic purse system, is built using Petri nets from user requirements, which is formally verified using model checking. Second, Petri nets models are automatically mined from the event traces generated from scientific workflows. Third, partial order models are automatically extracted from some instrumented concurrent program execution, and potential atomicity violation bugs are automatically verified based on the partial order models using model checking. Our formal specification and verification of Mondex have contributed to the world wide effort in developing a verified software repository. Our method to mine Petri net models automatically from provenance offers a new approach to build scientific workflows. Our dynamic prediction tool, named McPatom, can predict several known bugs in real world systems including one that evades several other existing tools. McPatom is efficient and scalable as it takes advantage of the nature of atomicity violations and considers only a pair of threads and accesses to a single shared variable at one time. However, predictive tools need to consider the tradeoffs between precision and coverage. Based on McPatom, this dissertation presents two methods for improving the coverage and precision of atomicity violation predictions: 1) a post-prediction analysis method to increase coverage while ensuring precision; 2) a follow-up replaying method to further increase coverage. Both methods are implemented in a completely automatic tool.

Nutritional requirements of the critically ill patient

Objective: Given the inaccessibility of indirect calorimetry, intensive care units generally use predictive equations or recommendations that are established by international societies to determine energy expenditure. The aim of the present study was to compare the energy expenditure of critically ill patients, as determined using indirect calorimetry, to the values obtained using the Harris-Benedict equation. Methods: A retrospective observational study was conducted at the Intensive Care Unit 1 of the Centro Hospitalar do Porto. The energy requirements of hospitalized critically ill patients as determined using indirect calorimetry were assessed between January 2003 and April 2012. The accuracy (± 10% difference between the measured and estimated values), the mean differences and the limits of agreement were determined for the studied equations. Results: Eighty-five patients were assessed using 288 indirect calorimetry measurements. The following energy requirement values were obtained for the different methods: 1,753.98±391.13 kcal/ day (24.48 ± 5.95 kcal/kg/day) for indirect calorimetry and 1,504.11 ± 266.99 kcal/day (20.72±2.43 kcal/kg/day) for the HarrisBenedict equation. The equation had a precision of 31.76% with a mean difference of -259.86 kcal/day and limits of agreement between -858.84 and 339.12 kcal/day. Sex (p=0.023), temperature (p=0.009) and body mass index (p< 0.001) were found to significantly affect energy expenditure Conclusion: The Harris-Benedict equation is inaccurate and tends to underestimate energy expenditure. In addition, the Harris-Benedict equation is associated with significant differences between the predicted and true energy expenditure at an individual level

Empowering engineering students through employability skills

A professional course program like engineering strives to get the maximum number of its students placed through campus interviews. While communication skills have been added in all the engineering courses with the aim to improve their performance in placement, the syllabus mostly concentrates on the development of four language skills. The students are not made aware of the employability skills and their significance. This essay intends to enlist the importance of skills and why students need to be aware of the skills they possess and how they can work on packaging their candidature around a few skills. The discussion starts by addressing the apparent gap between academic programs for engineering students and industry skills requirements. A list of vital employability skills from the standpoint of engineering students follows, with a discussion on how to potentially develop such skills through campus life. The essay stresses the role of academia in filling this gap by acting as facilitators in a three-step process (i.e., awareness, self-analysis, and acquisition). The author concludes that the combination of both employability skills along with an engineering degree should ensure students meet the high expectations of the employers.