Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “linear systems”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 1,711 records · Page 95
All sourcesNASA NTRSDOE OSTI
NASA NTRS2004

Motion of Air Bubbles in Water Subjected to Microgravity Accelerations

The International Space Station (ISS) serves as a platform for microgravity research for the foreseeable future. A microgravity environment is one in which the effects of gravity are drastically reduced which then allows physical experiments to be conducted without the overpowering effects of gravity. During his six month stay on the ISS, astronaut Donald R Pettit performed many informal/impromptu science experiments with available equipment. One such experiment focused on the motion of air bubbles in a rectangular container nearly filled with de-ionized water. Bubbles were introduced by shaking and the container was secured in place for several hours while motion of the bubbles were recorded using time-lapse photography. This paper shows correlation between bubble motion and quasi-steady acceleration levels during one such experiment operation. The quasi-steady acceleration vectors were measured by the Microgravity Acceleration Measurement System. Essentially linear motion was observed in the condition considered here. Dr. Pettit also created other conditions which produced linear and circulating motion, which are the subjects of further study. Initial observations of this bubble motion agree with calculations from many microgravity physical science experiments conducted on Shuttle microgravity science missions. Many crystal-growth furnaces involve heavy metals and high temperatures in which undesired acceleration-driven convection during solidification can adversely affect the crystal. Presented in this paper will be results showing correlation between bubble motion and the quasi-steady acceleration vector.

DeLombard, Richard↗
NASA NTRS2007

New, Improved Bulk-microphysical Schemes for Studying Precipitation Processes in WRF: Comparisons with Other Schemes - Part 1

Advances in computing power allow atmospheric prediction models to be mn at progressively finer scales of resolution, using increasingly more sophisticated physical parameterizations and numerical methods. The representation of cloud microphysical processes is a key component of these models, over the past decade both research and operational numerical weather prediction models have started using more complex microphysical schemes that were originally developed for high-resolution cloud-resolving models (CRMs). A recent report to the United States Weather Research Program (USWRP) Science Steering Committee specifically calls for the replacement of implicit cumulus parameterization schemes with explicit bulk schemes in numerical weather prediction (NWP) as part of a community effort to improve quantitative precipitation forecasts (QPF). An improved Goddard bulk microphysical parameterization is implemented into a state-of the-art of next generation of Weather Research and Forecasting (WRF) model. High-resolution model simulations are conducted to examine the impact of microphysical schemes on two different weather events (a midlatitude linear convective system and an Atllan"ic hurricane). The results suggest that microphysics has a major impact on the organization and precipitation processes associated with a summer midlatitude convective line system. The 31CE scheme with a cloud ice-snow-hail configuration led to a better agreement with observation in terms of simulated narrow convective line and rainfall intensity. This is because the 3ICE-hail scheme includes dense ice precipitating (hail) particle with very fast fall speed (over 10 m/s). For an Atlantic hurricane case, varying the microphysical schemes had no significant impact on the track forecast but did affect the intensity (important for air-sea interaction)

Tao, W.-K.↗
NASA NTRS2008

Application of Fast Multipole Methods to the NASA Fast Scattering Code

The NASA Fast Scattering Code (FSC) is a versatile noise prediction program designed to conduct aeroacoustic noise reduction studies. The equivalent source method is used to solve an exterior Helmholtz boundary value problem with an impedance type boundary condition. The solution process in FSC v2.0 requires direct manipulation of a large, dense system of linear equations, limiting the applicability of the code to small scales and/or moderate excitation frequencies. Recent advances in the use of Fast Multipole Methods (FMM) for solving scattering problems, coupled with sparse linear algebra techniques, suggest that a substantial reduction in computer resource utilization over conventional solution approaches can be obtained. Implementation of the single level FMM (SLFMM) and a variant of the Conjugate Gradient Method (CGM) into the FSC is discussed in this paper. The culmination of this effort, FSC v3.0, was used to generate solutions for three configurations of interest. Benchmarking against previously obtained simulations indicate that a twenty-fold reduction in computational memory and up to a four-fold reduction in computer time have been achieved on a single processor.

Dunn, Mark H.↗
NASA NTRS2008

Numerical Determination of Critical Conditions for Thermal Ignition

The determination of ignition or thermal explosion in an oxidizing porous body of material, as described by a dimensionless reaction-diffusion equation of the form .tu = .2u + .e-1/u over the bounded region O, is critically reexamined from a modern perspective using numerical methodologies. First, the classic stationary model is revisited to establish the proper reference frame for the steady-state solution space, and it is demonstrated how the resulting nonlinear two-point boundary value problem can be reexpressed as an initial value problem for a system of first-order differential equations, which may be readily solved using standard algorithms. Then, the numerical procedure is implemented and thoroughly validated against previous computational results based on sophisticated path-following techniques. Next, the transient nonstationary model is attacked, and the full nonlinear form of the reaction-diffusion equation, including a generalized convective boundary condition, is discretized and expressed as a system of linear algebraic equations. The numerical methodology is implemented as a computer algorithm, and validation computations are carried out as a prelude to a broad-ranging evaluation of the assembly problem and identification of the watershed critical initial temperature conditions for thermal ignition. This numerical methodology is then used as the basis for studying the relationship between the shape of the critical initial temperature distribution and the corresponding spatial moments of its energy content integral and an attempt to forge a fundamental conjecture governing this relation. Finally, the effects of dynamic boundary conditions on the classic storage problem are investigated and the groundwork is laid for the development of an approximate solution methodology based on adaptation of the standard stationary model.

Luo, W.↗
NASA NTRS2007

An Improved Bulk Microphysical Scheme for Studying Precipitation Processes: Comparisons with Other Schemes

Cloud microphysical processes play an important role in non-hydrostatic high-resolution simulations. Over the past decade both research and operational numerical weather prediction models have started using more complex cloud microphysical schemes that were originally developed for high-resolution cloud-resolving models. An improved bulk microphysical parameterization (adopted from the Goddard microphysics schemes) has recently implemented into the Weather Research and Forecasting (WRF) model. This bulk microphysical scheme has three different options --- 2ICE (cloud ice & snow), 3ICE-graupel (cloud ice, snow & graupel) and 3ICE-hail (cloud ice, snow & hail). High-resolution model simulations are conducted to examine the impact of microphysical schemes on two different weather events (a midlatitude linear convective system and an Atlantic hurricane). In addition, this bulk microphysical parameterization is compared with WIRF's three other bulk microphysical schemes.

Tao, W. K.↗
NASA NTRS2007

New, Improved Goddard Bulk-Microphysical Schemes for Studying Precipitation Processes in WRF

An improved bulk microphysical parameterization is implemented into the Weather Research and Forecasting ()VRF) model. This bulk microphysical scheme has three different options, 2ICE (cloud ice & snow), 3ICE-graupel (cloud ice, snow & graupel) and 3ICE-hail (cloud ice, snow & hail). High-resolution model simulations are conducted to examine the impact of microphysical schemes on two different weather events (a midlatitude linear convective system and an Atlantic hurricane). The results suggest that microphysics has a major impact on the organization and precipitation processes associated with a summer midlatitude convective line system. The Goddard 3ICE scheme with a cloud ice-snow-hail configuration agreed better with observations in terms of rainfall intensity and a narrow convective line than did simulations with a cloud ice-snow-graupel or cloud ice-snow (i.e., 2ICE) configuration. This is because the 3ICE-hail scheme includes dense ice precipitating (hail) particle with very fast fall speed (over 10 in For an Atlantic hurricane case, the Goddard microphysical schemes had no significant impact on the track forecast but did affect the intensity slightly. The improved Goddard schemes are also compared with WRF's three other 3ICE bulk microphysical schemes: WSM6, Purdue-Lin and Thompson. For the summer midlatitude convective line system, all of the schemes resulted in simulated precipitation events that were elongated in the southwest-northeast direction in qualitative agreement with the observed feature. However, the Goddard 3ICE scheme with the hail option and the Thompson scheme agree better with observations in terms of rainfall intensity, expect that the Goddard scheme simulated more heavy rainfall (over 48 mm/h). For the Atlantic hurricane case, none of the schemes had a significant impact on the track forecast; however, the simulated intensity using the Purdue-Lin scheme was much stronger than the other schemes. The vertical distributions of model simulated cloud species (i.e., snow) are quite sensitive to microphysical schemes, which is an important issue for future verification against satellite retrievals. Both the Purdue-Lin and WSM6 schemes simulated very little snow compared to the other schemes for both the midlatitude convective line and hurricane cases. Sensitivity tests are performed for these two WRF schemes to identify that snow productions could be increased by increasing the snow intercept, turning off the auto-conversion from snow to graupel and reducing the transfer processes from cloud-sized particles to precipitation-sized ice.

Tao, Wei-Kuo↗
NASA NTRS2008

A Systematic Methodology for Constructing High-Order Energy-Stable WENO Schemes

A third-order Energy Stable Weighted Essentially Non-Oscillatory (ESWENO) finite difference scheme developed by Yamaleev and Carpenter (AIAA 2008-2876, 2008) was proven to be stable in the energy norm for both continuous and discontinuous solutions of systems of linear hyperbolic equations. Herein, a systematic approach is presented that enables \energy stable" modifications for existing WENO schemes of any order. The technique is demonstrated by developing a one-parameter family of fifth-order upwind-biased ESWENO schemes; ESWENO schemes up to eighth order are presented in the appendix. New weight functions are also developed that provide (1) formal consistency, (2) much faster convergence for smooth solutions with an arbitrary number of vanishing derivatives, and (3) improved resolution near strong discontinuities.

Yamaleev, Nail K.↗
NASA NTRS2009

High-Order Energy Stable WENO Schemes

A third-order Energy Stable Weighted Essentially Non-Oscillatory (ESWENO) finite difference scheme developed by Yamaleev and Carpenter was proven to be stable in the energy norm for both continuous and discontinuous solutions of systems of linear hyperbolic equations. Herein, a systematic approach is presented that enables 'energy stable' modifications for existing WENO schemes of any order. The technique is demonstrated by developing a one-parameter family of fifth-order upwind-biased ESWENO schemes; ESWENO schemes up to eighth order are presented in the appendix. New weight functions are also developed that provide (1) formal consistency, (2) much faster convergence for smooth solutions with an arbitrary number of vanishing derivatives, and (3) improved resolution near strong discontinuities.

Yamaleev, Nail K.↗
NASA NTRS2009

Studying Precipitation Processes in WRF with Goddard Bulk Microphysics in Comparison with Other Microphysical Schemes

A Goddard bulk microphysical parameterization is implemented into the Weather Research and Forecasting (WRF) model. This bulk microphysical scheme has three different options, 2ICE (cloud ice & snow), 3ICE-graupel (cloud ice, snow & graupel) and 3ICE-hail (cloud ice, snow & hail). High-resolution model simulations are conducted to examine the impact of microphysical schemes on different weather events: a midlatitude linear convective system and an Atlantic hurricane. The results suggest that microphysics has a major impact on the organization and precipitation processes associated with a summer midlatitude convective line system. The Goddard 3ICE scheme with the cloud ice-snow-hail configuration agreed better with observations ill of rainfall intensity and having a narrow convective line than did simulations with the cloud ice-snow-graupel and cloud ice-snow (i.e., 2ICE) configurations. This is because the Goddard 3ICE-hail configuration has denser precipitating ice particles (hail) with very fast fall speeds (over 10 m/s) For an Atlantic hurricane case, the Goddard microphysical scheme (with 3ICE-hail, 3ICE-graupel and 2ICE configurations) had no significant impact on the track forecast but did affect the intensity slightly. The Goddard scheme is also compared with WRF's three other 3ICE bulk microphysical schemes: WSM6, Purdue-Lin and Thompson. For the summer midlatitude convective line system, all of the schemes resulted in simulated precipitation events that were elongated in southwest-northeast direction in qualitative agreement with the observed feature. However, the Goddard 3ICE-hail and Thompson schemes were closest to the observed rainfall intensities although the Goddard scheme simulated more heavy rainfall (over 48 mm/h). For the Atlantic hurricane case, none of the schemes had a significant impact on the track forecast; however, the simulated intensity using the Purdue-Lin scheme was much stronger than the other schemes. The vertical distributions of model-simulated cloud species (e.g., snow) are quite sensitive to the microphysical schemes, which is an issue for future verification against satellite retrievals. Both the Purdue-Lin and WSM6 schemes simulated very little snow compared to the other schemes for both the midlatitude convective line and hurricane case. Sensitivity tests with these two schemes showed that increasing the snow intercept, turning off the auto-conversion from snow to graupel, eliminating dry growth, and reducing the transfer processes from cloud-sized particles to precipitation-sized ice collectively resulted in a net increase in those schemes' snow amounts.

Tao, W.K.↗
NASA NTRS2008

Bounded Linear Stability Margin Analysis of Nonlinear Hybrid Adaptive Control

This paper presents a bounded linear stability analysis for a hybrid adaptive control that blends both direct and indirect adaptive control. Stability and convergence of nonlinear adaptive control are analyzed using an approximate linear equivalent system. A stability margin analysis shows that a large adaptive gain can lead to a reduced phase margin. This method can enable metrics-driven adaptive control whereby the adaptive gain is adjusted to meet stability margin requirements.

Nguyen, Nhan T.↗
NASA NTRS2009

A Systematic Methodology for Constructing High-Order Energy Stable WENO Schemes

A third-order Energy Stable Weighted Essentially Non{Oscillatory (ESWENO) finite difference scheme developed by Yamaleev and Carpenter [1] was proven to be stable in the energy norm for both continuous and discontinuous solutions of systems of linear hyperbolic equations. Herein, a systematic approach is presented that enables "energy stable" modifications for existing WENO schemes of any order. The technique is demonstrated by developing a one-parameter family of fifth-order upwind-biased ESWENO schemes; ESWENO schemes up to eighth order are presented in the appendix. New weight functions are also developed that provide (1) formal consistency, (2) much faster convergence for smooth solutions with an arbitrary number of vanishing derivatives, and (3) improved resolution near strong discontinuities.

Yamaleev, Nail K.↗
NASA NTRS2009

Boundary Closures for Fourth-order Energy Stable Weighted Essentially Non-Oscillatory Finite Difference Schemes

A general strategy exists for constructing Energy Stable Weighted Essentially Non Oscillatory (ESWENO) finite difference schemes up to eighth-order on periodic domains. These ESWENO schemes satisfy an energy norm stability proof for both continuous and discontinuous solutions of systems of linear hyperbolic equations. Herein, boundary closures are developed for the fourth-order ESWENO scheme that maintain wherever possible the WENO stencil biasing properties, while satisfying the summation-by-parts (SBP) operator convention, thereby ensuring stability in an L2 norm. Second-order, and third-order boundary closures are developed that achieve stability in diagonal and block norms, respectively. The global accuracy for the second-order closures is three, and for the third-order closures is four. A novel set of non-uniform flux interpolation points is necessary near the boundaries to simultaneously achieve 1) accuracy, 2) the SBP convention, and 3) WENO stencil biasing mechanics.

Fisher, Travis C.↗
NASA NTRS2010

Verification of Faulty Message Passing Systems with Continuous State Space in PVS

We present a library of Prototype Verification System (PVS) meta-theories that verifies a class of distributed systems in which agent commu nication is through message-passing. The theoretic work, outlined in, consists of iterative schemes for solving systems of linear equations , such as message-passing extensions of the Gauss and Gauss-Seidel me thods. We briefly review that work and discuss the challenges in formally verifying it.

Pilotto, Concetta↗
NASA NTRS2010

Analytic Development of a Reference Profile for the First Entry in a Skip Atmospheric Entry

This note shows that a feasible reference drag profile for the first entry portion of a skip entry can be generated as a polynomial expression of the velocity. The coefficients of that polynomial are found through the resolution of a system composed of m + 1 equations, where m is the degree of the drag polynomial. It has been shown that a minimum of five equations (m = 4) are required to establish the range and the initial and final conditions on velocity and flight path angle. It has been shown that at least one constraint on the trajectory can be imposed through the addition of one extra equation in the system, which must be accompanied by the increase in the degree of the drag polynomial. In order to simplify the resolution of the system of equations, the drag was considered as being a probability density function of the velocity, with the velocity as a distribution function of the drag. Combining this notion with the introduction of empirically derived constants, it has been shown that the system of equations required to generate the drag profile can be successfully reduced to a system of linear algebraic equations. For completeness, the resulting drag profiles have been flown using the feedback linearization method of differential geometric control as a guidance law with the error dynamics of a second order homogeneous equation in the form of a damped oscillator. Satisfactory results were achieved when the gains in the error dynamics were changed at a certain point along the trajectory that is dependent on the velocity and the curvature of the drag as a function of the velocity. Future work should study the capacity to update the drag profile in flight when dispersions are introduced. Also, future studies should attempt to link the first entry, as presented and controlled in this note, with a more standard control concept for the second entry, such as the Apollo entry guidance, to try to assess the overall skip entry performance. A guidance law that includes an integral feedback term, as is the case in the actual Space Shuttle entry guidance and as is proposed in Ref 29, could be tried in future studies to assess whether its use results in an improvement of the tracking performance, and to evaluate the design needs when determining the control gains.

Garcia-Llama, Eduardo↗
NASA NTRS2010

Extracting Independent Local Oscillatory Geophysical Signals by Geodetic Tropospheric Delay

Zenith Tropospheric Delay (ZTD) due to water vapor derived from space geodetic techniques and numerical weather prediction simulated-reanalysis data exhibits non-linear and non-stationary properties akin to those in the crucial geophysical signals of interest to the research community. These time series, once decomposed into additive (and stochastic) components, have information about the long term global change (the trend) and other interpretable (quasi-) periodic components such as seasonal cycles and noise. Such stochastic component(s) could be a function that exhibits at most one extremum within a data span or a monotonic function within a certain temporal span. In this contribution, we examine the use of the combined Ensemble Empirical Mode Decomposition (EEMD) and Independent Component Analysis (ICA): the EEMD-ICA algorithm to extract the independent local oscillatory stochastic components in the tropospheric delay derived from the European Centre for Medium-Range Weather Forecasts (ECMWF) over six geodetic sites (HartRAO, Hobart26, Wettzell, Gilcreek, Westford, and Tsukub32). The proposed methodology allows independent geophysical processes to be extracted and assessed. Analysis of the quality index of the Independent Components (ICs) derived for each cluster of local oscillatory components (also called the Intrinsic Mode Functions (IMFs)) for all the geodetic stations considered in the study demonstrate that they are strongly site dependent. Such strong dependency seems to suggest that the localized geophysical signals embedded in the ZTD over the geodetic sites are not correlated. Further, from the viewpoint of non-linear dynamical systems, four geophysical signals the Quasi-Biennial Oscillation (QBO) index derived from the NCEP/NCAR reanalysis, the Southern Oscillation Index (SOI) anomaly from NCEP, the SIDC monthly Sun Spot Number (SSN), and the Length of Day (LoD) are linked to the extracted signal components from ZTD. Results from the synchronization analysis show that ZTD and the geophysical signals exhibit (albeit subtle) site dependent phase synchronization index.

Botai, O. J.↗
NASA NTRS2012

The Validity Chlorophyll-a Estimation by Sun Induced Fluorescence in Estuarine Waters: An Analysis of Long-term (2003-2011) Water Quality Data from Tampa Bay, Florida (USA)

Satellite observation of phytoplankton concentration or chlorophyll-a is an important characteristic, critically integral to monitoring coastal water quality. However, the optical properties of estuarine and coastal waters are highly variable and complex and pose a great challenge for accurate analysis. Constituents such as suspended solids and dissolved organic matter and the overlapping and uncorrelated absorptions in the blue region of the spectrum renders the blue-green ratio algorithms for estimating chlorophyll-a inaccurate. Measurement of sun-induced chlorophyll fluorescence, on the other hand, which utilizes the near infrared portion of the electromagnetic spectrum, may provide a better estimate of phytoplankton concentrations. While modelling and laboratory studies have illustrated both the utility and limitations of satellite baseline algorithms based on the sun induced chlorophyll fluorescence signal, few have examined the empirical validity of these algorithms using a comprehensive long term in situ data set. In an unprecedented analysis of a long term (2003-2011) in situ monitoring data from Tampa Bay, Florida (USA), we assess the validity of the FLH product from the Moderate Resolution Imaging Spectrometer (MODIS) against chlorophyll ]a and a suite of water quality parameters taken in a variety of conditions throughout a large optically complex estuarine system. A systematic analysis of sampling sites throughout the bay is undertaken to understand how the relationship between FLH and in situ chlorophyll-a responds to varying conditions within the estuary including water depth, distance from shore and structures and eight water quality parameters. From the 39 station for which data was derived, 22 stations showed significant correlations when the FLH product was matched with in situ chlorophyll-alpha data. The correlations (r2) for individual stations within Tampa Bay ranged between 0.67 (n=28, pless than 0.01) and-0.457 (n=12, p=.016), indicating that for some areas within the Bay, FLH can be a good predictor of chlorophyll-alpha concentration and hence a useful tool for the analysis of water quality. Overall, the results show a 106% increase in the validity of chlorophyll -a concentration estimates using FLH over the standard the blue-green OC3M algorithm. This analysis also illustrates that the correlations between FLH and in situ chlorophyll -a measurements increases with increasing water depth and distance of the monitoring sites from both the shore and structures. However, due to confounding factors related to the complexity of the estuarine system, a linear improvement in the FLH to chlorophyll ]a relationship was not clearly noted with increasing depth and distance from shore alone. Correlations of FLH with turbidity, nutrients (total nitrogen and total phosphorous) biological oxygen demand, salinity, sea surface temperature correlated positively with FLH concentrations, while dissolved oxygen and pH showed negative correlations. Principle component analyses are employed to further describe the relationships between the multivariate water quality parameters and the FLH product. The majority of sites with higher and very significant correlations (pless than 0.01) also showed high correlation values for nutrients, turbidity and biological oxygen demand. These sites were on average in greater than seven meters of water and over five kilometers from shore. A thorough understanding of the relationship between the MODIS FLH product and in situ water quality parameters will enhance our understanding of the accuracy MODIS fs global FLH algorithm and assist in optimizing its calibration for use in monitoring the quality of estuarine and coastal waters worldwide.

Moreno-Madrinan, Max Jacobo↗
NASA NTRS2015

Small Body Hopper Mobility Concepts

A propellant-saving hopper mobility system was studied that could help facilitate the exploration of small bodies such as Phobos for long-duration human missions. The NASA Evolvable Mars Campaign (EMC) has proposed a mission to the moons of Mars as a transitional step for eventual Mars surface exploration. While a Mars transit habitat would be parked in High-Mars Orbit (HMO), crew members would visit the surface of Phobos multiple times for up to 14 days duration (up to 50 days at a time with logistics support). This paper describes a small body surface mobility concept that is capable of transporting a small, two-person Pressurized Exploration Vehicle (PEV) cabin to various sites of interest in the low-gravity environment. Using stored kinetic energy between bounces, a propellant-saving hopper mobility system can release the energy to vector the vehicle away from the surface in a specified direction. Alternatively, the stored energy can be retained for later use while the vehicle is stationary in respect to the surface. The hopper actuation was modeled using a variety of launch velocities, and the hopper mobility was evaluated using NASA Exploration Systems Simulations (NExSyS) for transit between surface sites of interest. A hopper system with linear electromagnetic motors and mechanical spring actuators coupled with Control Moment Gyroscope (CMG) for attitude control will use renewable electrical power, resulting in a significant propellant savings.

Phobos↗
NASA NTRS2017

MESA: Message-Based System Analysis Using Runtime Verification

In this paper, we present a novel approach and framework for run-time verication of large, safety critical messaging systems. This work was motivated by verifying the System Wide Information Management (SWIM) project of the Federal Aviation Administration (FAA). SWIM provides live air traffic, site and weather data streams for the whole National Airspace System (NAS), which can easily amount to several hundred messages per second. Such safety critical systems cannot be instrumented, therefore, verification and monitoring has to happen using a nonintrusive approach, by connecting to a variety of network interfaces. Due to a large number of potential properties to check, the verification framework needs to support efficient formulation of properties with a suitable Domain Specific Language (DSL). Our approach is to utilize a distributed system that is geared towards connectivity and scalability and interface it at the message queue level to a powerful verification engine. We implemented our approach in the tool called MESA: Message-Based System Analysis, which leverages the open source projects RACE (Runtime for Airspace Concept Evaluation) and TraceContract. RACE is a platform for instantiating and running highly concurrent and distributed systems and enables connectivity to SWIM and scalability. TraceContract is a runtime verication tool that allows for checking traces against properties specified in a powerful DSL. We applied our approach to verify a SWIM service against several requirements.We found errors such as duplicate and out-of-order messages.

Message-based System↗