Browse
Submit Data
Databases
API
Help

Dataset Information

26 Views

0 Connections

0 Citations

0 Reanalyses

0 Downloads

Omics score: 0

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

ABSTRACT: 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.

SUBMITTER: Gauhar A

PROVIDER: S-EPMC8022509 | biostudies-literature |

REPOSITORIES: biostudies-literature

ACCESS DATA

Json Xml

Similar Datasets

Formal reasoning about systems biology using theorem proving.

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

Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

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

Formal Verification of Heuristic Autonomous Intersection Management Using Statistical Model Checking.

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

MetaboNetworks, an interactive Matlab-based toolbox for creating, customizing and exploring sub-networks from KEGG.

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

Verification of the Crooks fluctuation theorem and recovery of RNA folding free energies.

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

Proving Scalability of an Organic Semiconductor To Print a TFT-Active Matrix Using a Roll-to-Roll Gravure.

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

ATLAS mPBPK: a MATLAb-based tool for modeling and Simulation of minimal Physiologically Based PharmacoKinetic models.

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

Comparison of discriminative motif optimization using matrix and DNA shape-based models.

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

Using data-driven model-brain mappings to constrain formal models of cognition.

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

MatVPC: A User-Friendly MATLAB-Based Tool for the Simulation and Evaluation of Systems Pharmacology Models.

Project description:Quantitative systems pharmacology (QSP) models are progressively entering the arena of contemporary pharmacology. The efficient implementation and evaluation of complex QSP models necessitates the development of flexible computational tools that are built into QSP mainstream software. To this end, we present MatVPC, a versatile MATLAB-based tool that accommodates QSP models of any complexity level. MatVPC executes Monte Carlo simulations as well as automatic construction of visual predictive checks (VPCs) and quantified VPCs (QVPCs).

| S-EPMC4592534 | biostudies-literature

OmicsDI is part of the ELIXIR infrastructure

OmicsDI is an Elixir interoperability service. Learn more ›

Tweets

OmicsDI Databases

PRIDE
PeptideAtlas
MassIVE
JPOST Repository
Physiome Model Repository

EGA
EVA
ENA
LINCS
PAXDB
Cell Collective

MetaboLights
Metabolomics Workbench
MetabolomeExpress
GNPS
BioModels
FAIRDOMHub

ArrayExpress
dbGaP
ExpressionAtlas
GEO
NODE

Information

Databases
Help
API
Contact us
Code on GitHub
Terms of use
Submit Data