-
Small brains but big challenges: white matter tractography in early life samples
Authors:
Jessica Dubois,
Mareike Grotheer,
Joseph Yuan-Mou Yang,
Jacques-Donald Tournier,
Christian Beaulieu,
Catherine Lebel
Abstract:
In the human brain, white matter development is a complex and long-lasting process involving intermingling micro-and macrostructural mechanisms, such as fiber growth, pruning and myelination. Did you know that all these neurodevelopmental changes strongly affect MRI signals, with consequences on tractography performances and reliability? This communication aims to elaborate on these aspects, highl…
▽ More
In the human brain, white matter development is a complex and long-lasting process involving intermingling micro-and macrostructural mechanisms, such as fiber growth, pruning and myelination. Did you know that all these neurodevelopmental changes strongly affect MRI signals, with consequences on tractography performances and reliability? This communication aims to elaborate on these aspects, highlighting the importance of tracking and studying the developing connections with dedicated approaches.
△ Less
Submitted 29 April, 2025;
originally announced April 2025.
-
PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller
Authors:
Ignacio D. Lopez-Miguel,
Jean-Charles Tournier,
Borja Fernandez Adiego
Abstract:
Programmable Logic Controllers (PLC) are widely used for industrial automation including safety systems at CERN. The incorrect behaviour of the PLC control system logic can cause significant financial losses by damage of property or the environment or even injuries in some cases, therefore ensuring their correct behaviour is essential. While testing has been for many years the traditional way of v…
▽ More
Programmable Logic Controllers (PLC) are widely used for industrial automation including safety systems at CERN. The incorrect behaviour of the PLC control system logic can cause significant financial losses by damage of property or the environment or even injuries in some cases, therefore ensuring their correct behaviour is essential. While testing has been for many years the traditional way of validating the PLC control system logic, CERN developed a model checking platform to go one step further and formally verify PLC logic. This platform, called PLCverif, first released internally for CERN usage in 2019, is now available to anyone since September 2020 via an open source licence. In this paper, we will first give an overview of the PLCverif platform capabilities before focusing on the improvements done since 2019 such as the larger support coverage of the Siemens PLC programming languages, the better support of the C Bounded Model Checker backend (CBMC) and the process of releasing PLCverif as an open-source software.
△ Less
Submitted 30 March, 2022;
originally announced March 2022.
-
Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program
Authors:
Borja Fernandez Adiego,
Ignacio D. Lopez-Miguel,
Jean-Charles Tournier,
Enrique Blanco,
Tomasz Ladzinski,
Frederic Havart
Abstract:
An important aspect of many particle accelerators is the constant evolution and frequent configuration changes that are needed to perform the experiments they are designed for. This often leads to the design of configurable software that can absorb these changes and perform the required control and protection actions. This design strategy minimizes the engineering and maintenance costs, but it mak…
▽ More
An important aspect of many particle accelerators is the constant evolution and frequent configuration changes that are needed to perform the experiments they are designed for. This often leads to the design of configurable software that can absorb these changes and perform the required control and protection actions. This design strategy minimizes the engineering and maintenance costs, but it makes the software verification activities more challenging since safety properties must be guaranteed for any of the possible configurations. Software model checking is a popular automated verification technique in many industries. This verification method explores all possible combinations of the system model to guarantee its compliance with certain properties or specification. This is a very appropriate technique for highly configurable software, since there is usually an enormous amount of combinations to be checked. This paper presents how PLCverif, a CERN model checking platform, has been applied to a highly configurable Programmable Logic Controller (PLC) program, the SPS Personnel Protection System (PPS). The benefits and challenges of this verification approach are also discussed.
△ Less
Submitted 30 March, 2022;
originally announced March 2022.
-
Magnetization Transfer-Mediated MR Fingerprinting
Authors:
Daniel J. West,
Gastao Cruz,
Rui P. A. G. Teixeira,
Torben Schneider,
Jacques-Donald Tournier,
Joseph V. Hajnal,
Claudia Prieto,
Shaihan J. Malik
Abstract:
Purpose: Magnetization transfer (MT) and inhomogeneous MT (ihMT) contrasts are used in MRI to provide information about macromolecular tissue content. In particular, MT is sensitive to macromolecules and ihMT appears to be specific to myelinated tissue. This study proposes a technique to characterize MT and ihMT properties from a single acquisition, producing both semiquantitative contrast ratios,…
▽ More
Purpose: Magnetization transfer (MT) and inhomogeneous MT (ihMT) contrasts are used in MRI to provide information about macromolecular tissue content. In particular, MT is sensitive to macromolecules and ihMT appears to be specific to myelinated tissue. This study proposes a technique to characterize MT and ihMT properties from a single acquisition, producing both semiquantitative contrast ratios, and quantitative parameter maps.
Theory and Methods: Building upon previous work that uses multiband radiofrequency (RF) pulses to efficiently generate ihMT contrast, we propose a cyclic-steady-state approach that cycles between multiband and single-band pulses to boost the achieved contrast. Resultant time-variable signals are reminiscent of a magnetic resonance fingerprinting (MRF) acquisition, except that the signal fluctuations are entirely mediated by magnetization transfer effects. A dictionary-based low-rank inversion method is used to reconstruct the resulting images and to produce both semiquantitative MT ratio (MTR) and ihMT ratio (ihMTR) maps, as well as quantitative parameter estimates corresponding to an ihMT tissue model.
Results: Phantom and in vivo brain data acquired at 1.5T demonstrate the expected contrast trends, with ihMTR maps showing contrast more specific to white matter (WM), as has been reported by others. Quantitative estimation of semisolid fraction and dipolar T1 was also possible and yielded measurements consistent with literature values in the brain.
Conclusions: By cycling between multiband and single-band pulses, an entirely magnetization transfer mediated 'fingerprinting' method was demonstrated. This proof-of-concept approach can be used to generate semiquantitative maps and quantitatively estimate some macromolecular specific tissue parameters.
△ Less
Submitted 23 August, 2021; v1 submitted 6 April, 2021;
originally announced April 2021.
-
Scattered slice SHARD reconstruction for motion correction in multi-shell diffusion MRI
Authors:
Daan Christiaens,
Lucilio Cordero-Grande,
Maximilian Pietsch,
Jana Hutter,
Anthony N. Price,
Emer J. Hughes,
Katy Vecchiato,
Maria Deprez,
A. David Edwards,
Joseph V. Hajnal,
J-Donald Tournier
Abstract:
Diffusion MRI offers a unique probe into neural microstructure and connectivity in the developing brain. However, analysis of neonatal brain imaging data is complicated by inevitable subject motion, leading to a series of scattered slices that need to be aligned within and across diffusion-weighted contrasts. Here, we develop a reconstruction method for scattered slice multi-shell high angular res…
▽ More
Diffusion MRI offers a unique probe into neural microstructure and connectivity in the developing brain. However, analysis of neonatal brain imaging data is complicated by inevitable subject motion, leading to a series of scattered slices that need to be aligned within and across diffusion-weighted contrasts. Here, we develop a reconstruction method for scattered slice multi-shell high angular resolution diffusion imaging (HARDI) data, jointly estimating an uncorrupted data representation and motion parameters at the slice or multiband excitation level. The reconstruction relies on data-driven representation of multi-shell HARDI data using a bespoke spherical harmonics and radial decomposition (SHARD), which avoids imposing model assumptions, thus facilitating to compare various microstructure imaging methods in the reconstructed output. Furthermore, the proposed framework integrates slice-level outlier rejection, distortion correction, and slice profile correction. We evaluate the method in the neonatal cohort of the developing Human Connectome Project (650 scans). Validation experiments demonstrate accurate slice-level motion correction across the age range and across the range of motion in the population. Results in the neonatal data show successful reconstruction even in severely motion-corrupted subjects. In addition, we illustrate how local tissue modelling can extract advanced microstructure features such as orientation distribution functions from the motion-corrected reconstructions.
△ Less
Submitted 21 April, 2020; v1 submitted 8 May, 2019;
originally announced May 2019.
-
Learning compact q-space representations for multi-shell diffusion-weighted MRI
Authors:
Daan Christiaens,
Lucilio Cordero-Grande,
Jana Hutter,
Anthony N. Price,
Maria Deprez,
Joseph V. Hajnal,
J-Donald Tournier
Abstract:
Diffusion-weighted MRI measures the direction and scale of the local diffusion process in every voxel through its spectrum in q-space, typically acquired in one or more shells. Recent developments in microstructure imaging and multi-tissue decomposition have sparked renewed attention in the radial b-value dependence of the signal. Applications in motion correction and outlier rejection therefore r…
▽ More
Diffusion-weighted MRI measures the direction and scale of the local diffusion process in every voxel through its spectrum in q-space, typically acquired in one or more shells. Recent developments in microstructure imaging and multi-tissue decomposition have sparked renewed attention in the radial b-value dependence of the signal. Applications in motion correction and outlier rejection therefore require a compact linear signal representation that extends over the radial as well as angular domain. Here, we introduce SHARD, a data-driven representation of the q-space signal based on spherical harmonics and a radial decomposition into orthonormal components. This representation provides a complete, orthogonal signal basis, tailored to the spherical geometry of q-space and calibrated to the data at hand. We demonstrate that the rank-reduced decomposition outperforms model-based alternatives in human brain data, whilst faithfully capturing the micro- and meso-structural information in the signal. Furthermore, we validate the potential of joint radial-spherical as compared to single-shell representations. As such, SHARD is optimally suited for applications that require low-rank signal predictions, such as motion correction and outlier rejection. Finally, we illustrate its application for the latter using outlier robust regression.
△ Less
Submitted 8 October, 2018; v1 submitted 17 June, 2018;
originally announced June 2018.
