Spelling suggestions: "subject:"model verification"" "subject:"godel verification""
1 |
A numerical investigation of mesoscale predictabilityBeattie, Jodi C. 03 1900 (has links)
Approved for public release; distribution in unlimited. / As mesoscale models increase in resolution there is a greater need to understand predictability on smaller scales. The predictability of a model is related to forecast skill. It is possible that the uncertainty of one scale of motion can affect the other scales due to the nonlinearity of the atmosphere. Some suggest that topography is one factor that can lead to an increase of forecast skill and therefore predictability. This study examines the uncertainty of a mesoscale model and attempts to characterize the predictability of the wind field. The data collected is from the summer, when the synoptic forcing is relatively benign. Mesoscale Model 5 (MM5) lagged forecasts are used to create a three-member ensemble over a 12-hour forecast cycle. The differences in these forecasts are used to determine the spread of the wind field. Results show that some mesoscale features have high uncertainty and others have low uncertainty, shedding light on the potential predictability of these features with a mesoscale model. Results indicate that topography is a large source of uncertainty. This is seen in all data sets, contrary to other studies. The ability of the model to properly forecast the diurnal cycle also impacted substantially on the character and evolution of forecast spread. The persistent mesoscale features were represented reasonably well, however the detailed structure of these features had a fair amount of uncertainty. / Lieutenant Junior Grade, United States Navy
|
2 |
Evaluation of COAMPS performance forecasting along coast wind events during a frontal passage / Evaluation of COAMPS forecasting performance of along coast wind events during frontal passagesJames, Carl S. 03 1900 (has links)
Approved for public release, distribution is unlimited / Performance of high resolution mesoscale models has been in a continuous state of refinement since their inception. Mesoscale models have become quite skillful in forecasting synoptic scale events such as mid-latitude cyclones. However, atmospheric forcing becomes a much more complicated process when faced with the challenge of forecasting near topography along the coastline. Phenomena such as gap flows, blocked flow winds and low level stratification become important to predictability at these scales. The problem is further complicated by the dynamics of a frontal passage event. The skill of mesoscale models in predicting these winds is not as well developed. This study examines several forecasts by the Coupled Ocean Atmospheric Mesoscale Prediction System (COAMPS) during frontal passage events for the Winter of 2003-2004. An attempt is made to characterize the predictability of the wind speed and direction both before and after frontal passage along the California coast. Synoptic forcing during this time is strong due to the effects of the mid-latitude cyclones propagate across the Pacific. The study's results indicate that the wind field predictability is subject to several consistent errors associated with the passage of fronts over topography. These errors arise due to difficulty in the model capturing weak thermal advection events and topographic wind funneling. The deficiencies in model representation of topography contributes to these errors. / Lieutenant, United States Navy
|
3 |
Multimodelové srovnání kvality předpovědi počasí / Multimodel weather forecast comparisonŽáček, Ondřej January 2018 (has links)
This thesis analyses comparison and verification of three global numeric weather models, GFS, ECMWF, NEMS. The research subjects are make comparison of their 48-hour forecast with, for this thesis created, index correspondence of models and evaluate predictability of weather. Next, introduce basic verification methods and their application to forecast verification, from previously mentioned models, against surface observations with resolution 2 ř x 2 ř lat/lon between 1. 6. 2017-28. 2. 2018. Results show, that the worst predictability is at areas with continental glaciers, extensive world mountain ranges and at ITCZ area. The best predictability is observed in subtropical anticyclones over the oceans. Verification of temperature we find out significant smoothing of diurnal cycle in all three models. Biases of relative humidity are strongly negative corelated with temperature bias, skill score for relative humidity is worse than for temperature. Performance of mean sea level pressure is the best for all verification metrics from all analysed quantities. Wind speed is for most world overestimated. Results of 3-hour precipitation depends on treshold. Models overestimate frequency of low intensity precipitation, opposite results are observed for high intensity precipitation, break occur at interval...
|
4 |
Multi-Model Heterogeneous Verification of Cyber-Physical SystemsRajhans, Akshay H. 01 May 2013 (has links)
Complex systems are designed using the model-based design paradigm in which mathematical models of systems are created and checked against specifications. Cyber-physical systems (CPS) are complex systems in which the physical environment is sensed and controlled by computational or cyber elements possibly distributed over communication networks. Various aspects of CPS design such as physical dynamics, software, control, and communication networking must interoperate correctly for correct functioning of the systems. Modeling formalisms, analysis techniques and tools for designing these different aspects have evolved independently, and remain dissimilar and disparate. There is no unifying formalism in which one can model all these aspects equally well. Therefore, model-based design of CPS must make use of a collection of models in several different formalisms and use respective analysis methods and tools together to ensure correct system design. To enable doing this in a formal manner, this thesis develops a framework for multi-model verification of cyber-physical systems based on behavioral semantics.
Heterogeneity arising from the different interacting aspects of CPS design must be addressed in order to enable system-level verification. In current practice, there is no principled approach that deals with this modeling heterogeneity within a formal framework. We develop behavioral semantics to address heterogeneity in a general yet formal manner. Our framework makes no assumptions about the specifics of any particular formalism, therefore it readily supports various formalisms, techniques and tools. Models can be analyzed independently in isolation, supporting separation of concerns. Mappings across heterogeneous semantic domains enable associations between analysis results. Interdependencies across different models and specifications can be formally represented as constraints over parameters and verification can be carried out in a semantically consistent manner. Composition of analysis results is supported both hierarchically across different levels of abstraction and structurally into interacting component models at a given level of abstraction. The theoretical concepts developed in the thesis are illustrated using a case study on the hierarchical heterogeneous verification of an automotive intersection collision avoidance system.
|
5 |
A model-based reasoning architecture for system-level fault diagnosisSaha, Bhaskar 04 January 2008 (has links)
This dissertation presents a model-based reasoning architecture with a two fold purpose: to detect and classify component faults from observable system behavior, and to generate fault propagation models so as to make a more accurate estimation of current operational risks. It incorporates a novel approach to system level diagnostics by addressing the need to reason about low-level inaccessible components from observable high-level system behavior. In the field of complex system maintenance it can be invaluable as an aid to human operators.
The first step is the compilation of the database of functional descriptions and associated fault-specific features for each of the system components. The system is then analyzed to extract structural information, which, in addition to the functional database, is used to create the structural and functional models. A fault-symptom matrix is constructed from the functional model and the features database. The fault threshold levels for these symptoms are founded on the nominal baseline data. Based on the fault-symptom matrix and these thresholds, a diagnostic decision tree is formulated in order to intelligently query about the system health. For each faulty candidate, a fault propagation tree is generated from the structural model. Finally, the overall system health status report includes both the faulty components and the associated at risk components, as predicted by the fault propagation model.
|
6 |
Modelling the cutting process and cutting performance in abrasive waterjet machining with controlled nozzle oscillationXu, Shunli January 2006 (has links)
Abrasive waterjet (AWJ) cutting is one of the most recently developed manufacturing technologies. It is superior to many other cutting techniques in processing various materials, particularly in processing difficult-to-cut materials. This technology is being increasingly used in various industries. However, its cutting capability in terms of the depth of jet penetration and kerf quality is the major obstruction limiting its further applications. More work is required to fully understand the cutting process and cutting mechanism, and to optimise cutting performance. This thesis presents a comprehensive study on the controlled nozzle oscillation technique aiming at increasing the cutting performance in AWJ machining. In order to understand the current state and development in AWJ cutting, an extensive literature review is carried out. It has found that the reported studies on controlled nozzle oscillation cutting are primarily about the use of large oscillation angles of 10 degrees or more. Nozzle oscillation in the cutting plane with such large oscillation angles results in theoretical geometrical errors on the component profile in contouring. No published attempt has been found on the study of oscillation cutting under small angles although it is a common application in practice. Particularly, there is no reported research on the integration of nozzle oscillation technique into AWJ multipass cutting, which is expected to significantly enhance the cutting performance. An experimental investigation is first undertaken to study the major cutting performance measures in AWJ single pass cutting of an 87% alumina ceramic with controlled nozzle oscillation at small angles. The trends and characteristics of cutting performance quantities with respect to the process parameters as well as the science behind which nozzle oscillation affects the cutting performance have been analysed. It has been shown that as with oscillation cutting at large angles, oscillation at small angles can have an equally significant impact on the cutting performance. When the optimum cutting parameters are used for both nozzle oscillation and normal cutting, the former can statistically increase the depth of cut by 23% and smooth depth of cut by 30.8%, and reduce kerf surface roughness by 11.7% and kerf taper by 54%. It has also been found that if the cutting parameters are not selected properly, nozzle oscillation can reduce some major cutting performance measures. In order to correctly select the process parameters and to optimise the cutting process, the mathematical models for major cutting performance measures have then been developed. The predictive models for the depth of cut in both normal cutting and oscillation cutting are developed by using a dimensional analysis technique. Mathematical models for other major cutting performance measures are also developed with the aid of empirical approach. These mathematical models are verified both qualitatively and quantitatively based on the experimental data. The assessment reveals that the developed models conform well to the experimental results and can provide an effective means for the optimum selection of process variables in AWJ cutting with nozzle oscillation. A further experimental investigation of AWJ cutting of alumina ceramics is carried out in order to study the application of AWJ oscillation technique in multipass cutting. While high nozzle traverse speed with multipass can achieve overall better cutting performance than low traverse speed with single pass in the same elapsed time, it has been found that the different combination of nozzle traverse speed with the number of passes significantly affects cutting process. Optimum combination of nozzle traverse speed with the number of passes is determined to achieve maximum depth of cut. It has also demonstrated that the multipass cutting with low nozzle traverse speed in the first pass and a comparatively high traverse speed for the following passes is a sensible choice for a small kerf taper requirement. When nozzle oscillation is incorporated into multipass cutting, it can greatly increase the depth of cut and reduce kerf taper. The predictive models for the depth of cut in both multipass normal cutting and multipass oscillation cutting are finally developed. With the help of dimensional analysis, the models of the incremental cutting depth for individual pass are derived based on the developed depth of cut models for single pass cutting. The models of depth of cut for a multipass cutting operation are then established by the sum of the incremental cutting depth from each pass. A numerical analysis has verified the models and demonstrated the adequacy of the models' predictions. The models provide an essential basis for the development of optimization strategies for the effective use of the AWJ cutting technology when the multipass cutting technique is used with controlled nozzle oscillation.
|
7 |
Pragmatic model verification / Vérification pragmatique de modèlesGonzalez Perez, Carlos Alberto 09 October 2014 (has links)
L’Ingénierie Dirigée par les Modèles (IDM) est une approche populaire pour le développement logiciel qui favorise l’utilisation de modèles au sein des processus de développement. Dans un processus de développement logiciel base sur l’IDM, le logiciel est développé en créant des modèles qui sont transformés successivement en d’autres modèles et éventuellement en code source. Quand l’IDM est utilisée pour le développement de logiciels complexes, la complexité des modèles et des transformations de modèles augmente, risquant d’affecter la fiabilité du processus de développement logiciel ainsi que le logiciel en résultant.Traditionnellement, la fiabilité des logiciels est assurée au moyen d’approches pour la vérification de logiciels, basées sur l’utilisation de techniques pour l’analyse formelle de systèmes et d’approches pour le test de logiciels. Pour assurer la fiabilité du processus IDM de développement logiciel, ces techniques ont en quelque sorte été adaptées pour essayer de s’assurer la correction des modèles et des transformations de modèles associées. L’objectif de cette thèse est de fournir de nouveaux mécanismes améliorant les approches existantes pour la vérification de modèles statiques, et d’analyser comment ces approches peuvent s’avérer utiles lors du test des transformations de modèles. / Model-Driven Engineering (MDE) is a popular approach to the development of software which promotes the use of models as first-Class citizens in the software development process. In a MDE-Based software development process, software is developed by creating models to be successively transformed into another models and eventually into the software source code. When MDE is applied to the development of complex software systems, the complexity of models and model transformations increase, thus risking both, the reliability of the software development process and the soundness of the resulting software. Traditionally, ensuring software correctness and absence of errors has been addressed by means of software verification approaches, based on the utilization of formal analysis techniques, and software testing approaches. In order to ensure the reliability of MDE-Based software development processes, these techniques have some how been adapted to try to ensure correctness of models and model transformations. The objective of this thesis is to provide new mechanisms to improve the landscape of approaches devoted to the verification of static models, and analyze how these static model verification approaches can be of assistance at the time of testing model transformations.
|
8 |
Analys av simulation för implementationer i en automatiserad verkstad / Analysis of simulation for implementations in an automated workshopKärrbrant, Robert, Labriz, Daniel January 2019 (has links)
En verkstad som tillverkar växellådor planerade att bygga om verkstaden. Det fanns flera problem i verkstaden som indirekt påverkade produktionen. Att tåg stod stilla utan att göra ett aktivt arbete på en huvudled i verkstaden sågs som ett stort problem. Ett annat problem var att det fanns för många tåg i verkstaden. Den planerade ombyggnationen var till för att få ned antalet tåg i verkstaden. Med ombyggnationen ville verkstadens ansvariga undersöka ytterligare möjligheter hur verkstaden skulle kunna förändras och kunna lösa delar av problemen. Det var även intressant att se om möjliga implementeringar av verkstaden skulle ge en ökad produktion. Målen var att skapa ett simuleringsverktyg för att undersöka hur olika lösningar som baserades på ombyggnationen skulle kunna påverka ett tåg som fyllde på material till monteringslinor i verkstaden. För att kunna testa olika lösningar behövde en simuleringsmodell utvecklas och verifieras mot den befintliga lösningen i verkstaden. Därefter utökades modellen för att testa nya lösningar. Från verkstaden fanns det data på konsumering av material. För tåget som skulle fylla på material fanns det teoretiska tider för olika arbetsmoment. Konsumeringen av material uppförde sig enligt en slumpfördelning som var normalfördelad. Resultatet blev att endast konsumeringen av material kunde verifieras då det bara fanns data på hur konsumtionen av material skedde. Resterande delar av simuleringen använde teoretiska planerade värden. Av de undersökta lösningarna var det en lösning med en ny hållplats på en mindre trafikerad väg, där ett tåg kunde vänta, som visade ett mer önskat resultat än de andra som undersöktes. / A workshop that produces gearboxes planned to remodel the workshop. There were several problems that indirectly affected the production. The fact that trains stood still without doing active work on the main road in the workshop was a major problem. Another problem was that there were too many trains in the workshop. The planned reconstruction was to reduce the number of trains in the workshop. With the remodel, those responsible for the workshop wanted to explore further possibilities on how the workshop could be changed. It was also interesting to see if the implementation of changes would give an increased production. The goals were to create a simulation tool to investigate how different solutions based on the rebuild could affect a train that loaded the material into assembly lines in the workshop. To be able to test different solutions, a simulation model needed to be developed and verified against the existing solution. Then the model was expanded to test new solutions. From the workshop there was data on the consumption of materials. For the train that would load up on materials, there were theoretical times for various work tasks. The consumption of materials behaved according to a random distribution that was normally distributed. The result was that only the consumption of materials could be verified as there was only data on how the consumption of materials took place. Remaining parts of the simulation used theoretically planned values. Of the solutions investigated, it was a solution with a new bus stop on a less busy road, where a train could wait, that showed a more desirable result than the others that were investigated.
|
9 |
Assessment of Single Crystal X-ray Diffraction Data QualityKrause, Lennard 02 March 2017 (has links)
No description available.
|
10 |
Contribution aux communications intra-véhicule et inter-véhicules / Contribution to Intra-Vehicular and Inter-Vehicular CommunicationsAyaida, Marwane 10 December 2012 (has links)
Les véhicules modernes sont équipés de périphériques permettant d'automatiser des tâches (changement de vitesse de transmission, régulation de vitesse, etc.) ou de fournir des services à l'utilisateur (aide à la conduite, détection d'obstacles, etc.). Les communications entre les véhicules permettent d'élargir ces services grâce à la collaboration de plusieurs véhicules (prévention des accidents, gestion du trafic routier, etc.). La multiplication de ces périphériques, de leurs interfaces et protocoles rend l'échange de données plus complexe. Par ailleurs, la communication inter- véhicules est plus contraignante à cause de la haute mobilité des véhicules. Dans cette thèse, nous proposons la conception d'un canal de communication Connect to All (C2A) qui permet d'assurer l'interopérabilité entre les périphériques embarqués dans un véhicule. En effet, il détecte la connexion à chaud d'un équipement, le reconnaît et lui permet d'échanger des données avec les autres périphériques connectés. La conception du canal commence par la modélisation de ce canal en utilisant deux techniques différentes (l'outil de modélisation et de vérification UPPAAL et le Langage de Description et de Spécification (LDS)). La vérification des modèles proposés a pour but de valider le fonctionnement. Ensuite, nous détaillons une implémentation réelle du canal sur une carte embarquée qui vise à démontrer la faisabilité du concept d'interopérabilité de C2A.Nous avons aussi étudié les effets de la mobilité dans la communication inter-véhiculaires grâce à une approche hybride mixant le routage et un service de localisation. Cette approche offre un mécanisme qui permet de réduire les coûts de la localisation des véhicules tout en augmentant les performances de routage. En plus, nous comparons deux applications de cette approche : Hybrid Routing and Grid Location Service (HRGLS) et Hybrid Routing and Hierarchical Location Service (HRHLS) avec des approches originelles pour démontrer la valeur ajoutée. Cette approche est enrichie avec un algorithme de prédiction de mobilité. Ce dernier permet de mieux cerner le déplacement des véhicules en les estimant. De même, l'approche hybride avec prédiction de mobilité Predictive Hybrid Routing and Hierarchical Location Service (PHRHLS) est comparée à HRHLS et l'approche originelle afin de révéler les bénéfices de la prédiction de mobilité. / Modern vehicles are equipped with various devices that aim to automate tasks (shift transmission, cruise control, etc.) or to provide services to the user (driver assistance, obstacle detection, etc.). Communications between vehicles help to expand these services through the collaboration of several vehicles (accident prevention, traffic management, etc.). The proliferation of these devices, their interfaces and protocols makes the data exchange more complex. In addition, inter-vehicle communication is more restrictive because of the vehicles' high mobility.In this work, we propose the design of a communication channel Connect to All (C2A) that ensures the interoperability between embedded devices in a vehicle. In fact, it detects the equipment connection, recognizes it and allows it to exchange data with other devices. The channel design starts by the modelling step using two different techniques (the model checker tool UPPAAL and the Specification and Description Language (SDL). Then, we validate the designed models. We also detail a concrete implementation of the channel on an embedded chip that aims to show the C2A interoperability concept feasibility.We also studied the mobility effects in the inter-vehicular communication through a hybrid approach mixing routing and location-based service. This approach provides a mechanism to reduce vehicle-tracking costs while increasing routing performances. Moreover, we compare two applications of this approach: Hybrid Routing and Grid Location Service (HRGLS) and Hybrid Routing and Hierarchical Location Service (HRHLS) with classical approaches to prove the added value. Then, this approach is improved with a mobility prediction algorithm. The latter allows a better understanding of the vehicle movements by estimating them. Similarly, the hybrid approach with mobility prediction Predictive Hybrid Routing and Hierarchical Location Service (PHRHLS) is compared with the basic approach and HRHLS in order to show the mobility prediction advantages.
|
Page generated in 0.1168 seconds