Gonad development and hormone titres in Loggerhead Sea Turtles (Caretta caretta) in the NE Atlantic

The study proposed to describe sexual development in pelagic stage loggerhead sea turtles Caretta caretta and compare this to hatchlings and adults. It is meant as an ontogenic approach, in order to understand reproductive development and population composition and their dynamics in the pelagic environment. The study focused on the pelagic loggerheads that are found in the waters offshore Madeira Island (Portugal) in the North-eastern Atlantic and use it as a developmental habitat. The innovating character of this work relied on the lack of any description regarding the gonad ontogenesis and reproductive development for the pelagic stage in any of the 7 existing sea turtle species, all of them in danger of extinction. Three methods were used to diagnose the sex of each juvenile individual and asses the level of reproductive development: (1) laparoscopy, (2) gonad biopsy and (3) the assessment of two sex steroids circulating levels, namely testosterone and estradiol. In order to cover all life stages and compare data obtained for the juvenile stage, hatchlings and nesting female adults were sampled at the nearest nesting rookery at Boa Vista Island in the Cape Verde Archipelago. Gonads from dead hatchlings were collected for gonad histology and blood was collected from nesting females for sex steroids assessment. Laparoscopies revealed to be a valid sexing method for the juvenile stage, since gonads are morphologically differentiated at these size classes. Moreover, laparoscopy was validated using gonad histology. Gonad histology of juveniles showed that gonads are already completely differentiated into ovaries or testes at the size classes examined, but development seems to be quiescent. Males present already developed seminiferous tubules with spermatogonia lining the interior of the seminiferous tubule. Female gonads present oocytes at different development stages, but only oocytes up to stage III were observed. The maximum oocyte diameter in each individual correlated with body size, suggesting that reproductive development is an on-going process in juvenile females. The circulating levels of both testosterone and estradiol in juveniles of both sexes were very low and consistently lower than the ones observed in the nesting females from Boa Vista Island. No bimodal distribution was found for any of the sex steroids analysed and thus circulating hormone levels were not a reliable tool for sexing juvenile individuals with a non-invasive technique. The ratio testosterone:estradiol did not show a bimodal distribution either. The levels of testosterone correlated with sea surface temperature. The fact that temperatures observed during this study were below 24ºC might have hindered a differential testosterone pattern between juvenile males and females. Sex ratios for this population were generated according to laparoscopy results and compared among years and size classes. An overall sex ratio of 2 females for each male was found, but they varied among size classes but not among years. Possible causes for the sex ratios observed are discussed. This study is a contribution to our knowledge on the pelagic stage of loggerhead turtles, namely on the population structure regarding sex ratio, which is a vital tool for implementing conservation strategies.

JML- Based formal development of a Java card application for managing medical appointments

Although formal methods can dramatically increase the quality of software systems, they have not widely been adopted in software industry. Many software companies have the perception that formal methods are not cost-effective cause they are plenty of mathematical symbols that are difficult for non-experts to assimilate. The Java Modelling Language (short for JML) Section 3.3 is an academic initiative towards the development of a common formal specification language for Java programs, and the implementation of tools to check program correctness. This master thesis work shows how JML based formal methods can be used to formally develop a privacy sensitive Java application. This is a smart card application for managing medical appointments. The application is named HealthCard. We follow the software development strategy introduced by João Pestana, presented in Section 3.4. Our work influenced the development of this strategy by providing hands-on insight on challenges related to development of a privacy sensitive application in Java. Pestana’s strategy is based on a three-step evolution strategy of software specifications, from informal ones, through semiformal ones, to JML formal specifications. We further prove that this strategy can be automated by implementing a tool that generates JML formal specifications from a welldefined subset of informal software specifications. Hence, our work proves that JML-based formal methods techniques are cost-effective, and that they can be made popular in software industry. Although formal methods are not popular in many software development companies, we endeavour to integrate formal methods to general software practices. We hope our work can contribute to a better acceptance of mathematical based formalisms and tools used by software engineers. The structure of this document is as follows. In Section 2, we describe the preliminaries of this thesis work. We make an introduction to the application for managing medical applications we have implemented. We also describe the technologies used in the development of the application. This section further illustrates the Java Card Remote Method Invocation communication model used in the medical application for the client and server applications. Section 3 introduces software correctness, including the design by contract and the concept of contract in JML. Section 4 presents the design structure of the application. Section 5 shows the implementation of the HealthCard. Section 6 describes how the HealthCard is verified and validated using JML formal methods tools. Section 7 includes some metrics of the HealthCard implementation and specification. Section 8 presents a short example of how a client-side of a smart card application can be implemented while respecting formal specifications. Section 9 describes a prototype tools to generate JML formal specifications from informal specifications automatically. Section 10 describes some challenges and main ideas came acrorss during the development of the HealthCard. The full formal specification and implementation of the HealthCard smart card application presented in this document can be reached at https://sourceforge.net/projects/healthcard/.

Analysis an development of a prototype based on media wiki and semantic media wiki integrated with a design modeling that allows modeling of organizations based on demo

In a world where organizations are ever more complex the need for the knowledge of the organizational self is a growing necessity. The DEMO methodology sets a goal in achieving the specification of the organizational self capturing the essence of the organization in way independent of its implementation and also coherent, consistent, complete, modular and objective. But having such organization self notion is of little meaning if this notion is not shared by the organization actors. To achieve this goal in a society that has grown attached to technology and where time is of utmost importance, using a tool such as a semantic Wikipedia may be the perfect way of making the information accessible. However, to establish DEMO methodology in such platform there is a need to create bridges between its modeling components and semantic Wikipedia. It’s in that aspect that our thesis focuses, trying to establish and implement, using a study case, the principles of a way of transforming the DEMO methodology diagrams in comprehensive pages on semantic Wikipedia but keeping them as abstract as possible to allow expansibility and generalization to all diagrams without losing any valuable information so that, if that is the wish, those diagrams may be recreated from the semantic pages and make this process a full cycle.