Consensus protocols are the core of modern blockchain systems, such as the Bitcoin, Ethereum, and Algorand networks. Thanks to these protocols, participants in a blockchain network can reach consensus on which blocks to add to a blockchain, to have a consistent chain of blocks in the whole network. Blocks are typically collections of transactions, e.g., transferring currency between participants, but can contain other data depending on the use case. Consensus protocols are difficult to design, test, and implement. Problems may only manifest in rare cases but can have disastrous consequences. Formal protocol models allow exhaustive analysis and formal verification. However, formal verification is only as good as the specification of the protocol. For example, specification properties could be vacuously true, or the specification may omit to mention liveness properties that are crucial for progress in a system implementation. This thesis describes the practical validation of a formal specification of Giskard, a consensus protocol used in the PlatON network. We translated key aspects of a formal model of Giskard in the Coq proof assistant to executable Python code, and integrated them into the Sawtooth blockchain framework. Then, we ran simulations of a blockchain network executing Giskard using Sawtooth, checking network node state properties of Giskard as well as its global safety properties. Automated clients from the Sawtooth network provided randomly generated transactions as input for the network. The implementation with the test results are available for reproducibility. Both consensus safety and liveness issues were found in the formal specification of Giskard during the simulations. Based on the previous informal English specification of Giskard, we propose a new formal specification which was validated to reach consensus on blocks in the simulated blockchain network and uphold the protocol’s crash and Byzantine failure tolerance to a certain degree. The improved formal model can serve as a new basis for verifying and implementing Giskard in the future. / Konsensusprotokoll utgör kärnan i moderna blockkedjesystem som Bitcoin-, Ethereum- och Algorandnätverken. Tack vare dessa protokoll kan deltagare i blockkedjenätverk nå konsensus om vilka block som ska läggas till, för att få en konsekvent blockkedja i hela nätverket. Block är vanligen samlingar av transaktioner, till exempel överföringar av valuta mellan deltagare, men kan också innehålla annan data beroende på användningsområdet. Konsensusprotokoll är svåra att designa, testa och implementera. Problem kanske bara visar sig i sällsynta fall, men kan ha katastrofala konsekvenser. Formella protokollmodeller tillåter uttömmande analys och formell verifiering. Men formell verifiering ger bara så goda resultat som protokollspecifikationen tillåter. Till exempel kan specfikationsegenskaper vara sanna innehållslöst eller så kan specifikationen underlåta att nämna framstegsegenskaper som är viktiga för att en systemimplementation inte ska låsa sig. Denna avhandling beskriver den praktiska valideringen av en formell specifikation av Giskard, ett konsensusprotokoll som används i PlatONnätverket. Vi översatte nyckelaspekter av en formell modell i bevisassistenten Coq till körbar Python-kod och integrerade koden i blockkedjeramverket Sawtooth. Sedan körde vi simuleringar av ett blockkedjenätverk som använder Giskard med hjälp av Sawtooth och undersökte Giskards tillståndsegenskaper för nätverksnoder och även dess globala säkerhetsegenskaper. Automatiserade klienter från Sawtooth-nätverket tillhandhöll slumpgenererade transaktioner som indata för nätverket. Implementeringen med testresultaten är tillgängliga för reproducerbarhet. Både säkerhets- och framstegsproblem hittades i den formella specifikationen av Giskard under simuleringarna. Baserat på en tidigare informell specifikation av Giskard på engelska föreslår vi en ny formell specifikation som validerades att nå konsensus på block i det simulerade blockkedjenätverket och att till en viss grad tolerera krascher och byzantinska fel. Den förbättrade formella modellen kan användas som en ny bas för att verifiera och implementera Giskard i framtiden.

No description available.

No description available.

An important part of the fusion research program is to understand and control the large number of plasma instabilities that a fusion plasma can exhibit. One such instability is known as the “sawtooth” instability, which is a perturbation in the plasma electric and magnetic fields that manifests itself as periodic relaxations of the temperature and density in the plasma center. The aim of this project was to investigate how the fuel ions in a fusion plasma react to the sawtooth instability. We were able to implement a model of the plasma electromagnetic field during a sawtooth relaxation into an existing code that computes the orbits of the fuel ions in the tokamak magnetic field. To this end, it was necessary to modify the orbit code to allow for non-zero electric fields, and for time-varying fields. In order to validate the new additions to the code, we compared simulated results to analytical ones. The model of the sawtooth electromagnetic fields required for our simulations was set up within a different student project. However, due to unforeseen complications, only the magnetic (not the electric) field contribution was available to us during our project, but once the electric field is available it is straightforward to include in our code. Our simulations did not exhibit any noticeable perturbation to the particle orbit during a sawtooth crash. However, before the electric field contribution is included it is not possible to draw any physics conclusions from these results. Our code could also be used as a foundation for future projects since it is possible (with further implementations to the existing code) to simulate how the spatial profile of the neutron emission is expected to vary during the sawtooth. These simulations can be compared against experimental measurements of the neutron emission profile in order to investigate the accuracy of the sawtooth model under consideration.

The phase and amplitude gradient estimator (PAGE) method has proven successful in improving the accuracy of measured energy quantities over the p-p method, which has traditionally been used, in several applications. One advantage of the PAGE method is the use of phase unwrapping, which allows for increased measurement bandwidth above the spatial Nyquist frequency. However, phase unwrapping works best for broadband sources in free-field environments with high coherence. Narrowband sources often do not have coherent phase information over a sufficient bandwidth for a phase unwrapping algorithm to unwrap properly. In fact, phase unwrapping processing can cause significant error when there is no coherent signal near and above the spatial Nyquist frequency. However, for signals at any frequencies up to the spatial Nyquist frequency, the PAGE method provides correct intensity measurements regardless of the bandwidth of the signal. This is an improved bandwidth over the traditional method. For narrowband sources above the spatial Nyquist frequency, additional information is necessary for the PAGE method to provide accurate acoustic intensity. With sufficient bandwidth and a coherence of at least 0.1 at the spatial Nyquist frequency, a relatively narrowband source above the spatial Nyquist frequency can be unwrapped accurately. One way of using extra information, called the extrapolated PAGE method, uses the phase of a tone below the spatial Nyquist frequency and an assumption of a propagating field, and therefore linear phase, to extrapolate the phase above the spatial Nyquist frequency. Also, within certain angular and amplitude constraints, low-level broadband noise can be added to the field near a source emitting a narrowband signal above the spatial Nyquist frequency. The low-level additive broadband noise can then provide enough phase information for the phase to be correct at the frequencies of the narrowband signal. All of these methods have been shown to work in a free-field environment.

Internal gravity waves play a fundamental role in the dynamics of stably stratified regions of the atmosphere and ocean. In addition to the radiation of momentum and energy remote from generation sites, internal waves drive vertical transport of heat and mass through the ocean by wave breaking and the mixing subsequently produced. Identifying regions where internal gravity waves contribute to ocean mixing and quantifying this mixing are therefore important for accurate climate and weather predictions. Field studies report significantly enhanced measurements of turbulence near 'rough' ocean topography compared with those recorded in the ocean interior or near more gradually varying topography (e.g. Toole et al. 1997, J. Geophys. Res. 102). Such observations suggest that interaction of waves with rough topography may act to skew wave energy spectra to high wavenumbers and hence promote wave breaking and fluid mixing. This thesis examines the high wavenumber scatter and spatial partitioning of wave energy at 'rough' topography containing features that are of similar scales to those characterising incident waves. The research presented here includes laboratory experiments using synthetic schlieren and PIV to visualise two-dimensional wavefields produced by small amplitude oscillations of cylinders within linear salt-water stratifications. Interactions of wavefields with planar slopes and smoothly varying sinusoidal topography are compared with those with square-wave, sawtooth and pseudo knife-edge profiles, which have discontinuous slopes. Far-field structures of scattered wavefields are compared with linear analytical models. Scatter to high wavenumbers is found to be controlled predominantly by the relative slopes and characterising length scales of the incident wavefield and topography, as well as the shape and aspect ratio of the topographic profile. Wave energy becomes highly focused and the spectra skewed to higher wavenumbers by 'critical' regions, where the topographic slope is comparable with the slope of the incident wave energy vector, and at sharp corners, where topographic slope is not defined. Contrary to linear geometric ray tracing predictions (Longuet-Higgins 1969, J. Fluid Mech. 37), a significant back-scattered field can be achieved in near-critical conditions as well as a forward scattered wavefield in supercritical conditions, where the slope of the boundary is steeper than that of the incident wave. Results suggest that interaction with rough benthic topography could efficiently convert wave energy to higher wavenumbers and promote fluid mixing in such ocean regions.

The aim of this study is to examine the public preferences for urban riparian corridors in arid ‎regions, by testing to what extent people are willing to trade-off unmaintained ecological ‎landscape for aesthetics offered by specific micro and ‎macro environmental factors. Landscape ‎design reflects ecological and aesthetic values, and trade-offs are often made ‎between the two in ‎‎practice. In arid regions, water scarcity means riparian corridors are the ‎richest landscape ‎typology and the only ‎blue-green links for hundreds of miles. Pressure from ‎urbanization and ‎lack of eco-literacy contribute to negative ‎feedback loops which present dire ‎challenges for ‎migrating avifauna and regional wildlife. Regarding natural ‎resources and ‎biodiversity, where ‎multiple deliverable ‎ecosystem services rely on the quality and health of that ‎‎ecosystem, riparian ‎systems with high biomass are more desirable. Although this can be ‎achieved with low or no ‎‎maintenance riparian buffers, these unmaintained ecological landscapes ‎play an intrinsic role in ‎sustaining the ‎global ecosystem services and are important for the survival of the inhabitants ‎‎(avifauna). Ecological ‎landscapes are often subjected to trade-offs with aesthetic ‎landscapes that ‎include micro and ‎macro environmental factors such as manicured landscapes. It is accepted that ‎‎there is a ‎preference for aesthetics in landscape design; however, it is unclear how laypeople ‎prioritize ‎aesthetics ‎over different ecological factors in landscape scenes. This study uses a ‎Discrete Choice ‎Experiment (DCE) to elicit the ‎preferences of current or pretendant residents of ‎Jeddah City, Saudi Arabia for multiple landscape scenes. The method ‎combines ecological ‎landscape characteristics adopted from ‎the QBR index that are found in the study area in Jeddah ‎and aesthetic ‎characteristics, such as micro and macro environmental factors that are commonly ‎suggested in landscape design projects adapted from relevant visual preference studies (Alsaiari, ‎‎2018; Kenwick et al., 2009; Kuper‎ ‎,‎2017; Zhao et al., 2017). ‎DCE is a widely used method to ‎reveal preferences by analyzing the trade-offs people make ‎between ‎alternatives. Participants in ‎this study were exposed to a set of designs, which included ‎various configurations of ‎aesthetic ‎and ecological elements. Participants' choices revealed the influence of their ecological and ‎‎aesthetic values. Results show that minimal design interventions would prevent trading off the ‎ecological unmaintained landscape and that there are four subgroups with distinct homogeneous ‎preferences for the attributes affecting the appeal for the urban riparian corridor in Jeddah City. ‎Finally, results show that even though there are significant differences between subgroups based ‎on preferences, the demographic information is proportionally distributed in a way the means ‎differences diminish between the subgroups. ‎Findings in this study will equip ‎decision-makers ‎with operational definitions relating to riparian ‎landscape design and a method ‎that they can use ‎to minimize losses in ecological value over aesthetic value. This study will help‎ ‎researchers and ‎landscape architects advance visual preference research further into the domain ‎of empirical ‎‎studies.‎ ‎ / Doctor of Philosophy / Landscape architecture is a profession that entails planning and design outdoor spaces, ‎‎landmarks, and ‎structures to improve the built environment and increasing the quality of ‎‎people's lives by achieving ‎environmental, social, economic, and aesthetic outcomes‎. The ‎profession often reflects ecological and ‎aesthetic values, and trade-offs are often made ‎between ‎the two in ‎practice. These ecological values ‎represent environmental characteristics that are ‎important for the survival of wildlife (protected path ‎and safe habitat) and the overall ecosystem ‎‎(every being has a role that sustain the health of the ‎environment). Culturally, human is ‎accustomed to a slick-and-clean (tamped) looking plant within urban ‎developments (i.e., ‎neighborhoods). An example of the trade-off that often happen in practice between ‎the ‎ecological and aesthetic values is replacing an ecologically unmaintained plants that play ‎important ‎ecological role (i.e., wildlife habitat) with clean tamped plants to increase the value of ‎a real estate. Due ‎to the uncertainty surrounding people's acceptance of the features of these ‎ecological unmaintained ‎plants, especially when it entails introducing ecological riparian ‎landscape attributes within ‎neighborhoods for the first time, this dissertation focuses on both ‎assessing ecological elements ‎preferences within an urban arid region in Jeddah, Saudi Arabia ‎and assessing the extent to which ‎advanced analytical methods are capable of providing a better ‎understanding of ecological riparian ‎landscape attributes preference differences among a ‎seemingly homogenous sample of participants. ‎The increasing usage of manipulated images in ‎choice tasks inspired this dissertation. The results of the ‎study demonstrate that among the ‎relatively homogenous sample of participants that was recruited, ‎four significant preference ‎patterns have emerged, which could be used to describe and predict ‎preference for ecological ‎riparian landscape attributes and choice with great accuracy. The dissertation ‎also investigates ‎policy implications that might be beneficial in creating a ‎physical environment that ‎match public ‎preferences. ‎It also offers research implications and recommendations for landscape ‎architects ‎and urban designers on how to employ visual choice experiments, which have been well-‎‎developed in other research field