BIOCHAM

Category Cross-Omics>Agent-Based Modeling/Simulation/Tools and Cross-Omics>Pathway Analysis/Tools

Abstract BIOCHAM (the BIOCHemical Abstract Machine) is a software environment for modeling biochemical systems.

It is based on two (2) aspects: 1) the analysis and simulation of Boolean, kinetic and stochastic models and 2) the formalization of biological properties in temporal logic.

BIOCHAM provides tools and languages for describing ‘protein networks’ with a simple and straightforward syntax, and for integrating biological properties into the model.

It then becomes possible to analyze, query, verify and maintain the model with respect to those properties.

For kinetic models, BIOCHAM can search for appropriate parameter values in order to reproduce a specific behavior observed in experiments and formalized in temporal logic.

Coupled with other methods such as bifurcation diagrams, this search assists the modeler/biologist in the modeling process.

BIOCHAM is an attempt to make progress on the issue of 'automatic validation', using model-checking techniques (automatic validation - to systematically validate and maintain models using automated reasoning tools).

BIOCHAM is based on two (2) formal languages:

One straightforward rule-based language that allows the user to write models of biochemical networks and to perform multi-level analyses with a minimum knowledge of mathematics or computer science;

And one advanced yet simple temporal logic language [Computation Tree Logic (CTL) or Linear Temporal Logic (LTL)] used for formalizing experimental knowledge.

The first versions of the software were restricted to Boolean model analysis using the NuSMV model-checker.

BIOCHAM now permits continuous or stochastic simulations, and also model validation or revision with respect to a formal qualitative or quantitative specification.

As a result, BIOCHAM features functions to automatically check that No mistake is made at different stages of the model-building process.

For example it is possible to verify that whenever an interaction or a molecule is added to the diagram, the global properties of the system, expressed by temporal logic formulae, are conserved.

Similarly, it is possible to automatically search for parameter values that reproduce the specified behavior of the system in different conditions. In its current version BIOCHAM is composed of:

1) A rule-based language for modeling biochemical systems;

2) A simple simulator (either Boolean or numerical);

3) An advanced ‘query language’ based on temporal logic, CTL or LTL with 'arithmetic constraints' over reals, for querying the temporal properties of the model;

4) An interface to the NuSMV model checker for evaluating CTL queries - [NuSMV is a 'symbolic model checker' originated from the reengineering, reimplementation and extension of CMU SMV, the original Binary Decision Diagram (BDD)-based ‘model checker’ developed at Carnegie Mellon University (CMU)];

5) A machine learning system for correcting/completing a model, either by changing rules (with respect to) a CTL specification or by estimating parameters (with respect to) an LTL specification.

Modeling Biochemical Processes in BIOCHAM --

1) A simple algebra of biochemical compounds - BIOCHAM manipulates formal objects that represent chemical or biochemical compounds, ranging from ions to small molecules, macromolecules and genes.

BIOCHAM objects can also be used to represent control variables and abstract biological processes.

2) Reaction rules - BIOCHAM reaction rules are used primarily to represent biochemical reactions. They can also be used to represent 'state transitions' involving control variables or abstract processes or to represent the main effects of complete subsystems such as protein synthesis by DNA transcription without introducing RNAs in the model.

3) Kripke semantics - A BIOCHAM model is a set of 'reaction rules' given with an initial state. The formal semantics of a BIOCHAM model is a Kripke structure that is a mathematical structure which provides a firm ground for:

4) Importing biochemical models from other formalisms - Since the basic building block of a BIOCHAM model is an (enzymatic) reaction, it is quite easy to import any model based on such reactions into BIOCHAM.

This is the case of most graphical map-based models, but also of some ordinary differential equation (ODE) models, derived from the mass-action law or Michaelis-Menten kinetics.

A well known source of such models is KEGG, which provides (graphical) maps of metabolic and signaling pathways.

BIOCHAM has been designed to provide such maps with a simple yet precise semantics.

Note: BIOCHAM was used [in synergy with BetaWB (see G6G Abstract Number 20383) and GINsim (see G6G Abstract Number 20333)] to win the Biological Modeling Competition of the Formal Methods in Molecular Biology Dagstuhl workshop in February 2009.

System Requirements

Contact manufacturer

Manufacturer

Manufacturer Web Site BIOCHAM

Price Contact manufacturer.

G6G Abstract Number 20474

G6G Manufacturer Number 104099