Automatic selection of verification tools for efficient analysis of biochemical models.

Motivation: Formal verification is a computational approach that checks system correctness (in relation to a desired functionality). It has been widely used in engineering applications to verify that systems work correctly. Model checking, an algorithmic approach to verification, looks at whether a system model satisfies its requirements specification. This approach has been applied to a large number of models in systems and synthetic biology as well as in systems medicine. Model checking is, however, computationally very expensive, and is not scalable to large models and systems. Consequently, statistical model checking (SMC), which relaxes some of the constraints of model checking, has been introduced to address this drawback. Several SMC tools have been developed; however, the performance of each tool significantly varies according to the system model in question and the type of requirements being verified. This makes it hard to know, a priori, which one to use for a given model and requirement, as choosing the most efficient tool for any biological application requires a significant degree of computational expertise, not usually available in biology labs. The objective of this article is to introduce a method and provide a tool leading to the automatic selection of the most appropriate model checker for the system of interest. Results: We provide a system that can automatically predict the fastest model checking tool for a given biological model. Our results show that one can make predictions of high confidence, with over 90% accuracy. This implies significant performance gain in verification time and substantially reduces the 'usability barrier' enabling biologists to have access to this powerful computational technology. Availability and implementation: SMC Predictor tool is available at http://www.smcpredictor.com. Supplementary information: Supplementary data are available at Bioinformatics online.

BioNexusSentinel: a visual tool for bioregulatory network and cytohistological RNA-seq genetic expression profiling within the context of multicellular simulation research using ChatGPT-augmented software engineering.

Summary: Motivated by the need to parameterize ongoing multicellular simulation research, this paper documents the culmination of a ChatGPT augmented software engineering cycle resulting in an integrated visual platform for efficient cytohistological RNA-seq and bioregulatory network exploration. As contrasted to other systems and synthetic biology tools, BioNexusSentinel was developed de novo to uniquely combine these features. Reactome served as the primary source of remotely accessible biological models, accessible using BioNexusSentinel's novel search engine and REST API requests. The innovative, feature-rich gene expression profiler component was developed to enhance the exploratory experience for the researcher, culminating in the cytohistological RNA-seq explorer based on Human Protein Atlas data. A novel cytohistological classifier would be integrated via pre-processed analysis of the RNA-seq data via R statistical language, providing for useful analytical functionality and good performance for the end-user. Implications of the work span prospects for model orthogonality evaluations, gap identification in network modelling, prototyped automatic kinetics parameterization, and downstream simulation and cellular biological state analysis. This unique computational biology software engineering collaboration with generative natural language processing artificial intelligence was shown to enhance worker productivity, with evident benefits in terms of accelerating coding and machine-human intelligence transfer. Availability and implementation: BioNexusSentinel project releases, with corresponding data and installation instructions, are available at https://github.com/RichardMatzko/BioNexusSentinel.

Verifiable biology.

The formalization of biological systems using computational modelling approaches as an alternative to mathematical-based methods has recently received much interest because computational models provide a deeper mechanistic understanding of biological systems. In particular, formal verification, complementary approach to standard computational techniques such as simulation, is used to validate the system correctness and obtain critical information about system behaviour. In this study, we survey the most frequently used computational modelling approaches and formal verification techniques for computational biology. We compare a number of verification tools and software suites used to analyse biological systems and biochemical networks, and to verify a wide range of biological properties. For users who have no expertise in formal verification, we present a novel methodology that allows them to easily apply formal verification techniques to analyse their biological or biochemical system of interest.

Novel Ground-Up 3D Multicellular Simulators for Synthetic Biology CAD Integrating Stochastic Gillespie Simulations Benchmarked with Topologically Variable SBML Models.

The elevation of Synthetic Biology from single cells to multicellular simulations would be a significant scale-up. The spatiotemporal behavior of cellular populations has the potential to be prototyped in silico for computer assisted design through ergonomic interfaces. Such a platform would have great practical potential across medicine, industry, research, education and accessible archiving in bioinformatics. Existing Synthetic Biology CAD systems are considered limited regarding population level behavior, and this work explored the in silico challenges posed from biological and computational perspectives. Retaining the connection to Synthetic Biology CAD, an extension of the Infobiotics Workbench Suite was considered, with potential for the integration of genetic regulatory models and/or chemical reaction networks through Next Generation Stochastic Simulator (NGSS) Gillespie algorithms. These were executed using SBML models generated by in-house SBML-Constructor over numerous topologies and benchmarked in association with multicellular simulation layers. Regarding multicellularity, two ground-up multicellular solutions were developed, including the use of Unreal Engine 4 contrasted with CPU multithreading and Blender visualization, resulting in a comparison of real-time versus batch-processed simulations. In conclusion, high-performance computing and client-server architectures could be considered for future works, along with the inclusion of numerous biologically and physically informed features, whilst still pursuing ergonomic solutions.

Toward Full-Stack In Silico Synthetic Biology: Integrating Model Specification, Simulation, Verification, and Biological Compilation.

We present the Infobiotics Workbench (IBW), a user-friendly, scalable, and integrated computational environment for the computer-aided design of synthetic biological systems. It supports an iterative workflow that begins with specification of the desired synthetic system, followed by simulation and verification of the system in high-performance environments and ending with the eventual compilation of the system specification into suitable genetic constructs. IBW integrates modeling, simulation, verification, and biocompilation features into a single software suite. This integration is achieved through a new domain-specific biological programming language, the Infobiotics Language (IBL), which tightly combines these different aspects of in silico synthetic biology into a full-stack integrated development environment. Unlike existing synthetic biology modeling or specification languages, IBL uniquely blends modeling, verification, and biocompilation statements into a single file. This allows biologists to incorporate design constraints within the specification file rather than using decoupled and independent formalisms for different in silico analyses. This novel approach offers seamless interoperability across different tools as well as compatibility with SBOL and SBML frameworks and removes the burden of doing manual translations for standalone applications. We demonstrate the features, usability, and effectiveness of IBW and IBL using well-established synthetic biological circuits.

Model-Based Integration Analysis Revealed Presence of Novel Prognostic miRNA Targets and Important Cancer Driver Genes in Triple-Negative Breast Cancers.

Background: miRNAs (microRNAs) play a key role in triple-negative breast cancer (TNBC) progression, and its heterogeneity at the expression, pathological and clinical levels. Stratification of breast cancer subtypes on the basis of genomics and transcriptomics profiling, along with the known biomarkers' receptor status, has revealed the existence of subgroups known to have diverse clinical outcomes. Recently, several studies have analysed expression profiles of matched mRNA and miRNA to investigate the underlying heterogeneity of TNBC and the potential role of miRNA as a biomarker within cancers. However, the miRNA-mRNA regulatory network within TNBC has yet to be understood. Results and Findings: We performed model-based integrated analysis of miRNA and mRNA expression profiles on breast cancer, primarily focusing on triple-negative, to identify subtype-specific signatures involved in oncogenic pathways and their potential role in patient survival outcome. Using univariate and multivariate Cox analysis, we identified 25 unique miRNAs associated with the prognosis of overall survival (OS) and distant metastases-free survival (DMFS) with "risky" and "protective" outcomes. The association of these prognostic miRNAs with subtype-specific mRNA genes was established to investigate their potential regulatory role in the canonical pathways using anti-correlation analysis. The analysis showed that miRNAs contribute to the positive regulation of known breast cancer driver genes as well as the activation of respective oncogenic pathway during disease formation. Further analysis on the "risk associated" miRNAs group revealed significant regulation of critical pathways such as cell growth, voltage-gated ion channel function, ion transport and cell-to-cell signalling. Conclusion: The study findings provide new insights into the potential role of miRNAs in TNBC disease progression through the activation of key oncogenic pathways. The results showed previously unreported subtype-specific prognostic miRNAs associated with clinical outcome that may be used for further clinical evaluation.

A Property-Driven Methodology for Formal Analysis of Synthetic Biology Systems.

This paper proposes a formal methodology to analyse bio-systems, in particular synthetic biology systems. An integrative analysis perspective combining different model checking approaches based on different property categories is provided. The methodology is applied to the synthetic pulse generator system and several verification experiments are carried out to demonstrate the use of our approach to formally analyse various aspects of synthetic biology systems.

Qualitative and quantitative analysis of systems and synthetic biology constructs using P systems.

Computational models are perceived as an attractive alternative to mathematical models (e.g., ordinary differential equations). These models incorporate a set of methods for specifying, modeling, testing, and simulating biological systems. In addition, they can be analyzed using algorithmic techniques (e.g., formal verification). This paper shows how formal verification is utilized in systems and synthetic biology through qualitative vs quantitative analysis. Here, we choose two well-known case studies: quorum sensing in P. aeruginosas and pulse generator. The paper reports verification analysis of two systems carried out using some model checking tools, integrated to the Infobiotics Workbench platform, where system models are based on stochastic P systems.