The Unified Modeling Language UML is well-suited for the design of real-time systems. In particul... more The Unified Modeling Language UML is well-suited for the design of real-time systems. In particular the design of dynamic system behaviors is supported by interaction diagrams and statecharts. Real-time aspects of behaviors can be described by time constraints. The semantics of the UML, however, is non-formal. In order to enable formal design verification, we therefore propose to complement the UML based design by additional formal models which refine UML diagrams to precise formal models. We apply the formal specification technique cTLA which is based on L. Lamport's Temporal Logic of Actions, TLA. In particular cTLA supports modular definitions of process types and the composition of systems from coupled process instances. Since process composition has superposition character each process system has all of the relevant properties of its constituting processes. Therefore mostly small subsystems are sufficient for the verification of system properties and it is not necessary to use complete and complex formal system models. We present this approach by means of an example and also exemplify the formal verification of its hard real-time properties
... The framework supplies veri ed and re-usable implications between prede ned protocol and serv... more ... The framework supplies veri ed and re-usable implications between prede ned protocol and service speci cation components. ... This leads to the idea of support-ing formal protocol speci cation and veri cation by a framework of re-usable prede ned components. ...
Component-structured software, which is coupled from independently developed software components,... more Component-structured software, which is coupled from independently developed software components, introduces new security problems. In particular, a component may attack components of its environment and, in consequence, spoil the application incorporating it. Therefore, to guard a system, we constrain the behavior of a component by ruling out the transmission of events between components which may cause harm. Security policies describing the behavior constraints are formally specified and, at runtime, so-called security wrappers monitor the interface traffic of components and check it for compliance with the specifications. Moreover, one can also use the specifications to prove formally that the combinations of the component security policies fulfill certain security properties of the complete component-structured application. A well-known method to express system security properties is access control which can be modelled by means of the popular Role Based Access Control (RBAC) method. Below, we will introduce a specification framework facilitating the formal proof that component security policy specifications fulfill RBAC-based application access control policies. The specification framework is based on the specification technique cTLA. The design of state-based security policy specifications and of RBAC-models is supported by framework libraries of specification patterns which may be instantiated and composed to a specification. Moreover, the framework contains already proven theorems facilitating the formal reasoning since a deduction proof can be reduced to proof steps which correspond directly to the theorems. In particular, we introduce the specification framework and clarify its application by means of an e-commerce example.
Tidal volume and plateau pressure limitation decreases mortality in acute respiratory distress sy... more Tidal volume and plateau pressure limitation decreases mortality in acute respiratory distress syndrome. Computed tomography demonstrated a small, normally aerated compartment on the top of poorly aerated and nonaerated compartments that may be hyperinflated by tidal inflation. We hypothesized that despite tidal volume and plateau pressure limitation, patients with a larger nonaerated compartment are exposed to tidal hyperinflation of the normally aerated compartment. Pulmonary computed tomography at end-expiration and end-inspiration was obtained in 30 patients ventilated with a low tidal volume (6 ml/kg predicted body weight). Cluster analysis identified 20 patients in whom tidal inflation occurred largely in the normally aerated compartment (69.9 +/- 6.9%; "more protected"), and 10 patients in whom tidal inflation occurred largely within the hyperinflated compartments (63.0 +/- 12.7%; "less protected"). The nonaerated compartment was smaller and the normally aerated compartment was larger in the more protected patients than in the less protected patients (p = 0.01). Pulmonary cytokines were lower in the more protected patients than in the less protected patients (p < 0.05). Ventilator-free days were 7 +/- 8 and 1 +/- 2 d in the more protected and less protected patients, respectively (p = 0.01). Plateau pressure ranged between 25 and 26 cm H(2)O in the more protected patients and between 28 and 30 cm H(2)O in the less protected patients (p = 0.006). Limiting tidal volume to 6 ml/kg predicted body weight and plateau pressure to 30 cm H(2)O may not be sufficient in patients characterized by a larger nonaerated compartment.
To evaluate whether the shape of the airway pressure-time (Paw-t) curve during constant flow infl... more To evaluate whether the shape of the airway pressure-time (Paw-t) curve during constant flow inflation corresponds to radiologic evidence of tidal recruitment or tidal hyperinflation in an experimental model of acute lung injury. Prospective randomized laboratory animal investigation. Department of Clinical Physiology, University of Uppsala, Sweden. Anesthetized, paralyzed, and mechanically ventilated pigs. Acute lung injury was induced by lung lavage. During constant inspiratory flow, the Paw-t curve was fitted to a power equation: airway pressure =a x time + c, where coefficient b (stress index) describes the shape of the curve:b = 1, straight curve; b < 1, progressive increase in slope; and b > 1, progressive decrease in slope. Tidal volume (Vt) was 6 mL/kg, and positive end-expiratory pressure was set to obtain a b value between 0.9 and 1.1 before (b = 1) and after (b = 1 after recruiting maneuver) application of a recruiting maneuver. Positive end-expiratory pressure was decreased and Vt increased to obtain 0.9 >b > 0.8 and 0.8 >b > 0.6, whereas positive end-expiratory pressure and Vt were both increased to obtain 1.3 >b > 1.1 and 1.5 >b > 1.3. Experimental conditions sequence was random. Pulmonary computed tomography was obtained during end-expiratory and end-inspiratory occlusions. Tidal recruitment was quantified as nonaerated (between -100 and +100 Hounsfield units) lung area at end-expiration minus end-inspiration. Tidal hyperinflation was quantified as hyperinflated (between -900 and -1000 Hounsfield units) lung area at end-inspiration minus end-expiration. Computed tomography images showed that tidal recruitment and tidal hyperinflation corresponded to b < 1 and b > 1, respectively. Stress index values and tidal recruitment and tidal hyperinflation values were significantly correlated (R =.917 and R =.911, p <.0001, respectively). Shape of the Paw-t curve detects tidal recruitment and tidal…
Objective To examine the effects of positive end-expiratory pressure (PEEP) on extravascular lung... more Objective To examine the effects of positive end-expiratory pressure (PEEP) on extravascular lung water (EVLW), lung tissue, and lung volume. Design and setting Experimental animal study at a university research facility. Subjects Fifteen adult sheep. Interventions All animals were studied before and after saline washout-induced lung injury while ventilated with sequentially increasing PEEP (0, 7, 14, or 21 cmH2O). Measurements and results Lung volume was determined by computed tomography and EVLW by the thermal dye dilution technique. Saline washout significantly increased lung tissue volume (21±3 to 37±5 ml/kg) and EVLW (9±2 to 36±9 ml/kg). While increasing levels of PEEP reduced EVLW (30±7, 24±8, and 18±4 ml/kg), lung tissue volume remained constant. Total lung volume significantly increased (50±8 ml/kg at PEEP 0 to 77±12 ml/kg at PEEP 21). Nonaerated lung volume significantly decreased and was closely correlated with the changes in EVLW (r=0.67). In addition, a highly significant correlation was found between PEEP-induced decrease in nonaerated lung volume and decrease in transpulmonary shunt (r=0.83). Conclusions The main findings are as follows: (a) PEEP effectively decreases EVLW. (b) The decrease in EVLW is closely correlated with the PEEP-induced decrease in nonaerated lung volume, making EVLW a valuable bedside parameter indicating alveolar recruitment, similar to measurements of transpulmonary shunt. (c) As excess tissue volume remained constant, however, EVLW may not be suitable to reflect overall severity of lung disease
The aim of the experiments was to check the feasibility of pulmonary perfusion imaging by functio... more The aim of the experiments was to check the feasibility of pulmonary perfusion imaging by functional electrical impedance tomography (EIT) and to compare the EIT findings with electron beam computed tomography (EBCT) scans. In three pigs, a Swan-Ganz catheter was positioned in a pulmonary artery branch and hypertonic saline solution or a radiographic contrast agent were administered as boli through the distal or proximal openings of the catheter. During the administration through the proximal opening, the balloon at the tip of the catheter was either deflated or inflated. The latter case represented a perfusion defect. The series of EIT scans of the momentary distribution of electrical impedance within the chest were obtained during each saline bolus administration at a rate of 13/s. EBCT scans were acquired at a rate of 3.3/s during bolus administrations of the radiopaque contrast material under the same steady-state conditions. The EIT data were used to generate local time-impedance curves and functional EIT images showing the perfusion of a small lung region, both lungs with a perfusion defect and complete both lungs during bolus administration through the distal and proximal catheter opening with an inflated or deflated balloon, respectively. The results indicate that EIT imaging of lung perfusion is feasible when an electrical impedance contrast agent is used.
Objective (1) To assess the impact of high intrathoracic pressure on left ventricular volume and ... more Objective (1) To assess the impact of high intrathoracic pressure on left ventricular volume and function. (2) To test the hypothesis that right ventricular end-diastolic volume (RVEDV) and intrathoracic blood volume (ITBV) represent cardiac preload and are superior to central venous pressure (CVP) or pulmonary capillary wedge pressure (PCWP). The validity of these parameters was tested by means of correlation with left ventricular end-diastolic volume (LVEDV), the true cardiac preload. Design Prospective animal study. Subjects Fifteen adult sheep. Interventions All animals were studied before and after saline washout-induced lung injury, undergoing volume-controlled ventilation with increasing levels of PEEP (0, 7, 14 and 21 cmH2O, respectively). Measurements and main results Left ventricular ejection fraction (LVEF), stroke volume (LVSV) and LVEDV were measured using computed tomography. ITBV and RVEDV were obtained by the thermal dye dilution technique. At PEEP 21 cmH2O, LVSV significantly decreased compared to baseline, PEEP 0 and PEEP 7 cmH2O. LVEDV was maintained except for the highest level of PEEP, while LVEF remained unchanged. RVEDV and RVEF also remained unchanged. The overall correlation of RVEDV and ITBV with LVEDV was satisfactory (r=0.56 and r=0.62, respectively) and clearly superior to cardiac filling pressures. Conclusion In the present study, (1) ventilation with increasing levels of PEEP did not alter RV function, while LV function was impaired at the highest level of PEEP; (2) unlike cardiac filling pressures, ITBV and RVEDV both provide valid estimates of cardiac preload even at high intrathoracic pressures.
In our service engineering approach, services are specified by UML 2.0 collaborations and activit... more In our service engineering approach, services are specified by UML 2.0 collaborations and activities, focusing on the interactions between cooperating entities. To execute services, however, we need precise behavioral descriptions of physical system components modeling how a component contributes to a service. For these descriptions we use the concept of state machines which form a suitable input for our existing code generators that produce efficiently executable programs. From the engineering viewpoint, the gap between the collaborations and the components will be covered by UML model transformations. To ensure the correctness of these transformations, we use the compositional Temporal Logic of Actions (cTLA) which enables us to reason about service specifications and their refinement formally. In this paper, we focus on the execution of services. By outlining an UML profile, we describe which form the descriptions of the components should have to be efficiently executable. To guarantee the correctness of the design process, we further introduce the cTLA specification style cTLA/e which is behaviorally equivalent with the UML 2.0 state machines used as code generator input. In this way, we bridge the gap between UML for modeling and design, cTLA specifications used for reasoning, and the efficient execution of services, so that we can prove important properties formally.
A fundamental problem in the area of service engineering is the so-called cross-cutting nature of... more A fundamental problem in the area of service engineering is the so-called cross-cutting nature of services, i.e., that service behavior results from a collaboration of partial component behaviors. We present an approach for model-based service engineering, in which system component models are derived automatically from collaboration models. These are specifications of sub-services incorporating both the local behavior of the components and the necessary inter-component communication. The collaborations are expressed in a compact and self-contained way by UML collaborations and activities. The UML activities can express service compositions precisely, so that components may be derived automatically by means of a model transformation. In this paper, we focus on the important issue of how to coordinate and compose collaborations that are executed with several sessions at the same time. We introduce an extension to activities for session selection. Moreover, we explain how this composition is mapped onto the components and how it can be translated into executable code.
The Unified Modeling Language UML is well-suited for the design of real-time systems. In particul... more The Unified Modeling Language UML is well-suited for the design of real-time systems. In particular the design of dynamic system behaviors is supported by interaction diagrams and statecharts. Real-time aspects of behaviors can be described by time constraints. The semantics of the UML, however, is non-formal. In order to enable formal design verification, we therefore propose to complement the UML based design by additional formal models which refine UML diagrams to precise formal models. We apply the formal specification technique cTLA which is based on L. Lamport's Temporal Logic of Actions, TLA. In particular cTLA supports modular definitions of process types and the composition of systems from coupled process instances. Since process composition has superposition character each process system has all of the relevant properties of its constituting processes. Therefore mostly small subsystems are sufficient for the verification of system properties and it is not necessary to use complete and complex formal system models. We present this approach by means of an example and also exemplify the formal verification of its hard real-time properties
... The framework supplies veri ed and re-usable implications between prede ned protocol and serv... more ... The framework supplies veri ed and re-usable implications between prede ned protocol and service speci cation components. ... This leads to the idea of support-ing formal protocol speci cation and veri cation by a framework of re-usable prede ned components. ...
Component-structured software, which is coupled from independently developed software components,... more Component-structured software, which is coupled from independently developed software components, introduces new security problems. In particular, a component may attack components of its environment and, in consequence, spoil the application incorporating it. Therefore, to guard a system, we constrain the behavior of a component by ruling out the transmission of events between components which may cause harm. Security policies describing the behavior constraints are formally specified and, at runtime, so-called security wrappers monitor the interface traffic of components and check it for compliance with the specifications. Moreover, one can also use the specifications to prove formally that the combinations of the component security policies fulfill certain security properties of the complete component-structured application. A well-known method to express system security properties is access control which can be modelled by means of the popular Role Based Access Control (RBAC) method. Below, we will introduce a specification framework facilitating the formal proof that component security policy specifications fulfill RBAC-based application access control policies. The specification framework is based on the specification technique cTLA. The design of state-based security policy specifications and of RBAC-models is supported by framework libraries of specification patterns which may be instantiated and composed to a specification. Moreover, the framework contains already proven theorems facilitating the formal reasoning since a deduction proof can be reduced to proof steps which correspond directly to the theorems. In particular, we introduce the specification framework and clarify its application by means of an e-commerce example.
Tidal volume and plateau pressure limitation decreases mortality in acute respiratory distress sy... more Tidal volume and plateau pressure limitation decreases mortality in acute respiratory distress syndrome. Computed tomography demonstrated a small, normally aerated compartment on the top of poorly aerated and nonaerated compartments that may be hyperinflated by tidal inflation. We hypothesized that despite tidal volume and plateau pressure limitation, patients with a larger nonaerated compartment are exposed to tidal hyperinflation of the normally aerated compartment. Pulmonary computed tomography at end-expiration and end-inspiration was obtained in 30 patients ventilated with a low tidal volume (6 ml/kg predicted body weight). Cluster analysis identified 20 patients in whom tidal inflation occurred largely in the normally aerated compartment (69.9 +/- 6.9%; "more protected"), and 10 patients in whom tidal inflation occurred largely within the hyperinflated compartments (63.0 +/- 12.7%; "less protected"). The nonaerated compartment was smaller and the normally aerated compartment was larger in the more protected patients than in the less protected patients (p = 0.01). Pulmonary cytokines were lower in the more protected patients than in the less protected patients (p < 0.05). Ventilator-free days were 7 +/- 8 and 1 +/- 2 d in the more protected and less protected patients, respectively (p = 0.01). Plateau pressure ranged between 25 and 26 cm H(2)O in the more protected patients and between 28 and 30 cm H(2)O in the less protected patients (p = 0.006). Limiting tidal volume to 6 ml/kg predicted body weight and plateau pressure to 30 cm H(2)O may not be sufficient in patients characterized by a larger nonaerated compartment.
To evaluate whether the shape of the airway pressure-time (Paw-t) curve during constant flow infl... more To evaluate whether the shape of the airway pressure-time (Paw-t) curve during constant flow inflation corresponds to radiologic evidence of tidal recruitment or tidal hyperinflation in an experimental model of acute lung injury. Prospective randomized laboratory animal investigation. Department of Clinical Physiology, University of Uppsala, Sweden. Anesthetized, paralyzed, and mechanically ventilated pigs. Acute lung injury was induced by lung lavage. During constant inspiratory flow, the Paw-t curve was fitted to a power equation: airway pressure =a x time + c, where coefficient b (stress index) describes the shape of the curve:b = 1, straight curve; b < 1, progressive increase in slope; and b > 1, progressive decrease in slope. Tidal volume (Vt) was 6 mL/kg, and positive end-expiratory pressure was set to obtain a b value between 0.9 and 1.1 before (b = 1) and after (b = 1 after recruiting maneuver) application of a recruiting maneuver. Positive end-expiratory pressure was decreased and Vt increased to obtain 0.9 >b > 0.8 and 0.8 >b > 0.6, whereas positive end-expiratory pressure and Vt were both increased to obtain 1.3 >b > 1.1 and 1.5 >b > 1.3. Experimental conditions sequence was random. Pulmonary computed tomography was obtained during end-expiratory and end-inspiratory occlusions. Tidal recruitment was quantified as nonaerated (between -100 and +100 Hounsfield units) lung area at end-expiration minus end-inspiration. Tidal hyperinflation was quantified as hyperinflated (between -900 and -1000 Hounsfield units) lung area at end-inspiration minus end-expiration. Computed tomography images showed that tidal recruitment and tidal hyperinflation corresponded to b < 1 and b > 1, respectively. Stress index values and tidal recruitment and tidal hyperinflation values were significantly correlated (R =.917 and R =.911, p <.0001, respectively). Shape of the Paw-t curve detects tidal recruitment and tidal…
Objective To examine the effects of positive end-expiratory pressure (PEEP) on extravascular lung... more Objective To examine the effects of positive end-expiratory pressure (PEEP) on extravascular lung water (EVLW), lung tissue, and lung volume. Design and setting Experimental animal study at a university research facility. Subjects Fifteen adult sheep. Interventions All animals were studied before and after saline washout-induced lung injury while ventilated with sequentially increasing PEEP (0, 7, 14, or 21 cmH2O). Measurements and results Lung volume was determined by computed tomography and EVLW by the thermal dye dilution technique. Saline washout significantly increased lung tissue volume (21±3 to 37±5 ml/kg) and EVLW (9±2 to 36±9 ml/kg). While increasing levels of PEEP reduced EVLW (30±7, 24±8, and 18±4 ml/kg), lung tissue volume remained constant. Total lung volume significantly increased (50±8 ml/kg at PEEP 0 to 77±12 ml/kg at PEEP 21). Nonaerated lung volume significantly decreased and was closely correlated with the changes in EVLW (r=0.67). In addition, a highly significant correlation was found between PEEP-induced decrease in nonaerated lung volume and decrease in transpulmonary shunt (r=0.83). Conclusions The main findings are as follows: (a) PEEP effectively decreases EVLW. (b) The decrease in EVLW is closely correlated with the PEEP-induced decrease in nonaerated lung volume, making EVLW a valuable bedside parameter indicating alveolar recruitment, similar to measurements of transpulmonary shunt. (c) As excess tissue volume remained constant, however, EVLW may not be suitable to reflect overall severity of lung disease
The aim of the experiments was to check the feasibility of pulmonary perfusion imaging by functio... more The aim of the experiments was to check the feasibility of pulmonary perfusion imaging by functional electrical impedance tomography (EIT) and to compare the EIT findings with electron beam computed tomography (EBCT) scans. In three pigs, a Swan-Ganz catheter was positioned in a pulmonary artery branch and hypertonic saline solution or a radiographic contrast agent were administered as boli through the distal or proximal openings of the catheter. During the administration through the proximal opening, the balloon at the tip of the catheter was either deflated or inflated. The latter case represented a perfusion defect. The series of EIT scans of the momentary distribution of electrical impedance within the chest were obtained during each saline bolus administration at a rate of 13/s. EBCT scans were acquired at a rate of 3.3/s during bolus administrations of the radiopaque contrast material under the same steady-state conditions. The EIT data were used to generate local time-impedance curves and functional EIT images showing the perfusion of a small lung region, both lungs with a perfusion defect and complete both lungs during bolus administration through the distal and proximal catheter opening with an inflated or deflated balloon, respectively. The results indicate that EIT imaging of lung perfusion is feasible when an electrical impedance contrast agent is used.
Objective (1) To assess the impact of high intrathoracic pressure on left ventricular volume and ... more Objective (1) To assess the impact of high intrathoracic pressure on left ventricular volume and function. (2) To test the hypothesis that right ventricular end-diastolic volume (RVEDV) and intrathoracic blood volume (ITBV) represent cardiac preload and are superior to central venous pressure (CVP) or pulmonary capillary wedge pressure (PCWP). The validity of these parameters was tested by means of correlation with left ventricular end-diastolic volume (LVEDV), the true cardiac preload. Design Prospective animal study. Subjects Fifteen adult sheep. Interventions All animals were studied before and after saline washout-induced lung injury, undergoing volume-controlled ventilation with increasing levels of PEEP (0, 7, 14 and 21 cmH2O, respectively). Measurements and main results Left ventricular ejection fraction (LVEF), stroke volume (LVSV) and LVEDV were measured using computed tomography. ITBV and RVEDV were obtained by the thermal dye dilution technique. At PEEP 21 cmH2O, LVSV significantly decreased compared to baseline, PEEP 0 and PEEP 7 cmH2O. LVEDV was maintained except for the highest level of PEEP, while LVEF remained unchanged. RVEDV and RVEF also remained unchanged. The overall correlation of RVEDV and ITBV with LVEDV was satisfactory (r=0.56 and r=0.62, respectively) and clearly superior to cardiac filling pressures. Conclusion In the present study, (1) ventilation with increasing levels of PEEP did not alter RV function, while LV function was impaired at the highest level of PEEP; (2) unlike cardiac filling pressures, ITBV and RVEDV both provide valid estimates of cardiac preload even at high intrathoracic pressures.
In our service engineering approach, services are specified by UML 2.0 collaborations and activit... more In our service engineering approach, services are specified by UML 2.0 collaborations and activities, focusing on the interactions between cooperating entities. To execute services, however, we need precise behavioral descriptions of physical system components modeling how a component contributes to a service. For these descriptions we use the concept of state machines which form a suitable input for our existing code generators that produce efficiently executable programs. From the engineering viewpoint, the gap between the collaborations and the components will be covered by UML model transformations. To ensure the correctness of these transformations, we use the compositional Temporal Logic of Actions (cTLA) which enables us to reason about service specifications and their refinement formally. In this paper, we focus on the execution of services. By outlining an UML profile, we describe which form the descriptions of the components should have to be efficiently executable. To guarantee the correctness of the design process, we further introduce the cTLA specification style cTLA/e which is behaviorally equivalent with the UML 2.0 state machines used as code generator input. In this way, we bridge the gap between UML for modeling and design, cTLA specifications used for reasoning, and the efficient execution of services, so that we can prove important properties formally.
A fundamental problem in the area of service engineering is the so-called cross-cutting nature of... more A fundamental problem in the area of service engineering is the so-called cross-cutting nature of services, i.e., that service behavior results from a collaboration of partial component behaviors. We present an approach for model-based service engineering, in which system component models are derived automatically from collaboration models. These are specifications of sub-services incorporating both the local behavior of the components and the necessary inter-component communication. The collaborations are expressed in a compact and self-contained way by UML collaborations and activities. The UML activities can express service compositions precisely, so that components may be derived automatically by means of a model transformation. In this paper, we focus on the important issue of how to coordinate and compose collaborations that are executed with several sessions at the same time. We introduce an extension to activities for session selection. Moreover, we explain how this composition is mapped onto the components and how it can be translated into executable code.
Uploads
Papers by Peter Herrmann