scholarly journals Motor-Transmission Drive System: a Benchmark Example for Safety Verification

10.29007/ct87 ◽  
2018 ◽  
Author(s):  
Hongxu Chen ◽  
Sayan Mitra ◽  
Guangyu Tian
Keyword(s):  
Safety Analysis ◽  
Drive System ◽  
Safety Verification ◽  
System A ◽  
Safety Property ◽  
Verification Problem ◽  
Problem Description ◽  
Verification Tools ◽  
Initial States ◽  
The Impact

This paper introduces the Motor-Transmission Drive System as a benchmark example for the safety analysis of hybrid systems.In particular, we illustrate the problem of checking the gear meshing duration and the impact impulse (both of which we refer to as safety) of the Motor-Transmission Drive System.We aim to provide a complete problem description to which different verification tools or approaches for safety analysis can be applied and compared.For this reason, we first elaborate on a hybrid automaton (HA) model of the Motor-Transmission Drive System to describe the gear meshing process with uncertain initial states, and then we specify the safety property of interest.Next, we clarify the characteristic phenomena exhibited by the benchmark which make the verification problem hard to solve.Finally, we show some simulation results to illustrate the influences of the initial states on the safety property.This benchmark example can help the researchers and engineers to find appropriate methods for safety verification of this kind of hybrid system.

scholarly journals Implicit Semi-Algebraic Abstraction for Polynomial Dynamical Systems

2021 ◽  
pp. 529-551
Author(s):  
Sergio Mover ◽  
Alessandro Cimatti ◽  
Alberto Griggio ◽  
Ahmed Irfan ◽  
Stefano Tonetta
Keyword(s):  
Dynamical Systems ◽  
Discrete Systems ◽  
Model Checker ◽  
Safety Verification ◽  
Polynomial Dynamical Systems ◽  
Main Challenge ◽  
Safety Property ◽  
Verification Problem ◽  
Explicit Enumeration ◽  
Infinite State

AbstractSemi-algebraic abstraction is an approach to the safety verification problem for polynomial dynamical systems where the state space is partitioned according to the sign of a set of polynomials. Similarly to predicate abstraction for discrete systems, the number of abstract states is exponential in the number of polynomials. Hence, semi-algebraic abstraction is expensive to explicitly compute and then analyze (e.g., to prove a safety property or extract invariants).In this paper, we propose an implicit encoding of the semi-algebraic abstraction, which avoids the explicit enumeration of the abstract states: the safety verification problem for dynamical systems is reduced to a corresponding problem for infinite-state transition systems, allowing us to reuse existing model-checking tools based on Satisfiability Modulo Theory (SMT). The main challenge we solve is to express the semi-algebraic abstraction as a first-order logic formula that is linear in the number of predicates, instead of exponential, thus letting the model checker lazily explore the exponential number of abstract states with symbolic techniques. We implemented the approach and validated experimentally its potential to prove safety for polynomial dynamical systems.

Technology and Hospital Information System: A Case of Implementation of Electronic Clinical Records in Hospital Maternity Irene Neto in Lubango, Angola

2019 ◽  
Vol 10 (11) ◽  
pp. 1131-1135
Author(s):  
Tomas Hambili Paulo Sanjuluca ◽  
◽  
Ricardo Correia ◽  
Anabela Antunes de Almeida ◽  
Ana Gloria Diaz Martinez ◽  
...  
Keyword(s):  
Maternity Hospital ◽  
Management Support ◽  
Retrospective Case ◽  
System A ◽  
Clinical Records ◽  
Retrospective Case Study ◽  
The Impact ◽  
And Child Health

Introduction: In order to have a good assessment of the quality of maternal and child health care, it is essential that there is up-to-date and reliable information. Objective: To evaluate the impact of the implementation of a computerized database of clinical processes in the admission, archive and medical statistics section, of Maternity hospital Irene Neto/Lubango-Angola. Methodology: A descriptive study with a quantitative and qualitative approach to carry out a retrospective case study deliveries and newborns, records from 2014 to 2017. Final considerations: The implementation of this project may contribute to the improvement of clinical management support management of the hospital as well as facilitating access to information for research and scientific production.

Instability and Collapse in Discrete Wave Equations

2005 ◽  
Vol 5 (3) ◽  
pp. 223-241
Author(s):  
A. Carpio ◽  
G. Duro
Keyword(s):  
Continuum Limit ◽  
Wave Equations ◽  
Numerical Solutions ◽  
Blow Up ◽  
Theoretical Predictions ◽  
Initial States ◽  
The Impact ◽  
The Continuum

AbstractUnstable growth phenomena in spatially discrete wave equations are studied. We characterize sets of initial states leading to instability and collapse and obtain analytical predictions for the blow-up time. The theoretical predictions are con- trasted with the numerical solutions computed by a variety of schemes. The behavior of the systems in the continuum limit and the impact of discreteness and friction are discussed.

The Impact of Political Transition on Ghana’s Educational System. A Case Study of the 4th Republic

2018 ◽  
Author(s):  
Emmanuel Owusu-Kwarteng ◽  
Prince Opoku ◽  
Gershon Dagba ◽  
Mark Amankwa
Keyword(s):  
Educational System ◽  
Political Transition ◽  
System A ◽  
The Impact

Impact Load Buffering Method Based on Stress Wave Attenuation Principle

2019 ◽  
Vol 11 (02) ◽  
pp. 1950019 ◽  
Author(s):  
Lin Gan ◽  
He Zhang ◽  
Cheng Zhou ◽  
Lin Liu
Keyword(s):  
Stress Wave ◽  
Wave Attenuation ◽  
Impact Load ◽  
Dynamics Simulation ◽  
Scanning System ◽  
Isolation Method ◽  
Element Analysis ◽  
System A ◽  
High Emission ◽  
The Impact

Rotating scanning motor is the important component of synchronous scanning laser fuze. High emission overload environment in the conventional ammunition has a serious impact on the reliability of the motor. Based on the theory that the buffer pad can attenuate the impact stress wave, a new motor buffering Isolation Method is proposed. The dynamical model of the new buffering isolation structure is established by ANSYS infinite element analysis software to do the nonlinear impact dynamics simulation of rotating scanning motor. The effectiveness of Buffering Isolation using different materials is comparatively analyzed. Finally, the Macht hammer impact experiment is done, the results show that in the experience of the 70,000[Formula: see text]g impact acceleration, the new buffering Isolation method can reduce the impact load about 15 times, which can effectively alleviate the plastic deformation of rotational scanning motor and improve the reliability of synchronization scanning system. A new method and theoretical basis of anti-high overload research for Laser Fuze is presented.

Statistical Approaches to Structural Change in Regional Interindustry Models

1986 ◽  
Vol 18 (9) ◽  
pp. 1189-1207
Author(s):  
B Ó Huallacháin
Keyword(s):  
Structural Change ◽  
Structural Changes ◽  
Washington State ◽  
Multivariate Statistical Analyses ◽  
Input Output ◽  
Multivariate Statistical ◽  
State Data ◽  
System A ◽  
Statistical Approaches ◽  
The Impact

The conventional approach to assessing structural change in regional input – output tables is to measure the impact of coefficient change on the estimation of outputs and multipliers. The methods developed and tested in this paper focus exclusively on the coefficients. Univariate and multivariate statistical analyses can be used to identify and measure various types of changes ranging from coefficient instability to changes in interindustry relationships as a system. A distinction is made between structural changes in input relationships and those in output relationships. The methods are tested by using Washington State data for the years 1963 and 1967. The results are compared with previous analyses of change in these data.

scholarly journals Modeling and image quality enhancement for dynamic compressive imaging system

2021 ◽  
Vol 15 ◽  
pp. 174830262110080
Author(s):  
Changjun Zha* ◽  
Qian Zhang* ◽  
Huimin Duan
Keyword(s):  
Image Quality ◽  
Imaging System ◽  
Quality Enhancement ◽  
Target Image ◽  
Compressive Imaging ◽  
Image Quality Enhancement ◽  
System A ◽  
Single Column ◽  
The Impact

Traditional single-pixel imaging systems are aimed mainly at relatively static or slowly changing targets. When there is relative motion between the imaging system and the target, sizable deviations between the measurement values and the real values can occur and result in poor image quality of the reconstructed target. To solve this problem, a novel dynamic compressive imaging system is proposed. In this system, a single-column digital micro-mirror device is used to modulate the target image, and the compressive measurement values are obtained for each column of the image. Based on analysis of the measurement values, a new recovery model of dynamic compressive imaging is given. Differing from traditional reconstruction results, the measurement values of any column of vectors in the target image can be used to reconstruct the vectors of two adjacent columns at the same time. Contingent upon characteristics of the results, a method of image quality enhancement based on an overlapping average algorithm is proposed. Simulation experiments and analysis show that the proposed dynamic compressive imaging can effectively reconstruct the target image; and that when the moving speed of the system changes within a certain range, the system reconstructs a better original image. The system overcomes the impact of dynamically changing speeds, and affords significantly better performance than traditional compressive imaging.

scholarly journals Impact of an accelerated melting of Greenland on malaria distribution over Africa

2021 ◽  
Vol 12 (1) ◽  
Author(s):  
Alizée Chemison ◽  
Gilles Ramstein ◽  
Adrian M. Tompkins ◽  
Dimitri Defrance ◽  
Guigone Camus ◽  
...  
Keyword(s):  
Climate Change ◽  
Malaria Transmission ◽  
Ice Sheet ◽  
Transmission Risk ◽  
Future Climate Change ◽  
Climate Change Scenarios ◽  
Climate Change Risk ◽  
System A ◽  
Climate Simulations ◽  
The Impact

AbstractStudies about the impact of future climate change on diseases have mostly focused on standard Representative Concentration Pathway climate change scenarios. These scenarios do not account for the non-linear dynamics of the climate system. A rapid ice-sheet melting could occur, impacting climate and consequently societies. Here, we investigate the additional impact of a rapid ice-sheet melting of Greenland on climate and malaria transmission in Africa using several malaria models driven by Institute Pierre Simon Laplace climate simulations. Results reveal that our melting scenario could moderate the simulated increase in malaria risk over East Africa, due to cooling and drying effects, cause a largest decrease in malaria transmission risk over West Africa and drive malaria emergence in southern Africa associated with a significant southward shift of the African rain-belt. We argue that the effect of such ice-sheet melting should be investigated further in future public health and agriculture climate change risk assessments.

Sign in / Sign up

Export Citation Format

Share Document