-
Just what the doctor ordered: An evaluation of provider preference-based Instrumental Variable methods in observational studies, with application for comparative effectiveness of type 2 diabetes therapy
Authors:
Laura M. Güdemann,
Beverley M. Shields,
John M. Dennis,
Jack Bowden
Abstract:
Instrumental Variables provide a way of addressing bias due to unmeasured confounding when estimating treatment effects using observational data. As instrument prescription preference of individual healthcare providers has been proposed. Because prescription preference is hard to measure and often unobserved, a surrogate measure constructed from available data is often required for the analysis. D…
▽ More
Instrumental Variables provide a way of addressing bias due to unmeasured confounding when estimating treatment effects using observational data. As instrument prescription preference of individual healthcare providers has been proposed. Because prescription preference is hard to measure and often unobserved, a surrogate measure constructed from available data is often required for the analysis. Different construction methods for this surrogate measure are possible, such as simple rule-based methods which make use of the observed treatment patterns, or more complex model-based methods that employ formal statistical models to explain the treatment behaviour whilst considering measured confounders. The choice of construction method relies on aspects like data availability within provider, missing data in measured confounders, and possible changes in prescription preference over time. In this paper we conduct a comprehensive simulation study to evaluate different construction methods for surrogates of prescription preference under different data conditions, including: different provider sizes, missing covariate data, and change in preference. We also propose a novel model-based construction method to address between provider differences and change in prescription preference. All presented construction methods are exemplified in a case study of the relative glucose lowering effect of two type 2 diabetes treatments in observational data. Our study shows that preference-based Instrumental Variable methods can be a useful tool for causal inference from observational health data. The choice of construction method should be driven by the data condition at hand. Our proposed method is capable of estimating the causal treatment effect without bias in case of sufficient prescription data per provider, changing prescription preference over time and non-ignorable missingness in measured confounders.
△ Less
Submitted 15 August, 2023;
originally announced August 2023.
-
BlueCov: Integrating Test Coverage and Model Checking with JBMC
Authors:
Matthias Güdemann,
Peter Schrammel
Abstract:
Automated test case generation tools help businesses to write tests and increase the safety net provided by high regression test coverage when making code changes. Test generation needs to cover as much as possible of the uncovered code while avoiding generating redundant tests for code that is already covered by an existing test-suite.
In this paper we present our work on a tool for the real wo…
▽ More
Automated test case generation tools help businesses to write tests and increase the safety net provided by high regression test coverage when making code changes. Test generation needs to cover as much as possible of the uncovered code while avoiding generating redundant tests for code that is already covered by an existing test-suite.
In this paper we present our work on a tool for the real world application of integrating formal analysis with automatic test case generation. The test case generation is based on coverage analysis using the Java bounded model checker (JBMC). Counterexamples of the model checker can be translated into Java method calls with specific parameters.
In order to avoid the generation of redundant tests, it is necessary to measure the coverage in the exact same way as JBMC generates its coverage goals. Each existing coverage measurement tool uses a slightly different instrumentation and thus a different coverage criterion. This makes integration with a test case generator based on formal analysis difficult. Therefore, we developed BlueCov as a specific runtime coverage measurement tool which uses the exact same coverage criteria as JBMC does. This approach also allows for incremental test-case generation, only generating test coverage for previously untested code, e.g., to complete existing test suites.
△ Less
Submitted 30 December, 2022;
originally announced December 2022.
-
Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version)
Authors:
Eugene Goldberg,
Matthias Gudemann,
Daniel Kroening,
Rajdeep Mukherjee
Abstract:
We consider the problem of efficiently checking a set of safety properties P1,....,Pk of one design. We introduce a new approach called JA-verification where JA stands for "Just-Assume" (as opposed to "assume-guarantee"). In this approach, when proving property Pi, one assumes that every property Pj for j!=i holds. The process of proving properties either results in showing that P1,....,Pk hold wi…
▽ More
We consider the problem of efficiently checking a set of safety properties P1,....,Pk of one design. We introduce a new approach called JA-verification where JA stands for "Just-Assume" (as opposed to "assume-guarantee"). In this approach, when proving property Pi, one assumes that every property Pj for j!=i holds. The process of proving properties either results in showing that P1,....,Pk hold without any assumptions or finding a "debugging set" of properties. The latter identifies a subset of failed properties that cause failure of other properties. The design behaviors that cause the properties in the debugging set to fail must be fixed first. Importantly, in our approach, there is no need to prove the assumptions used. We describe the theory behind our approach and report experimental results that demonstrate substantial gains in performance, especially in the cases where a small debugging set exists.
△ Less
Submitted 8 March, 2018; v1 submitted 15 November, 2017;
originally announced November 2017.
-
Probabilistic Model-Based Safety Analysis
Authors:
Matthias Güdemann,
Frank Ortmeier
Abstract:
Model-based safety analysis approaches aim at finding critical failure combinations by analysis of models of the whole system (i.e. software, hardware, failure modes and environment). The advantage of these methods compared to traditional approaches is that the analysis of the whole system gives more precise results. Only few model-based approaches have been applied to answer quantitative question…
▽ More
Model-based safety analysis approaches aim at finding critical failure combinations by analysis of models of the whole system (i.e. software, hardware, failure modes and environment). The advantage of these methods compared to traditional approaches is that the analysis of the whole system gives more precise results. Only few model-based approaches have been applied to answer quantitative questions in safety analysis, often limited to analysis of specific failure propagation models, limited types of failure modes or without system dynamics and behavior, as direct quantitative analysis is uses large amounts of computing resources. New achievements in the domain of (probabilistic) model-checking now allow for overcoming this problem.
This paper shows how functional models based on synchronous parallel semantics, which can be used for system design, implementation and qualitative safety analysis, can be directly re-used for (model-based) quantitative safety analysis. Accurate modeling of different types of probabilistic failure occurrence is shown as well as accurate interpretation of the results of the analysis. This allows for reliable and expressive assessment of the safety of a system in early design stages.
△ Less
Submitted 25 June, 2010;
originally announced June 2010.
