Formalization of bond graph using higher-order-logic theorem proving.

Bond graph is a unified graphical approach for describing the dynamics of complex engineering and physical systems and is widely adopted in a variety of domains, such as, electrical, mechanical, medical, thermal and fluid mechanics. Traditionally, these dynamics are analyzed using paper-and-pencil proof methods and computer-based techniques. However, both of these techniques suffer from their inherent limitations, such as human-error proneness, approximations of results and enormous computational requirements. Thus, these techniques cannot be trusted for performing the bond graph based dynamical analysis of systems from the safety-critical domains like robotics and medicine. Formal methods, in particular, higher-order-logic theorem proving, can overcome the shortcomings of these traditional methods and provide an accurate analysis of these systems. It has been widely used for analyzing the dynamics of engineering and physical systems. In this paper, we propose to use higher-order-logic theorem proving for performing the bond graph based analysis of the physical systems. In particular, we provide formalization of bond graph, which mainly includes functions that allow conversion of a bond graph to its corresponding mathematical model (state-space model) and the verification of its various properties, such as, stability. To illustrate the practical effectiveness of our proposed approach, we present the formal stability analysis of a prosthetic mechatronic hand using HOL Light theorem prover. Moreover, to help non-experts in HOL, we encode our formally verified stability theorems in MATLAB to perform the stability analysis of an anthropomorphic prosthetic mechatronic hand.

Effects of social and emotional context on neural activation and synchrony during movie viewing.

Sharing emotional experiences impacts how we perceive and interact with the world, but the neural mechanisms that support this sharing are not well characterized. In this study, participants (N = 52) watched videos in an MRI scanner in the presence of an unfamiliar peer. Videos varied in valence and social context (i.e., participants believed their partner was viewing the same (joint condition) or a different (solo condition) video). Reported togetherness increased during positive videos regardless of social condition, indicating that positive contexts may lessen the experience of being alone. Two analysis approaches were used to examine both sustained neural activity averaged over time and dynamic synchrony throughout the videos. Both approaches revealed clusters in the medial prefrontal cortex that were more responsive to the joint condition. We observed a time-averaged social-emotion interaction in the ventromedial prefrontal cortex, although this region did not demonstrate synchrony effects. Alternatively, social-emotion interactions in the amygdala and superior temporal sulcus showed greater neural synchrony in the joint compared to solo conditions during positive videos, but the opposite pattern for negative videos. These findings suggest that positive stimuli may be more salient when experienced together, suggesting a mechanism for forming social bonds.

Formal verification of Matrix based MATLAB models using interactive theorem proving.

MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.

Formal reasoning about synthetic biology using higher-order-logic theorem proving.

Synthetic biology is an interdisciplinary field that uses well-established engineering principles for performing the analysis of the biological systems, such as biological circuits, pathways, controllers and enzymes. Conventionally, the analysis of these biological systems is performed using paper-and-pencil proofs and computer simulation methods. However, these methods cannot ensure accurate results due to their inherent limitations. Higher-order-logic (HOL) theorem proving is proposed and used as a complementary approach for analysing linear biological systems, which is based on developing a mathematical model of the genetic circuits and the bio-controllers used in synthetic biology based on HOL and analysing it using deductive reasoning in an interactive theorem prover. The involvement of the logic, mathematics and the deductive reasoning in this method ensures the accuracy of the analysis. It is proposed to model the continuous dynamics of the genetic circuits and their associated controllers using differential equations and perform their transfer function-based analysis using the Laplace transform in a theorem prover. For illustration, the genetic circuits of activated and repressed expressions and autoactivation of protein, and phase lag and lead controllers, which are widely used in cancer-cell identifiers and multi-input receptors for precise disease detection, are formally analyzed.

Toward Resilient Wireless Sensor Networks: A Virtualized Perspective.

The Internet of Things (IoT) has been one of the main focus areas of the research community in recent years, the requirements of which help network administrators to design and ensure the functionalities and resources of each device. Generally, two types of devices-constrained and unconstrained devices-are typical in the IoT environment. Devices with limited resources-for example, sensors and actuators-are known as constrained devices. Unconstrained devices includes gateways or border routers. Such devices are challenging in terms of their deployment because of their connectivity, channel selection, multiple interfaces, local and global address assignment, address resolution, remote access, mobility, routing, border router scope and security. To deal with these services, the availability of the IoT system ensures that the desired network services are available even in the presence of denial-of-service attacks, and the use of the system has become a difficult but mandatory task for network designers. To this end, we present a novel design for wireless sensor networks (WSNs) to address these challenges by shifting mandatory functionalities from unreliable to reliable and stable domains. The main contribution of our work consists in addressing the core network requirements for IoT systems and pointing out several guidelines for the design of standard virtualized protocols and functions. In addition, we propose a novel architecture which improves IoT systems, lending them more resilience and robustness, together with highlighting and some important open research topics.

Formal reasoning about systems biology using theorem proving.

System biology provides the basis to understand the behavioral properties of complex biological organisms at different levels of abstraction. Traditionally, analysing systems biology based models of various diseases have been carried out by paper-and-pencil based proofs and simulations. However, these methods cannot provide an accurate analysis, which is a serious drawback for the safety-critical domain of human medicine. In order to overcome these limitations, we propose a framework to formally analyze biological networks and pathways. In particular, we formalize the notion of reaction kinetics in higher-order logic and formally verify some of the commonly used reaction based models of biological networks using the HOL Light theorem prover. Furthermore, we have ported our earlier formalization of Zsyntax, i.e., a deductive language for reasoning about biological networks and pathways, from HOL4 to the HOL Light theorem prover to make it compatible with the above-mentioned formalization of reaction kinetics. To illustrate the usefulness of the proposed framework, we present the formal analysis of three case studies, i.e., the pathway leading to TP53 Phosphorylation, the pathway leading to the death of cancer stem cells and the tumor growth based on cancer stem cells, which is used for the prognosis and future drug designs to treat cancer patients.

Relationships of retinal structure and humphrey 24-2 visual field thresholds in patients with glaucoma.

PURPOSE: To determine relationships between spectral-domain optical coherence tomography (SD-OCT) derived regional damage to the retinal ganglion cell-axonal complex (RGC-AC) and visual thresholds for each location of the Humphrey 24-2 visual field, in all stages of open-angle glaucoma. METHODS: Patients with early, moderate, and advanced glaucoma were recruited from a tertiary glaucoma clinic. Humphrey 24-2 and 9-field Spectralis SD-OCT were acquired for each subject. Individual OCT volumes were aligned, nerve fiber layer (NFL), ganglion cell and inner plexiform layers (GCL+IPL) cosegmented. These layers were then partitioned into 54 sectors corresponding to the 24-2 grid. A Support Vector Machine was trained independently for each sector to predict the sector threshold, using these structural properties. RESULTS: One hundred twenty-two consecutive subjects, 43 early, 39 moderate, and 40 advanced, glaucoma were included (122 eyes). Average correlation coefficient (R) was 0.68 (0.47-0.82), and average root mean square error (RMSE) was 6.92 dB (3.93-8.68 dB). Prediction performance averaged over the entire field, superior hemifield, and inferior hemifield had R (RMSE) values of 0.77 (3.76), 0.80 (5.05), and 0.84 (3.80) dB, respectively. CONCLUSIONS: Predicting individual 24-2 visual field thresholds from structural information derived from nine-field SD-OCT local NFL and GCL+IPL thicknesses using the RGC-AC concept is feasible, showing the potential for the predictive ability of SD-OCT structural information for visual function. Ultimately, it may be feasible to complement and reduce the burden of subjective visual field testing in glaucoma patients with predicted function derived objectively from OCT.