Considering the complexity in the design of future satellites and the need for compliance with ECSS standards, the METASAT project proposes a novel design methodology based on model-based engineering and supported by open architecture hardware. The initiative highlights the potential of software vir-tualisation layers, like hypervisors, to meet standards compliance on high-performance computing platforms. Our focus is on the development of a toolchain tailored for these advanced hard-ware/software layers. In our view, without such innovation, the satellite industry may face high and unsustainable development costs and timelines, which could affect its competitiveness and reliability. This paper provides an overview of the model-based engineering toolchain, the workflow, and the digital twin concept proposed for the METASAT project. We present the purpose of each component and how they work together in the broader METASAT vision, with the objective of showing how this approach can make the development process more efficient and enhance dependability in the sector.

MOTIVATION: Model-based approaches to safety and efficacy assessment of pharmacological drugs, treatment strategies or medical devices (In Silico Clinical Trial, ISCT) aim to decrease time and cost for the needed experimentations, reduce animal and human testing, and enable precision medicine. Unfortunately, in presence of non-identifiable models (e.g. reaction networks), parameter estimation is not enough to generate complete populations of Virtual Patients (VPs), i.e. populations guaranteed to show the entire spectrum of model behaviours (phenotypes), thus ensuring representativeness of the trial. RESULTS: We present methods and software based on global search driven by statistical model checking that, starting from a (non-identifiable) quantitative model of the human physiology (plus drugs PK/PD) and suitable biological and medical knowledge elicited from experts, compute a population of VPs whose behaviours are representative of the whole spectrum of phenotypes entailed by the model (completeness) and pairwise distinguishable according to user-provided criteria. This enables full granularity control on the size of the population to employ in an ISCT, guaranteeing representativeness while avoiding over-representation of behaviours. We proved the effectiveness of our algorithm on a non-identifiable ODE-based model of the female Hypothalamic-Pituitary-Gonadal axis, by generating a population of 4 830 264 VPs stratified into 7 levels (at different granularity of behaviours), and assessed its representativeness against 86 retrospective health records from Pfizer, Hannover Medical School and University Hospital of Lausanne. The datasets are respectively covered by our VPs within Average Normalized Mean Absolute Error of 15%, 20% and 35% (90% of the latter dataset is covered within 20% error). Availability and implementation. Our open-source software is available at https://bitbucket.org/mclab/vipgenerator. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.

In Silico Clinical Trials (ISCT), i.e. clinical experimental campaigns carried out by means of computer simulations, hold the promise to decrease time and cost for the safety and efficacy assessment of pharmacological treatments, reduce the need for animal and human testing, and enable precision medicine. In this paper we present methods and an algorithm that, by means of extensive computer simulation-based experimental campaigns (ISCT) guided by intelligent search, optimise a pharmacological treatment for an individual patient (precision medicine). We show the effectiveness of our approach on a case study involving a real pharmacological treatment, namely the downregulation phase of a complex clinical protocol for assisted reproduction in humans.

One of the main goals of systems biology models in a health-care context is to individualise models in order to compute patient-specific predictions for the time evolution of species (e.g., hormones) concentrations. In this paper we present a statistical model checking based approach that, given an inter-patient model and a few clinical measurements, computes a value for the model parameter vector (model individualisation) that, with high confidence, is a global minimum for the function evaluating the mismatch between the model predictions and the available measurements. We evaluate effectiveness of the proposed approach by presenting experimental results on using the GynCycle model (describing the feedback mechanisms regulating a number of reproductive hormones) to compute patient-specific predictions for the time evolution of blood concentrations of E2 (Estradiol), P4 (Progesterone), FSH (Follicle-Stimulating Hormone) and LH (Luteinizing Hormone) after a certain number of clinical measurements.