Code Verification of Non-Newtonian Fluid Solvers for Single- and Two-Phase Laminar Flows

The presence of complex fluids in nature and industrial applications combined with the rapid growth of computer power over the past decades has led to an increasing number of numerical studies of non-Newtonian flows. In most cases, non-Newtonian models can be implemented in existing Newtonian solvers by relatively simple modifications of the viscosity. However, due to the scarcity of analytical solutions for non-Newtonian fluid flows and the widespread use of regularization methods, performing rigorous code verification is a challenging task. The method of manufactured solutions (MMS) is a powerful tool to generate analytical solutions for code verification. In this article, we present and discuss the results of three verification exercises based on MMS: (i) steady single-phase flow; (ii) unsteady two-phase flow with a smooth interface; (iii) unsteady two-phase flow with a free surface. The first and second exercises showed that rigorous verification of non-Newtonian fluid solvers is possible both on single- and two-phase flows. The third exercise revealed that “spurious velocities” typical of free-surface calculations with the Volume-of-Fluid model lead to “spurious viscosities” in the non-Newtonian fluid. The procedure is illustrated herein on a second-order finite volume flow solver, using the regularized Herschel-Bulkley fluid model as an example. The same methodology is however applicable to any flow solver and to all the rheological models falling under the class of generalized Newtonian fluid models.

FIRST STEPS TO COUPLED HYDRAULIC AND MECHANICAL CALCULATIONS WITHIN A PARAMETER STUDY TO DEFINE POSSIBLE CORE DESIGNS FOR THE CONVERSION OF FRM II

The Forschungs-Neutronenquelle Heinz Meier-Leibnitz (FRM II) is actively participating in the worldwide efforts on developing high-density uranium fuels in order to reduce the enrichment of fuels used in high flux research reactors. This work is part of a parameter study to define possible compatible FRM II core designs for conversion. As a first step, a code-to-code verification is performed and experimental data is used for validation. The Gambill experiment was performed in the early 1960’s in support of the HFIR program and provides results regarding the heat transfer coefficient and friction factors of water flowing through an electrically heated thin rectangular channel. A comparison is made between the Gambill Test and the results simulated by Ansys CFX and STAR-CCM+.

Verified Software Units

Modularity - the partitioning of software into units of functionality that interact with each other via interfaces - has been the mainstay of software development for half a century. In case of the C language, the main mechanism for modularity is the compilation unit / header file abstraction. This paper complements programmatic modularity for C with modularity idioms for specification and verification in the context of Verifiable C, an expressive separation logic for CompCert . Technical innovations include (i) abstract predicate declarations – existential packages that combine Parkinson & Bierman’s abstract predicates with their client-visible reasoning principles; (ii) residual predicates, which help enforcing data abstraction in callback-rich code; and (iii) an application to pure (Smalltalk-style) objects that connects code verification to model-level reasoning about features such as subtyping, self, inheritance, and late binding. We introduce our techniques using concrete example modules that have all been verified using the Coq proof assistant and combine to fully linked verified programs using a novel, abstraction-respecting component composition rule for Verifiable C.