Neural source separation enables the extraction of individual spike trains from complex electrophysiological recordings. When applied to electromyographic (EMG) signals, it provides a unique window into the motor output of the nervous system by isolating the spiking activity of motor units (MUs). MU decomposition from EMG signals is currently the only scalable neural interfacing approach available in behaving humans and has become foundational in motor neuroscience and neuroprosthetics. However, unlike related domains such as spike sorting or electroencephalography (EEG) analysis, decomposition of EMG signals lacks open benchmarks that reflect the diversity of muscles, movement contexts, and noise sources encountered in practice.To address this gap, we introduce MUniverse, a modular simulation and benchmarking suite for decomposing EMG signals into individual MU spiking activity. MUniverse provides: (1) a simulation stack with a user-friendly interface to a state-of-the-art EMG generator; (2) a curated library of datasets across synthetic, hybrid synthetic-real data with ground truth spikes, and experimental EMG; (3) a set of internal and external decomposition pipelines; and (4) a unified benchmark with well-defined tasks, standard evaluation metrics, and baseline results from established decomposition pipelines.MUniverse is designed for extensibility, reproducibility, and community use, and all datasets are distributed with standardised metadata (Croissant, BIDS). By standardising evaluation and enabling dataset simulation at scale, MUniverse aims to catalyze progress on this long-standing neural signal processing problem.

Postinhibitory excitation is a transient overshoot of a neuron's baseline firing rate following an inhibitory stimulus and can be observed in vivo in human motoneurons. However, the biophysical origin of this phenomenon is still unknown and both reflex pathways and intrinsic motoneuron properties have been proposed. We hypothesized that postinhibitory excitation in motoneurons can be facilitated by hyperpolarization-activated inward currents (h-currents). Using an electrical circuit model, we investigated how h-currents can modulate the postinhibitory response of motoneurons. Further, we analyzed the spike trains of human motor units from the tibialis anterior muscle during reciprocal inhibition. The simulations revealed that the activation of h-currents by an inhibitory postsynaptic potential can cause a short-term increase in a motoneuron's firing probability. This result suggests that the neuron can be excited by an inhibitory stimulus. In detail, the modulation of the firing probability depends on the time delay between the inhibitory stimulus and the previous action potential. Further, the postinhibitory excitation's strength correlates with the inhibitory stimulus's amplitude and is negatively correlated with the baseline firing rate as well as the level of input noise. Hallmarks of h-current activity, as identified from the modeling study, were found in 50% of the human motor units that showed postinhibitory excitation. This study suggests that h-currents can facilitate postinhibitory excitation and act as a modulatory system to increase motoneuron excitability after a strong inhibition.

Contractions on the descending limb of the total (active + passive) muscle force-length relationship (i. e. when muscle stiffness is negative) are expected to lead to vast half-sarcomere-length inhomogeneities. This is however not observed in experiments-vast half-sarcomere-length inhomogeneities can be absent in myofibrils contracting in this range, and initial inhomogeneities can even decrease. Here we show that the absence of half-sarcomere-length inhomogeneities can be predicted when considering interactions of the semi-active protein titin with the actin filaments. Including a model of actin-titin interactions within a multi-scale continuum-mechanical model, we demonstrate that stability, accurate forces and nearly homogeneous half-sarcomere lengths can be obtained on the descending limb of the static total force-length relation. This could be a key to durable functioning of the muscle because large local stretches, that might harm, for example, the transverse-tubule system, are avoided.

In this work we present a verification framework for applications for the embedded system operating system Contiki, based on the software model checking tool CBMC. A challenge when verifying such systems is the modeling of the hardware environment, especially the handling of interrupts. After an introduction to the Contiki system, we discuss approaches to model interrupts at the level of hardware independent C source code and present a new modeling approach for periodically occurring interrupts. Finally, verification results for these approaches based on different Contiki applications are presented.

This paper proposes a design methodology for fault-tolerant embedded systems development that starts from software specification and goes down to hardware execution. The proposed design methodology uses formally verified and correct-by-construction software created from high-level UML statechart models for software specification and implementation. On the hardware reliability side, this paper uses the MoMa architecture for reliable embedded computing which we deploy as a soft-core onto an off-the-shelf FPGA. MoMa introduces architectural innovations that support the semantics of the UML statechart execution in a reliable fashion. The proposed design methodology is evaluated with a real automotive case study based on an exhaustive FPGA-implemented fault injection campaign.

Formally verifying a product in an early phase of the design process has several advantages. First, errors and contradictions in the specification can be found early. Second, an unambiguous common understanding of the specification is created. In summary, the quality and security of a product can be significantly increased. This paper describes how formal verification can be integrated into the industrial design process of a smart card in a practical way. The described method allows to reach high assurance levels in Common Criteria certifications.

The design of correctly implemented controls in material handling systems (MHS) is time consuming and cumbersome. The developer has to deal with an ever increasing complexity and heterogeneity of MHS on the one hand, but also with short development cycles and high demands to MHS on the other hand. For baggage handling systems (BHS) at airports, the error-free implementation of routing strategies is especially of importance, as these strategies are critical to safety. This paper proposes a compositional approach to the formal verification of routing in MHS. The approach is based on the theory of assume-guarantee reasoning, where proofs of the overall system are derived from proofs of subsystems. Moreover, the approach has been implemented in a tool that automatically carries out the verification. A real-world example is discussed in this paper, showing the benefits and scalability of the presented approach.

The design of properly working material handling systems (MHS) is a difficult process as these systems consist of a vast number of single elements with dedicated controls. While currently these systems are usually validated using simulation, formal methods provide a means to analyze the complete behavior of a system. However, these methods can often only be applied to systems of a moderate size, which hampers their application to verify real-world systems. This paper presents an approach to the compositional verification of MHS, which is based on the theory of assume-guarantee reasoning. The approach has been implemented in a tool that automatically carries out the verification. The application of the approach is shown using a real-world example.

The development of correctly working logistic systems is a tedious task. On the one hand, the developer is faced with the increasing complexity of systems and shrinking time-to-markets, but on the other hand, the need for reliability and safety of the implemented controls becomes more and more important. Formal verification techniques such as model checking allow for proving whether a system completely fulfills its specification. Existing work, though, considered only the verification of single controllers, but did not analyze the behavior of a complete logistic system. In this paper, an approach to the formal verification of material handling systems is presented. The approach is based on the definition of material handling system elements and their interconnection. Experimental results show that the approach can ensure the correct functionality of logistic systems.

For covering the real-time characteristics of an automation system during model-based design it is essential to model not only the function but also the behaviour of the control programs running on a real-time controller. This paper introduces an approach to the modelling and evaluation of the functional and time behaviour of Programmable Logic Controllers (PLC) on model level. The control algorithm consisting of UML statecharts is extended with an execution model of the controller which is also given as a statechart. The approach is integrated into a model-based design system for industrial control systems focusing on the field of production systems. An example will be employed to illustrate the benefits of a model-based design system which does incorporate real-time aspects of the controller.

Programmable logic controllers (PLCs) are applied in a wide field of application and, especially, for safety-critical controls. Thus, there is the demand for high reliability of PLCs. Moreover, the increasing complexity of the PLC programs and the short time-to-market are hard to cope with. Formal verification techniques such as model checking allow for proving whether a PLC program meets its specification. However, the manual formalization of PLC programs is error-prone and time-consuming. This paper presents a novel approach to apply model checking to machine controls. The PLC program is modeled in form of Unified Modeling Language (UML) state-charts that serve as the input to our tool that automatically generates a corresponding formal model for the model checker NuSMV. We evaluate the capabilities of the proposed approach on an industrial machine control.

Property checking is a promising approach to prove the correctness of today's complex designs. However, in practice this requires the formulation of formal properties which is a time consuming and non-trivial task. Therefore the acceptance and efficiency of formal verification techniques can be raised by an automated support for formulating design properties. In this paper we propose a new methodology to automatically generate complex properties for a given design. The tool, Dianosis, implements this methodology by analyzing a simulation trace. The extracted properties describe the abstract design behavior and are presented in a format that is easy to read and can be added to the set of properties used for formal or assertion-based verification. We provide experimental results on industrial hardware designs that show the effectiveness of Dianosis and motivate the practical use.