57 research outputs found
Sympathetic activity, assessed by power spectral analysis of heart rate variability, in white-coat, masked and sustained hypertension versus true normotension.
No full textOBJECTIVE:
To assess, in a population-based approach, sympathetic nervous system activity by the use of power spectral analysis of heart rate variability, in normotension, white-coat hypertension, masked hypertension and sustained hypertension.
METHODS:
The electrocardiographic RR interval was registered in the supine and standing positions and the low-frequency and high-frequency components of its variability were quantified. Cut-off values of 140/90 mmHg for conventional blood pressure and 135/85 mmHg for daytime ambulatory blood pressure were used to define the four blood pressure groups.
RESULTS:
After exclusion of patients with diabetes, myocardial infarction or treated hypertension, 1485 subjects with complete data remained for the analysis in the supine position. Age averaged 39 +/- 14 years; 54% were women. Conventional and ambulatory blood pressure averaged, respectively, 122 +/- 16/79 +/- 11 mmHg and 124 +/- 12/77 +/- 8 mmHg. After adjusting for demographic, anthropometric and lifestyle characteristics, the low-frequency to high-frequency ratio (geometric mean) averaged 0.81 in normotension and was significantly higher in white-coat hypertension (1.11; P < 0.001), based on a higher low-frequency component and a lower high-frequency component (P < 0.01). This ratio was not significantly different between normotension, masked hypertension (0.97) and sustained hypertension (0.93). The adjusted standing-to-supine ratio of the high-frequency component (geometric mean) was significantly higher in sustained hypertension (0.50) than in normotension (0.39; P < 0.01), but not in white-coat (0.40) and masked hypertension (0.45).
CONCLUSION:
The findings at rest are compatible with increased sympathetic activity and decreased parasympathetic modulation in white-coat hypertension, with normal autonomic cardiac regulation in masked and sustained hypertension. In addition, sustained hypertension is characterized by a blunted decrease of the high-frequency component on standing
BLOOD PRESSURE VARIES WITH PHYSIOLOGICALLY DETERMINED EPIGENETIC INTERACTIONS AMONG THE ADDUCIN GENES IN 6 EUROPEAN POPULATIONS
No full textQUALITY CONTROL OF THE BLOOD PRESSURE PHENOTYPE IN THE EUROPEAN PROJECT ON GENES IN HYPERTENSION
No full textOBJECTIVES:
In the European Project on Genes in Hypertension (EPOGH) standardized epidemiological methods were used to determine complex phenotypes consisting of blood pressure (BP) in combination with other traits. In this report, we present the quality control of one of the BP phenotypes.
METHODS:
In seven European countries eight different research groups recruited random samples of nuclear families. Trained observers measured the BP five times consecutively with the participants in the seated position at each of two separate home visits, 1 to 3 weeks apart, according to the guidelines of the British Hypertension Society. Quality assurance and quality control of this BP phenotype were implemented according to detailed instructions defined in the protocol of the EPOGH study.
RESULTS:
On 31 August 2001, BP measurements of 2476 subjects were available for analysis. Fewer BP readings than the five planned per visit occurred in one of the eight centres, but only in 0.4% of the home visits. Across centres the relative frequency of identical consecutive readings for systolic or diastolic blood pressure varied from 0 to 6%. The occurrence of odd readings ranged from 0 to 0.1%. Of the 49,488 systolic and diastolic BP readings, 24.0% ended on a zero (expected 20%). In most EPOGH centres there was a progressive decline in the BP from the first to the second home visit. Overall, these decreases averaged 2.36 mmHg [95% confidence interval (CI): 1.98-2.74, P < 0.001] for systolic BP and 1.74 mmHg (95% CI: 1.46-2.02, P < 0.001) for diastolic BP.
CONCLUSIONS:
Quality assurance and control should be planned at the design stage of a project involving BP measurement and implemented from its very beginnings until the end. The procedures of quality assurance set up in the EPOGH study for the BP measurements resulted in a well-defined BP phenotype, which was consistent across centres
A wide-spectrum language for verification of programs on weak memory models
No full textModern processors deploy a variety of weak memory models, which for efficiency reasons may (appear to) execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be complex and subtle, and can impact on ensuring correctness. Previous work on the semantics of weak memory models has focussed on the behaviour of assembler-level programs. In this paper we utilise that work to extract some general principles underlying instruction reordering, and apply those principles to a wide-spectrum language encompassing abstract data types as well as low-level assembler code. The goal is to support reasoning about implementations of data structures for modern processors with respect to an abstract specification. Specifically, we encode a weak memory model in a pair-wise reordering relation on instructions. Some architectures require an additional definition of the behaviour of the global storage system if it does not provide multi-copy atomicity. In this paper we use the reordering relation in an operational semantics. We derive some properties of program refinement under weak memory models, and encode the semantics in the rewriting engine Maude as a model-checking tool. The tool is used to validate the semantics against the behaviour of a set of litmus tests (small assembler programs) run on hardware, and also to model check implementations of data structures from the literature against their abstract specifications
SDN-Actors:Modeling and Verification of SDN Programs
No full textSoftware-Defined Networking (SDN) is a recent networking paradigm that has become increasingly popular in the last decade. It gives unprecedented control over the global behavior of the network and provides a new opportunity for formal methods. Much work has appeared in the last few years on providing bridges between SDN and verification. This paper advances this research line and provides a link between SDN and traditional work on formal methods for verification of distributed software—actor-based modelling. We show how SDN programs can be seamlessly modelled using actors, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops.Depto. de Sistemas Informáticos y ComputaciónFac. de InformáticaTRUEpu
UniForM Workbench - Formal Methods and the Development of Dependable Systems
No full textIn this article we describe a formal framework for the development of dependable systems, supporting the systematic development of cooperating mechanisms designed to encounter combinations of threats. We focus on the combination of fault-tolerance mechanisms and security mechanisms in communication protocols. Until recently, fault-tolerant systems and secure systems were discussed and developed, at least in Germany, in different -- often non-communicating -- communities. Based on experiences with systems developed by the author in various industrial projects we motivate that a unified approach for the development of systems that combine both security and fault-tolerance properties will become increasingly important. Practical experience has shown that the a posteriori integration of security features into a fault-tolerant system and vice versa is much more complicated than pre-planning every desired dependability and security feature simultaneously during the specification phase of th..
The activity of the sympathetic nervous system, assessed by power spectral analysis of heart rate variability, in whitecoat, masked and sustained hypertension
No full textAbstract
OBJECTIVE:
To assess, in a population-based approach, sympathetic nervous system activity by the use of power spectral analysis of heart rate variability, in normotension, white-coat hypertension, masked hypertension and sustained hypertension.
METHODS:
The electrocardiographic RR interval was registered in the supine and standing positions and the low-frequency and high-frequency components of its variability were quantified. Cut-off values of 140/90 mmHg for conventional blood pressure and 135/85 mmHg for daytime ambulatory blood pressure were used to define the four blood pressure groups.
RESULTS:
After exclusion of patients with diabetes, myocardial infarction or treated hypertension, 1485 subjects with complete data remained for the analysis in the supine position. Age averaged 39 +/- 14 years; 54% were women. Conventional and ambulatory blood pressure averaged, respectively, 122 +/- 16/79 +/- 11 mmHg and 124 +/- 12/77 +/- 8 mmHg. After adjusting for demographic, anthropometric and lifestyle characteristics, the low-frequency to high-frequency ratio (geometric mean) averaged 0.81 in normotension and was significantly higher in white-coat hypertension (1.11; P < 0.001), based on a higher low-frequency component and a lower high-frequency component (P < 0.01). This ratio was not significantly different between normotension, masked hypertension (0.97) and sustained hypertension (0.93). The adjusted standing-to-supine ratio of the high-frequency component (geometric mean) was significantly higher in sustained hypertension (0.50) than in normotension (0.39; P < 0.01), but not in white-coat (0.40) and masked hypertension (0.45).
CONCLUSION:
The findings at rest are compatible with increased sympathetic activity and decreased parasympathetic modulation in white-coat hypertension, with normal autonomic cardiac regulation in masked and sustained hypertension. In addition, sustained hypertension is characterized by a blunted decrease of the high-frequency component on standing
Testen von End-zu-End Chains mittels Domain Spezifischer Sprachen
No full textTesting systems is a time consuming (and hence expensive) activity. Nevertheless, it is a very important and necessary step before using systems, especially safety critical systems. Therefore, many different test procedures are used: Unit Tests, Black-Box Tests, Software Integration Tests (SWI), Hardware-Software Integration Tests (HSI), Hardware-In-The-Loop Tests, just to name a few. Especially in the avionics domain, a variety of systems and applications communicate which each other. Furthermore, they depend and rely on the received information. However, some faults are only detected when all systems are connected and in operational mode. A new testing approach is to create model based End-To-End Chain scenarios with original and simulated equipment in any combination. The first aim is to automatically derive test data and test cases from the model, which is defined by a Domain Specific Language (DSL). Test data generators can be attached to quickly create a variety of stimuli for the systems under test. Furthermore, the system under test can be stimulated by either original equipment which is connected to the test bench or the test bench can simulate equipment and create inputs for the tested systems. Any mixture of simulated and original equipment is possible and can be changed on the fly. In the end, the results from the system under test are collected. These results can then be displayed back in the model. This method was used and improved in the project E-Enabled Cabin (E-Cab) in which the author was involved. Passengers traveling by plane are in the focus of this project. Complete services and service chains ranging from booking at home with a computer, being en route using mobile devices to leaving the destination airport are created and used by many systems communicating with each other. A special focus is set on a guidance scenario at an airport. The user of the system signs in to a guidance and notification system which will inform him via his own digital equipment (mobile device/smart phone). The system notifies the user about his in-time status. Either he is in-time for his flight, or he needs to hurry up and proceed to the next area or he will be too late and cannot catch his flight. The DSL itself is designed according to the comprehension of information processes. The ability of the human brain to process visual information in parallel in contrast to sequential processing of textual information is described and applied in the design of the DSL and the concepts of the project. The development of the DSL and the workflow is developed with the real world in mind. This means that the work fits in established workflows and enhances the current situation. As this project took place in the aircraft industry, the appropriate development standards, like DO178B and ABD100/200 (Airbus Directives ABD100/ABD200), build the foundation. The generation of clean code is established by applying generator guidelines (through coding standards) in order to create maintainable tests and test data
Serum HDL cholesterol in relation to genetic variation in PPAR-gamma2, GNB3 and alcohol intake
No full textImpact factor 2007: 4.69
Effective Infinite-State Model Checking by Input Equivalence Class Partitioning
No full textPart 1: Model Based TestingInternational audienceIn this paper, it is shown how a complete input equivalence class testing strategy developed by the second author can be effectively used for infinite-state model checking of system models with infinite input domains but finitely many internal state values and finite output domains. This class of systems occurs frequently in the safety-critical domain, where controllers may input conceptually infinite analogue data, but make a finite number of control decisions based on inputs and current internal state. A variant of Kripke Structures is well-suited to provide a behavioural model for this system class. It is shown how the known construction of specific input equivalence classes can be used to abstract the infinite input domain of the reference model into finitely many classes. Then quick checks can be made on the implementation model showing that the implementation is not I/O-equivalent to the reference model if its abstraction to observable minimal finite state machines has a different number of states or a different input partitioning as the reference model. Only if these properties are consistent with the reference model, a detailed equivalence check between the abstracted models needs to be performed. The complete test suites obtained as a by-product of the checking procedure can be used to establish counter examples showing the non-conformity between implementation model and reference model. Using various sample models, it is shown that this approach outperforms model checkers that do not possess this equivalence class generation capability
- …
