Formal verification of Matrix based MATLAB models using interactive theorem proving.
Ontology highlight
ABSTRACT:
SUBMITTER: Gauhar A
PROVIDER: S-EPMC8022509 | biostudies-literature |
REPOSITORIES: biostudies-literature
Similar Datasets
Project description: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.
| S-EPMC5495343 | biostudies-literature
Project description:In interactive theorem provers (ITPs), extensible syntax is not only crucial to lower the cognitive burden of manipulating complex mathematical objects, but plays a critical role in developing reusable abstractions in libraries. Most ITPs support such extensions in the form of restrictive “syntax sugar” substitutions and other ad hoc mechanisms, which are too rudimentary to support many desirable abstractions. As a result, libraries are littered with unnecessary redundancy. Tactic languages in these systems are plagued by a seemingly unrelated issue: accidental name capture, which often produces unexpected and counterintuitive behavior. We take ideas from the Scheme family of programming languages and solve these two problems simultaneously by proposing a novel hygienic macro system custom-built for ITPs. We further describe how our approach can be extended to cover type-directed macro expansion resulting in a single, uniform system offering multiple abstraction levels that range from supporting simplest syntax sugars to elaboration of formerly baked-in syntax. We have implemented our new macro system and integrated it into the upcoming version (v4) of the Lean theorem prover. Despite its expressivity, the macro system is simple enough that it can easily be integrated into other systems. Electronic supplementary material The online version of this chapter (10.1007/978-3-030-51054-1_10) contains supplementary material, which is available to authorized users.
| S-EPMC7324063 | biostudies-literature
Project description:Autonomous vehicles are gaining popularity throughout the world among researchers and consumers. However, their popularity has not yet reached the level where it is widely accepted as a fully developed technology as a large portion of the consumer base feels skeptical about it. Proving the correctness of this technology will help in establishing faith in it. That is easier said than done because of the fact that the formal verification techniques has not attained the level of development and application that it is ought to. In this work, we present Statistical Model Checking (SMC) as a possible solution for verifying the safety of autonomous systems and algorithms. We apply it on Heuristic Autonomous Intersection Management (HAIM) algorithm. The presented verification routine can be adopted for other conflict point based autonomous intersection management algorithms as well. Along with verifying the HAIM, we also demonstrate the modeling and verification applied at each stage of development to verify the inherent behavior of the algorithm. The HAIM scheme is formally modeled using a variant of the language of Timed Automata. The model consists of automata that encode the behavior of vehicles, intersection manager (IM) and collision checkers. To verify the complete nature of the heuristic and ensure correct modeling of the system, we model it in layers and verify each layer separately for their expected behavior. Along with that, we perform implementation verification and error injection testing to ensure faithful modeling of the system. Results show with high confidence the freedom from collisions of the intersection controlled by the HAIM algorithm.
| S-EPMC7472046 | biostudies-literature
Project description:SummaryMetaboNetworks is a tool to create custom sub-networks in Matlab using main reaction pairs as defined by the Kyoto Encyclopaedia of Genes and Genomes and can be used to explore transgenomic interactions, for example mammalian and bacterial associations. It calculates the shortest path between a set of metabolites (e.g. biomarkers from a metabonomic study) and plots the connectivity between metabolites as links in a network graph. The resulting graph can be edited and explored interactively. Furthermore, nodes and edges in the graph are linked to the Kyoto Encyclopaedia of Genes and Genomes compound and reaction pair web pages.Availability and implementationMetaboNetworks is available from http://www.mathworks.com/matlabcentral/fileexchange/42684.Contactjmp111@ic.ac.uk or j.nicholson@imperial.ac.ukSupplementary informationSupplementary data are available at Bioinformatics online.
| S-EPMC3957072 | biostudies-literature
Project description:Atomic force microscopes and optical tweezers are widely used to probe the mechanical properties of individual molecules and molecular interactions, by exerting mechanical forces that induce transitions such as unfolding or dissociation. These transitions often occur under nonequilibrium conditions and are associated with hysteresis effects-features usually taken to preclude the extraction of equilibrium information from the experimental data. But fluctuation theorems allow us to relate the work along nonequilibrium trajectories to thermodynamic free-energy differences. They have been shown to be applicable to single-molecule force measurements and have already provided information on the folding free energy of a RNA hairpin. Here we show that the Crooks fluctuation theorem can be used to determine folding free energies for folding and unfolding processes occurring in weak as well as strong nonequilibrium regimes, thereby providing a test of its validity under such conditions. We use optical tweezers to measure repeatedly the mechanical work associated with the unfolding and refolding of a small RNA hairpin and an RNA three-helix junction. The resultant work distributions are then analysed according to the theorem and allow us to determine the difference in folding free energy between an RNA molecule and a mutant differing only by one base pair, and the thermodynamic stabilizing effect of magnesium ions on the RNA structure.
| S-EPMC1752236 | biostudies-literature
Project description:Organic semiconductor-based thin-film transistors' (TFTs) charge-carrier mobility has been enhanced up to 25 cm2/V s through the improvement of fabrication methods and greater understanding of the microstructure charge-transport mechanism. To expand the practical feasibility of organic semiconductor-based TFTs, their electrical properties should be easily accessed from the fully printed devices through a scalable printing method, such as a roll-to-roll (R2R) gravure. In this study, four commercially available organic semiconductors were separately formulated into gravure inks. They were then employed in the R2R gravure system (silver ink for printing gate and drain-source electrodes and BaTiO3 ink for printing dielectric layers) for printing 20 × 20 TFT-active matrix with the resolution of 10 pixels per inch on poly(ethylene terephthalate) (PET) foils to attain electrical properties of organic semiconductors a practical printing method. Electrical characteristics (mobility, on-off current ratio, threshold voltage, and transconductance) of the R2R gravure-printed 20 × 20 TFT-active matrices fabricated with organic semiconducting ink were analyzed statistically, and the results showed more than 98% device yield and 50 % electrical variations in the R2R gravure TFT-active matrices along the PET web.
| S-EPMC6644715 | biostudies-literature
Project description:Minimal physiologically-based pharmacokinetic (mPBPK) models are frequently used to model plasma PK data and utilize and yield physiologically-relevant parameters. Compared to classical compartment and whole-body PBPK modeling approaches, mPBPK models maintain a structure of intermediate physiological complexity that can be adequately informed by plasma PK data. In this tutorial, we present a MATLAb-based tool for modeling and Simulation of mPBPK models (ATLAS mPBPK) of small and large molecules. This tool enables the users to perform: i) PK data visualization, ii) simulation, iii) parameter optimization, and iv) local sensitivity analysis (SA) of mPBPK models in a simple and efficient manner. Along with the theoretical background and implementation of the different tool functionalities, this tutorial includes simulation and SA showcases of small and large molecules with and without target-mediated drug disposition. This article is protected by copyright. All rights reserved.
| S-EPMC6709424 | biostudies-literature
Project description:BackgroundTranscription factor (TF) binding site specificity is commonly represented by some form of matrix model in which the positions in the binding site are assumed to contribute independently to the site's activity. The independence assumption is known to be an approximation, often a good one but sometimes poor. Alternative approaches have been developed that use k-mers (DNA "words" of length k) to account for the non-independence, and more recently DNA structural parameters have been incorporated into the models. ChIP-seq data are often used to assess the discriminatory power of motifs and to compare different models. However, to measure the improvement due to using more complex models, one must compare to optimized matrix models.ResultsWe describe a program "Discriminative Additive Model Optimization" (DAMO) that uses positive and negative examples, as in ChIP-seq data, and finds the additive position weight matrix (PWM) that maximizes the Area Under the Receiver Operating Characteristic Curve (AUROC). We compare to a recent study where structural parameters, serving as features in a gradient boosting classifier algorithm, are shown to improve the AUROC over JASPAR position frequency matrices (PFMs). In agreement with the previous results, we find that adding structural parameters gives the largest improvement, but most of the gain can be obtained by an optimized PWM and nearly all of the gain can be obtained with a di-nucleotide extension to the PWM.ConclusionTo appropriately compare different models for TF bind sites, optimized models must be used. PWMs and their extensions are good representations of binding specificity for most TFs, and more complex models, including the incorporation of DNA shape features and gradient boosting classifiers, provide only moderate improvements for a few TFs.
| S-EPMC5840810 | biostudies-literature
Project description:Connectomics is fundamental in propelling our understanding of the nervous system's organization, unearthing cells and wiring diagrams reconstructed from volume electron microscopy (EM) datasets. Such reconstructions, on the one hand, have benefited from ever more precise automatic segmentation methods, which leverage sophisticated deep learning architectures and advanced machine learning algorithms. On the other hand, the field of neuroscience at large, and of image processing in particular, has manifested a need for user-friendly and open source tools which enable the community to carry out advanced analyses. In line with this second vein, here we propose mEMbrain, an interactive MATLAB-based software which wraps algorithms and functions that enable labeling and segmentation of electron microscopy datasets in a user-friendly user interface compatible with Linux and Windows. Through its integration as an API to the volume annotation and segmentation tool VAST, mEMbrain encompasses functions for ground truth generation, image preprocessing, training of deep neural networks, and on-the-fly predictions for proofreading and evaluation. The final goals of our tool are to expedite manual labeling efforts and to harness MATLAB users with an array of semi-automatic approaches for instance segmentation. We tested our tool on a variety of datasets that span different species at various scales, regions of the nervous system and developmental stages. To further expedite research in connectomics, we provide an EM resource of ground truth annotation from four different animals and five datasets, amounting to around 180 h of expert annotations, yielding more than 1.2 GB of annotated EM images. In addition, we provide a set of four pre-trained networks for said datasets. All tools are available from https://lichtman.rc.fas.harvard.edu/mEMbrain/. With our software, our hope is to provide a solution for lab-based neural reconstructions which does not require coding by the user, thus paving the way to affordable connectomics.
| S-EPMC10309043 | biostudies-literature
Project description:In this paper we propose a method to create data-driven mappings from components of cognitive models to brain regions. Cognitive models are notoriously hard to evaluate, especially based on behavioral measures alone. Neuroimaging data can provide additional constraints, but this requires a mapping from model components to brain regions. Although such mappings can be based on the experience of the modeler or on a reading of the literature, a formal method is preferred to prevent researcher-based biases. In this paper we used model-based fMRI analysis to create a data-driven model-brain mapping for five modules of the ACT-R cognitive architecture. We then validated this mapping by applying it to two new datasets with associated models. The new mapping was at least as powerful as an existing mapping that was based on the literature, and indicated where the models were supported by the data and where they have to be improved. We conclude that data-driven model-brain mappings can provide strong constraints on cognitive models, and that model-based fMRI is a suitable way to create such mappings.
| S-EPMC4352055 | biostudies-literature