title: Deconstructive replication: How to tell if a thought experiment-population pairing is fit for purpose

authors: Weijers, Dan M.

abstract: Thought experiments/scenarios are often rolled out to help answer research questions
The idea is that they tell us what people really think, value, etc. about the research question
But how do we know whether the judgments elicited are really about the research question?
Scenarios might work well for some people but not others.
What we need is a way to assess a scenario-population pairing’s fitness for purpose in relation to a particular research question

text: Deconstructive replication: How to tell if a thought experiment-population pairing is fit for purpose Thought experiments/scenarios are often rolled out to help answer research questions
The idea is that they tell us what people really think, value, etc. about the research question
But how do we know whether the judgments elicited are really about the research question?
Scenarios might work well for some people but not others.
What we need is a way to assess a scenario-population pairing’s fitness for purpose in relation to a particular research question

year: 2017

title: Model checking for cloud autoscaling using WATERS

authors: van Zijl, Martin

subjects: cloud computing

abstract: This thesis investigates the use of formal methods to verify cloud system designs against Service Level Agreements (SLAs), towards providing guarantees under uncertainty. We used WATERS (the Waikato Analysis Toolkit for Events in Reactive Systems), which is a model-checking tool based on discrete event systems. We created models for one aspect of cloud computing, horizontal autoscaling, and used this to verify cloud system designs against an SLA that specifies the maximum request response time.

To evaluate the accuracy of the WATERS models, the cloud system designs are simulated on a private Kubernetes cluster, using JMeter to drive the workload. The results from Kubernetes are compared to the verification results from WATERS. A key research goal was to have these match as closely as possible, and to explain the discrepancies between the two. This process is followed for two applications: a default installation of NGINX, a web server with a fast but variable response time, and a hand-written Node.js program enforcing a fixed response time.

The results suggest that WATERS can be used to predict potential SLA violations. Lessons learned include that the state space must be constrained to avoid excessive checking times, and we provide a method for doing so. An advantage of our model checking-based technique is that it verifies against all possible patterns of arriving requests (up to a given maximum), which would be impractical to test with a load testing tool such as JMeter.

A key difference from existing work is our use non-probabilistic finite state machines, as opposed to probabilistic models which are prevalent in existing research. In addition, we have attempted to model the detail of the autoscaling process (a “white-box” approach), whereas much existing research attempts to find patterns between autoscaling parameters and SLA violation, effectively viewing autoscaling as a black-box process.

Future work includes refining the WATERS models to more closely match Kubernetes, and modelling other SLO types. Other methods may also be used to limit the compilation and verification time for the models. This includes attempting different algorithms and perhaps editing the models to reduce the state space.

text: Model checking for cloud autoscaling using WATERS This thesis investigates the use of formal methods to verify cloud system designs against Service Level Agreements (SLAs), towards providing guarantees under uncertainty. We used WATERS (the Waikato Analysis Toolkit for Events in Reactive Systems), which is a model-checking tool based on discrete event systems. We created models for one aspect of cloud computing, horizontal autoscaling, and used this to verify cloud system designs against an SLA that specifies the maximum request response time.

To evaluate the accuracy of the WATERS models, the cloud system designs are simulated on a private Kubernetes cluster, using JMeter to drive the workload. The results from Kubernetes are compared to the verification results from WATERS. A key research goal was to have these match as closely as possible, and to explain the discrepancies between the two. This process is followed for two applications: a default installation of NGINX, a web server with a fast but variable response time, and a hand-written Node.js program enforcing a fixed response time.

The results suggest that WATERS can be used to predict potential SLA violations. Lessons learned include that the state space must be constrained to avoid excessive checking times, and we provide a method for doing so. An advantage of our model checking-based technique is that it verifies against all possible patterns of arriving requests (up to a given maximum), which would be impractical to test with a load testing tool such as JMeter.

A key difference from existing work is our use non-probabilistic finite state machines, as opposed to probabilistic models which are prevalent in existing research. In addition, we have attempted to model the detail of the autoscaling process (a “white-box” approach), whereas much existing research attempts to find patterns between autoscaling parameters and SLA violation, effectively viewing autoscaling as a black-box process.

Future work includes refining the WATERS models to more closely match Kubernetes, and modelling other SLO types. Other methods may also be used to limit the compilation and verification time for the models. This includes attempting different algorithms and perhaps editing the models to reduce the state space.

year: 2020

title: Environmental ethics in a New Zealand context

authors: Gunn, Alastair S.

subjects: environmental ethics

abstract: Environmental ethics has many strands and roots but there is increasing for a holistic approach. Such an approach, which is consistent with te ao Maori and tikanga Maori, is especially appropriate for New Zealand.

text: Environmental ethics in a New Zealand context Environmental ethics has many strands and roots but there is increasing for a holistic approach. Such an approach, which is consistent with te ao Maori and tikanga Maori, is especially appropriate for New Zealand.

year: 2007