Software for space applications has special requirements in terms of reliability and dependability. As the verification & validation activities (VAs) of these software systems account for more than 50% of the development effort and the industry is faced with political and market pressure to deliver software faster and cheaper, new ways need to be established to reduce this verification & validation effort. In a research project together with RUAG Aerospace Sweden AB and the Swedish Space Corporation, the Blekinge Tekniska Högskola is trying to find out how to optimize the VAs with respect to effectiveness and efficiency. The goal of this thesis is therefore to develop a coherent framework for the management and optimization of verification & validation activities (VAMOS) and is evaluated at the RUAG Aerospace Sweden AB in Göteborg.

Formal methods is a discipline of using a collection of mathematical techniques and formalisms to model and analyze software systems. Motivated by the new formal methods-based certification recommendations for safety-critical embedded software and the significant increase in the cost of verification and validation (V\&V), this research is about creating a software development process for control systems that can provide mathematical guarantees of high-level functional properties on the code. The process, dubbed credible autocoding, leverages control theory in the automatic generation of control software documented with proofs of their stability and performance. The main output of this research is an automated, credible autocoding prototype that transforms the Simulink model of the controller into C code documented with a code-level proof of the stability of the controller. The code-level proof, expressed using a formal specification language, are embedded into the code as annotations. The annotations guarantee that the auto-generated code conforms to the input model to the extent that key properties are satisfied. They also provide sufficient information to enable an independent, automatic, formal verification of the auto-generated controller software.

Computational Fluid Dynamics (CFD) is increasingly being used in nuclear reactor safety analysis as a tool that enables safety related physical phenomena occurring in the reactor coolant system to be described in more detail and accuracy. Validation is a necessary step in improving predictive capability of a computationa code or coupled computational codes. Validation refers to the assessment of model accuracy incorporating any uncertainties (aleatory and epistemic) that may be of importance. The uncertainties must be identi ed, quanti ed and if possible, reduced. In the rst part of this thesis, a discussion on the development of an approach and experimental facility for the validation of coupled Computational Fluid Dynamics codes and System Thermal Hydraulics (STH) codes is given. The validation of a coupled code requires experiments which feature signi cant two-way feedbacks between the component (CFD sub-domain) and the system (STH sub-domain). Results of CFD analysis that are used in the development of a exible design of the TALL-3D experimental facility are presented. The facility consists of a lead-bismuth eutectic (LBE) thermal-hydraulic loop operating in forced and natural circulation regimes with a heated pool-type 3D test section. Transient analysis of the mixing and strati cation phenomena in the 3D test section under forced and natural circulation conditions in the loop show that the test section outlet temperature deviates from that predicted by analytical solution (which the 1D STH solution essentially is). Also an experimental validation test matrix according to the key physical phenomena of interest in the new experimental facility is developed. In the second part of the thesis we consider the risk related to steam generator tube leakage or rupture (SGTL/R) in a pool-type design of lead-cooled reactor (LFR). We demonstrate that there is a possibility that small steam bubbles leaking from the SGT will be dragged by the turbulent coolant ow into the core region. Voiding of the core might cause threats of reactivity insertion accident or local damage (burnout) of fuel rod cladding. Trajectories of the bubbles are determined by the bubble size and turbulent ow eld of lead coolant. The main objective of such study is to quantify likelihood of steam bubble transport to the core region in case of SGT leakage in the primary coolant system of the ELSY (European Lead-cooled SYstem) design. Coolant ow eld and bubble motion are simulated by CFD code Star-CCM+. First, we discuss drag correlations for a steam bubble moving in liquid lead. Thereafter the steady state liquid lead ow eld in the primary system is modeled according to the ELSY design parameters of nominal full power operation. Finally, the consequences of SGT leakage are modeled by injecting bubbles in the steam generator region. An assessment of the probability that bubbles can reach the core region and also accumulate in the primary system, is performed. The most dangerous leakage positions in the SG and bubble sizes are identi ed. Possible design solutions for prevention of core voiding in case of SGTL/R are discussed.

Mathematical models of regulatory networks become more difficult to construct and understand as they grow in size and complexity. Large regulatory network models can be built up from smaller models, representing subsets of reactions within the larger network. This dissertation focuses on novel model construction techniques that extend the ability of biological modelers to construct larger models by supplying them with tools for decomposing models and using the resulting components to construct larger models. Over the last 20 years, molecular biologists have amassed a great deal of information about the genes and proteins that carry out fundamental biological processes within living cells --- processes such as growth and reproduction, movement, signal reception and response, and programmed cell death. The full complexity of these macromolecular regulatory networks is too great to tackle mathematically at the present time. Nonetheless, modelers have had success building dynamical models of restricted parts of the network. Systems biologists need tools now to support composing "submodels" into more comprehensive models of integrated regulatory networks. We have identified and developed four novel processes (fusion, composition, flattening, and aggregation) whose purpose is to support the construction of larger models. Model Fusion combines two or more models in an irreversible manner. In fusion, the identities of the original (sub)models are lost. Beyond some size, fused models will become too complex to grasp and manage as single entities. In this case, it may be more useful to represent large models as compositions of distinct components. In Model Composition one thinks of models not as monolithic entities but rather as collections of smaller components (submodels) joined together. A composed model is built from two or more submodels by describing their redundancies and interactions. While it is appealing in the short term to build larger models from pre-existing models, each developed independently for their own purposes, we believe that ultimately it will become necessary to build large models from components that have been designed for the purpose of combining them. We define Model Aggregation as a restricted form of composition that represents a collection of model elements as a single entity (a "module"). A module contains a definition of pre-determined input and output ports. The process of aggregation (connecting modules via their interface ports) allows modelers to create larger models in a controlled manner. Model Flattening converts a composed or aggregated model with some hierarchy or connections to one without such connections. The relationships used to describe the interactions among the submodels are lost, as the composed or aggregated model is converted into a single large (flat) model. Flattening allows us to use existing simulation tools, which have no support for composition or aggregation. / Ph. D.

La simulation multi-disciplinaire et multi-physique représente un enjeu scientifique et industriel majeur. La simulation a été essentiellement traitée par les physiciens (mécanique, électromagnétique, ...) comme un problème numérique sur des cas d'étude très précis mais n'a jamais été abordée d'un point de vue système. La problématique générale posée par la simulation de systèmes complexes inclut la composition des modèles, l'optimisation multi-objectifs, la sémantique et la vérification formelle des compositions et le cadre offert par l'ingénierie système. Cette thèse propose une démarche originale établissant les fondements théoriques et méthodologiques pour un processus sans rupture entre ingénierie système, optimisation multi-objectif et simulation multi-physique. Des cas d'études issus de l'automobile démontrent la validité de cette approche expérimentée sur la base du langage Modelica. / Multi-disciplinary and multi-physics simulation represents a major scientific and industrial challenge. The simulation has essentially been considered by physicists (mechanic domain, electromagnetic domain, ...) as a numerical problem on specific case studies but has never been adressed from a system perspective. The general problem induced by the numerical simulation of complex systems include model composition, multi-objective optimization, the semantics and formal verification of compositions and the frame of systems engineering. This thesis proposes an original approach establishing the theoretical and methodological foundations for a seamless process between systems engineering, multi-objective optimization and multi-physics simulation. Automotive case studies show the validity of such an approach based on Modelica langage.