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.

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.

Probabilistic verification of satellite systems for mission critical applications

In this thesis, we present a quantitative approach using probabilistic verification techniques for the analysis of reliability, availability, maintainability, and safety (RAMS) properties of satellite systems. The subject of our research is satellites used in mission critical industrial applications. A strong case for using probabilistic model checking to support RAMS analysis of satellite systems is made by our verification results. This study is intended to build a foundation to help reliability engineers with a basic background in model checking to apply probabilistic model checking to small satellite systems. We make two major contributions. One of these is the approach of RAMS analysis to satellite systems. In the past, RAMS analysis has been extensively applied to the field of electrical and electronics engineering. It allows system designers and reliability engineers to predict the likelihood of failures from the indication of historical or current operational data. There is a high potential for the application of RAMS analysis in the field of space science and engineering. However, there is a lack of standardisation and suitable procedures for the correct study of RAMS characteristics for satellite systems. This thesis considers the promising application of RAMS analysis to the case of satellite design, use, and maintenance, focusing on its system segments. Data collection and verification procedures are discussed, and a number of considerations are also presented on how to predict the probability of failure. Our second contribution is leveraging the power of probabilistic model checking to analyse satellite systems. We present techniques for analysing satellite systems that differ from the more common quantitative approaches based on traditional simulation and testing. These techniques have not been applied in this context before. We present the use of probabilistic techniques via a suite of detailed examples, together with their analysis. Our presentation is done in an incremental manner: in terms of complexity of application domains and system models, and a detailed PRISM model of each scenario. We also provide results from practical work together with a discussion about future improvements.

Motion Planning and Controls with Safety and Temporal Constraints

Motion planning, or trajectory planning, commonly refers to a process of converting high-level task specifications into low-level control commands that can be executed on the system of interest. For different applications, the system will be different. It can be an autonomous vehicle, an Unmanned Aerial Vehicle(UAV), a humanoid robot, or an industrial robotic arm. As human machine interaction is essential in many of these systems, safety is fundamental and crucial. Many of the applications also involve performing a task in an optimal manner within a given time constraint. Therefore, in this thesis, we focus on two aspects of the motion planning problem. One is the verification and synthesis of the safe controls for autonomous ground and air vehicles in collision avoidance scenarios. The other part focuses on the high-level planning for the autonomous vehicles with the timed temporal constraints. In the first aspect of our work, we first propose a verification method to prove the safety and robustness of a path planner and the path following controls based on reachable sets. We demonstrate the method on quadrotor and automobile applications. Secondly, we propose a reachable set based collision avoidance algorithm for UAVs. Instead of the traditional approaches of collision avoidance between trajectories, we propose a collision avoidance scheme based on reachable sets and tubes. We then formulate the problem as a convex optimization problem seeking control set design for the aircraft to avoid collision. We apply our approach to collision avoidance scenarios of quadrotors and fixed-wing aircraft. In the second aspect of our work, we address the high level planning problems with timed temporal logic constraints. Firstly, we present an optimization based method for path planning of a mobile robot subject to timed temporal constraints, in a dynamic environment. Temporal logic (TL) can address very complex task specifications such as safety, coverage, motion sequencing etc. We use metric temporal logic (MTL) to encode the task specifications with timing constraints. We then translate the MTL formulae into mixed integer linear constraints and solve the associated optimization problem using a mixed integer linear program solver. We have applied our approach on several case studies in complex dynamical environments subjected to timed temporal specifications. Secondly, we also present a timed automaton based method for planning under the given timed temporal logic specifications. We use metric interval temporal logic (MITL), a member of the MTL family, to represent the task specification, and provide a constructive way to generate a timed automaton and methods to look for accepting runs on the automaton to find an optimal motion (or path) sequence for the robot to complete the task.

Compliance verification of virtual Phasor Measuring Unit using Ip-DFT algorithm according to the IEEE-60255-118-1(2018).

With the increase in load demand for various sectors, protection and safety of the network are key factors that have to be taken into consideration over the electric grid and distribution network. A phasor Measuring unit is an Intelligent electronics device that collects the data in the form of a real-time synchrophasor with a precise time tag using GPS (Global positioning system) and transfers the data to the grid command to monitor and assess the data. The measurements made by PMU have to be very precise to protect the relays and measuring equipment according to the IEEE 60255-118-1(2018). As a device PMU is very expensive to research and develop new functionalities there is a need to find an alternative to working with. Hence many open source virtual libraries are available to replicate the exact function of PMU in the virtual environment(Software) to continue the research on multiple objectives, providing the very least error results when verified. In this thesis, I executed performance and compliance verification of the virtual PMU which was developed using the I-DFT (Interpolated Discrete Fourier transforms) C-class algorithm in MATLAB. In this thesis, a test environment has been developed in MATLAB and tested the virtually developed PMU on both steady state and dynamic state for verifying the latest standard compliance(IEEE-60255-118-1).

Verification of rupture disc sizing of Acrylic Reactor

The primary goal of this thesis is to verify the rupture disc sizing of the acrylic reactor. Primarily the test to check the sizing was divided into several stages. It went on to examine ideas to explain the concern and ethical ways, as well as remedies and suggestions to solve the issues and difficulties that were discovered. This thesis will highlight the gathering and arranging of reaction data (recipe composition, enthalpies, reaction temperature, and catalyst feeding times) of the products to be chosen, in accordance with pre-established criteria. To collaborate with the research and development team in the lab to carry out calorimetric testing for the important recipes that have been identified. The verification of the currently installed Rupture Discs in the plant based on the calorimetric test findings is the final stage. This thesis used two separate calorimetry techniques: Phi-TEC II adiabatic calorimetry and differential scanning calorimetry (DSC). The target of the experiment is to check and confirm the correct size of the reactor rupture disc. Arkema (Boretto/Coatex) plant (Emilia romagna) provided a recipe and a scenario following multiple meetings and discussions. The purpose of this technical paper is to describe the outcomes of adiabatic calorimetry performed at the lab scale so that the computation of the vents for a particular recipe and scenario can be verified.

Predictive Value Of Phase I Trials For Safety In Later Trials And Final Approved Dose: Analysis Of 61 Approved Cancer Drugs.

Phase I trials use a small number of patients to define a maximum tolerated dose (MTD) and the safety of new agents. We compared data from phase I and registration trials to determine whether early trials predicted later safety and final dose. We searched the U.S. Food and Drug Administration (FDA) website for drugs approved in nonpediatric cancers (January 1990-October 2012). The recommended phase II dose (R2PD) and toxicities from phase I were compared with doses and safety in later trials. In 62 of 85 (73%) matched trials, the dose from the later trial was within 20% of the RP2D. In a multivariable analysis, phase I trials of targeted agents were less predictive of the final approved dose (OR, 0.2 for adopting ± 20% of the RP2D for targeted vs. other classes; P = 0.025). Of the 530 clinically relevant toxicities in later trials, 70% (n = 374) were described in phase I. A significant relationship (P = 0.0032) between increasing the number of patients in phase I (up to 60) and the ability to describe future clinically relevant toxicities was observed. Among 28,505 patients in later trials, the death rate that was related to drug was 1.41%. In conclusion, dosing based on phase I trials was associated with a low toxicity-related death rate in later trials. The ability to predict relevant toxicities correlates with the number of patients on the initial phase I trial. The final dose approved was within 20% of the RP2D in 73% of assessed trials.

Efficacy And Safety Of Intravitreal Bevacizumab In Eyes With Neovascular Glaucoma Undergoing Ahmed Glaucoma Valve Implantation: 2-year Follow-up.

To evaluate the efficacy and safety of intravitreal bevacizumab (IVB) in eyes with neovascular glaucoma (NVG) undergoing Ahmed glaucoma valve (AGV) implantation. This was a multicentre, prospective, randomized clinical trial that enrolled 40 patients with uncontrolled neovascular glaucoma that had undergone panretinal photocoagulation and required glaucoma drainage device implantation. Patients were randomized to receive IVB (1.25 mg) or not during Ahmed valve implant surgery. Injections were administered intra-operatively, and 4 and 8 weeks after surgery. After a mean follow-up of 2.25 ± 0.67 years (range 1.5-3 years), both groups showed a significant decrease in IOP (p < 0.05). There was no difference in IOP between groups except at the 18-month interval, when IOP in IVB group was significantly lower (14.57 ± 1.72 mmHg vs. 18.37 ± 1.06 mmHg - p = 0.0002). There was no difference in survival success rates between groups. At 24 months, there was a trend to patients treated with IVB using less antiglaucoma medications than the control group (p = 0.0648). Complete regression of rubeosis iridis was significantly more frequent in the IVB group (80%) than in the control group (25%) (p = 0.0015). Intravitreal bevacizumab may lead to regression of new vessels both in the iris and in the anterior chamber angle in patients with neovascular glaucoma undergoing Ahmed glaucoma valve implantation. There is a trend to slightly lower IOPs and number of medications with IVB use during AGV implantation for neovascular glaucoma.

Long-term Efficacy And Safety Of Tenofovir Disoproxil Fumarate In Hiv-1-infected Adolescents Failing Antiretroviral Therapy: The Final Results Of Study Gs-us-104-0321.

Reports of long-term tenofovir disoproxil fumarate (TDF) treatment in HIV-infected adolescents are limited. We present final results from the open-label (OL) TDF extension following the randomized, placebo (PBO)-controlled, double-blind phase of GS-US-104-0321 (Study 321). HIV-infected 12- to 17-year-olds treated with TDF 300 mg or PBO with an optimized background regimen (OBR) for 24-48 weeks subsequently received OL TDF plus OBR in a single arm study extension. HIV-1 RNA and safety, including bone mineral density (BMD), was assessed in all TDF recipients. Eighty-one subjects received TDF (median duration 96 weeks). No subject died or discontinued OL TDF for safety/tolerability. At week 144, proportions with HIV-1 RNA <50 copies/mL were 30.4% (7 of 23 subjects with baseline HIV-1 RNA >1000 c/mL initially randomized to TDF), 41.7% (5 of 12 subjects with HIV-1 RNA <1000 c/mL who switched PBO to TDF) and 0% (0 of 2 subjects failed randomized PBO plus OBR with HIV-1 RNA >1000 c/mL and switched PBO to TDF). Viral resistance to TDF occurred in 1 subject. At week 144, median decrease in estimated glomerular filtration rate was 38.1 mL/min/1.73 m (n = 25). Increases in median spine (+12.70%, n = 26) and total body less head BMD (+4.32%, n = 26) and height-age adjusted Z-scores (n = 21; +0.457 for spine, +0.152 for total body less head) were observed at week 144. Five of 81 subjects (6%) had persistent >4% BMD decreases from baseline. Some subjects had virologic responses to TDF plus OBR, and TDF resistance was rare. TDF was well tolerated and can be considered for treatment of HIV-infected adolescents.

Segurança no circo : questão de prioridade = Circus safety: a priority issue

Universidade Estadual de Campinas . Faculdade de Educação Física

Reviewed evidence about the safety of the daily use of alcohol-based mouthrinses

Current scientific knowledge provides clear evidence that alcohol-based mouthwashes can be beneficial in a daily oral health routine, including dental hygiene and plaque control. Several issues are worth discussing, in spite of the wealth of supporting evidence. Despite some undesirable effects to some people, like burning sensation, and some contraindications, like the use by infants, alcohol addicts and patients with mucosal injuries, there is no reason to avoid the use of alcohol-containing mouthwashes as long as they are used following proper guidance by dental professionals and the manufacturers' instructions. The alleged correlation between oral cancer and alcohol-based mouthrinses presents so little, weak, inconsistent and even contradictory evidence in the literature that any kind of risk warning to patients would be uncalled for. Antimicrobial mouthrinses are safe and effective in reducing plaque and gingivitis, and should be part of a comprehensive oral health care regimen that includes brushing, flossing and rinsing to prevent or minimize periodontal disease.

Microbiological indicators for the assessment of performance in the hazard analysis and critical control points (HACCP) system in meat lasagna production

The HACCP system is being increasingly used to ensure food safety. This study investigated the validation of the control measures technique in order to establish performance indicators of this HACCP system in the manufacturing process of Lasagna Bolognese (meat lasagna). Samples were collected along the manufacturing process as a whole, before and after the CCPs. The following microorganism s indicator (MIs) was assessed: total mesophile and faecal coliform counts. The same MIs were analyzed in the final product, as well as, the microbiological standards required by the current legislation. A significant reduction in the total mesophile count was observed after cooking (p < 0.001). After storage, there was a numerical, however non-significant change in the MI count. Faecal coliform counts were also significantly reduced (p < 0.001) after cooking. We were able to demonstrate that the HACCP system allowed us to meet the standards set by both, the company and the Brazilian regulations, proved by the reduction in the established indicators

Safety Assessment of Potentially Inappropriate Medications (PIM) use in Older People and the Factors Associated with Hospital Admission

Purpose: Potentially Inappropriate Medications (PIM) use in elderly people may be responsible for the development of Adverse Drug Reaction (ADR) which, when severe, leads to hospital admissions. Objectives: to estimate the prevalence of elderly who had used PIM before being admitted to hospital and to identify the risk factors and the hospitalizations related to ADR arising from PIM. Methods: A descriptive and cross-sectional study was performed in the internal medicine ward of a teaching hospital (Brazil), in 2008. With the aid of a validated form, patients aged >= 60 years, with length of hospital stay >= 24 hours, were interviewed about drugs taken prior to the hospital admission and the complaints/reasons for hospitalization. Results: 19.1% (59/308) of older patients had taken PIM before hospital admission and in 4.9%; there were a causal relation between the PIM taken and the complaint reported. PIM responsible for admissions were: amiodarone, amitriptyline, cimetidine, clonidine, diazepam, digoxin, estrogen, fluoxetine, lorazepam, short-acting nifedipine and propranolol. 47.0% of the clinical manifestations of PIM-related ADR were: dizziness, fatigue, digoxin toxicity and erythema. Only polypharmacy was detected as a risk factor for the occurrence of ADR of PIM (p = 0.02). Conclusion: PIM use in elderly people is not a risk factor for ADR-related hospital admission. Probably, severe ADR, which lead to hospitalizations of older people, can be explained by idiosyncratic response or the predisposition of these patients to develop adverse drug events, whether or not drugs are classed as PIM.