What is the BMA?
Bio Model Analyzer is a new biological modelling tool that illustrates signalling pathways and determines cellular stabilization. The tool represents a merging of perspectives from systems biology, formal methods, human computer interaction and design. At one level, Bio Model Analyzer is a sketching tool that enables users to draw out a biological system of interest (e.g. a genetic regulatory network) by dragging and dropping cells, their contents (DNA, proteins, etc.), extracellular components and relationships onto a simple canvas.
At another level, Bio Model Analyzer’s analysis proves stabilization of biological systems, based upon formal methods that were developed for the specification and verification of properties in concurrent software systems. We hope you enjoy using Bio Model Analyzer and welcome your feedback.
Maintenance, development and design of the Bio Model Analyzer is funded by the Royal Society and the MRC. The Bio Model Analyzer was originally developed and supported by Microsoft Research.
Publications
Laure Talarmain, Matthew A. Clarke, David Shorthouse, Lilia Cabrera-Cosme, David G. Kent, Jasmin Fisher and Benjamin A. Hall,
Nature Communications 13, 5829 (2022), DOI 10.1038/s41467-022-33189-w
Peter Kreuzaler, Matthew A. Clarke, Elizabeth J. Brown, Catherine H. Wilson, Roderik M. Kortlever, Nir Piterman, Trevor Littlewood, Gerard I. Evan, and Jasmin Fisher
PNAS 2019, DOI 10.1073/pnas.1903485116
David Shorthouse, Angela Riedel, Emma Kerr, Luisa Pedro, Dóra Bihary, Shamith Samarajiwa, Carla P. Martins, Jacqueline Shields, Benjamin A. Hall
Nature Communications volume 9, Article number: 3011 (2018), DOI:10.1038/s41467-018-05414-y
Matthew A. Clarke, Steven Woodhouse, Nir Piterman, Benjamin A. Hall and Jasmin Fisher
In Automated Reasoning for Systems Biology and Medicine 2018
Yasmin Z. Paterson, David Shorthouse, Markus W. Pleijzier, Nir Piterman, Claus Bendtsen , Benjamin A. Hall, Jasmin Fisher
Integrative Biology 6/2018 DOI: 10.1039/c8ib00026c
Dana Silverbush, Shaun Grosskurth, Dennis Wang, Francoise Powell, Berthold Gottgens, Jonathan Dry, Jasmin Fisher
Cancer Research 2/2017: pages 827-838; DOI:10.1158/0008-5472.can-16-1578
David Shorthouse, Angela Riedel, Jacqueline Shields, Benjamin A. Hall
CMSB 2016, DOI:10.17863/CAM.4585 IEEE TCSIM best poster award
Zara Ahmed, David Benque, Sergey Berezin, Anna Caroline E. Dahl, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Jay Nanavati, Nir Piterman, Maik Riechert, Nikita Skoblov
Verification, Model Checking, and Abstract Interpretation, 01/2017: pages 1-13; ISBN: 978-3-319-52233-3, DOI:10.1007/978-3-319-52234-0_1
Benjamin A Hall, Nir Piterman, Alex Hajnal, Jasmin Fisher
Biophysical Journal 07/2015; 109(2):428-38., DOI:10.1016/j.bpj.2015.06.007
Chuang R., Hall B.A., Benque D., Cook B., Ishtiaq S., Piterman N., Taylor A., Vardi M., Koschmieder S., Gottgens B., and Fisher J.
Scientific Reports, 5:8190, February 2015
Taylor, Fisher, Cook, Ishtiaq, Piterman
Computational Culture, Nov 2014
Cook, Fisher, Hall, Ishtiaq, Juniwal, Piterman
CAV 2014
Taylor, Piterman, Ishtiaq, Fisher, Cook, Cockerton, Bourton, Benque
CHI 2013
Claessen, Fisher, Ishtiaq, Piterman, Wang
CAV 2013
Benque, Bourton, Cockerton, Cook, Fisher, Ishtiaq, Piterman, Taylor, Vardi
CAV 2012
Cook, Fisher, Krepska, Piterman
VMCAI 2011
Schaub, Henzinger, Fisher
BMC Systems Biology. 1:4, 2007
Funding
Open source development of the BioModelAnalyzer has been supported by the following grants.
Azure for Research
2017-2018
Microsoft
Ben Hall
Royal Society Enhancement Award (RGF\EA\180224)
2017-2022
Royal Society
Ben Hall
MRC Cancer Unit Core Funding
2017-2022
Medical Research Council
Ben Hall
New investigator research grant (MR/S000216/1)
2018-2022
Medical Research Council
Ben Hall
Team
Ben Hall is a Royal Society University Research Fellow working at the department of medical physics and biomedical engineering at University College London, and led the open-source development of the BMA tool since 2017, supported by awards from Microsoft, MRC, and the Royal Society. His research focuses on developing computational models of the decision making processes of cancer, from the early events of carcinogenesis to the later stages of metastasis. Alongside this, he maintains a long-standing interest in the development of algorithms and tools in formal methods for biology.
Jasmin Fisher is a Professor of Computational Biology in the Cancer Institute at University College London. She is also a Visiting Professor in the Department of Biochemistry at Cambridge University and a member of the Cancer Research UK Cambridge Centre and the Mark Foundation Institute for Integrated Cancer Medicine at the University of Cambridge. Jasmin is a pioneer in using formal verification methods to analyse executable mechanistic models of cellular processes. Her research group develops state-of-the-art computational models and analysis techniques to study cancer evolution and mechanisms of therapy resistance to identify better personalised treatments for cancer patients.
Nir Piterman is an associate professor in the Department of Computer Science and Engineering at the University of Gothenburg.
His research interests include formal verification, automata theory, and applications of formal methods to biological modeling.
Nicole is co-founder of the internationally acclaimed multi-disciplinary studio 'Kapitza', renowned for it’s innovative and pioneering font,
colour and pattern design. Studio output includes three critically celebrated pattern art books, of which 'Organic' was nominated for the prestigious Designs of the Year award.
Kapitza also gained recognition for an extensive font foundry with e-commerce store, a cutting-edge interactive pattern app as well as a diverse range of bespoke consultancy
services for clients from advertising, branding, packaging design, fashion, homeware and publishing.
Rachel is a Research Software Engineer in UCL's Advanced Research Computing centre, with a particular interest in computational and structural biology.
Frequently Asked Questions
How do I open Bio Model Analyzer?
To get started, click ‘Enter Tool’ on the Bio Model Analyzer website. You will enter Bio Model Analyzer’s blank canvas screen, with the icons aligned at the top of the screen and ‘Default Model: Version 1’ displayed in the lower right-hand corner.
How do I drag and drop elements onto the canvas?
Drag and drop works the same way for cells, membrane receptors, red variables and grey constants. Click the icon, drag it onto the canvas and release the mouse button to place the variable. Note that the canvas has ‘soft spots’ where the components can be placed and if you are not hovering over a soft spot, you won’t be able to place the component. These soft spots are apparent through highlighting. For instance, if you’re dragging a cell, a grid will highlight when you’ve reached a spot where you can release the cell onto the canvas. Similarly, when dragging receptors onto the cell membrane, you’ll see a circular spot appear highlighted in eight possible locations to attach the receptor around a given cell.
Drawing out the relationships that connect these components is done by firstly clicking on the activating / inhibiting relationship button and seeing it highlighted – this means the arrow is ready to be drawn between variables. Hover over a variable where the relationship starts to see it highlight, click, hold and drag it to another variable until that one is highlighted; release the mouse button and the relationship is drawn.
How do I zoom and scroll around the canvas?
The zoom operates by using either your mouse wheel or the zoom bar in the top right-hand corner. There is also a panning hand icon; when this mode is on (clicked and highlighted), you can pan around the grid, which you cannot do when the selection tool is on.
How do I name and give ranges to variables?
Clicking on a variable opens up a dialogue box in the bottom left corner. Here you can specify a name and descriptive range for variables. As usual it is good practice not to include symbols in names of variables (or files). For example, a ‘-‘ symbols in the name of a variable increases the likelihood of getting a failed analysis run as the tool processes subtraction relationships too, specified by ‘-‘. Typical qualitatively descriptive ranges are as follows: 0-1 for ‘off’ and ‘on’; 0-3 for ‘off’, ‘low’, ‘medium’ and ‘high’ concentrations; 1-1 for a ‘low concentration constant’; 3-3 for a ‘high concentration constant’; etc.
If you include variables with different ranges in the same model please have a look at "What happens with variables with different ranges?".
What are some basic target functions?
You can leave the default target function, which will entail that your variables get processed as follows: ave(pos) – ave(neg). This function means that the variable gradually changes its value to the difference between the average of the variables having an activating influence on it and the average of the variables having an inhibitive influence on it. This target function is built to optimize the usage of the range of the variable (see below when discussing sum).
Different target functions can be written using basic mathematical operators listed below. The following are typical target functions used in Bio Model Analyzer:
1. A constant’s target function is defined by the constant value that it takes (e.g. 0, 1, 2, etc.). [image:constant target box]
2. Using the default target function for a variable that has only inhibitions is not very useful. In such a case, the average of the positive influences is always 0. Then, if any of the negative influences are on, the variable will want to decrease below 0, if that was possible. Hence, it makes more sense to include the target of the maximal possible value minus the average of inhibitions. [image:only inhibition]
3. Sometimes, the average of positive activations is not appropriate if you desire multiple positive inputs having more of an impact than negative inputs. In such a case, it may make more sense to use the sum of values.
[image:sum activation]
Notice that this produces a very different behaviour. For example, if there is medium level of inhibition (2) and both the activators are in their maximum value of activity (4), then the target of the variable would be maximal (4). However, this does not change at all when the activators decrease to 3 or when the inhibitor increases to 3. The default target function, by contrast, computes the target of 2 and utilizes better the range of 0-4 by setting a target of 4 only when both activators are at their maximal level and the inhibitor is at the minimum level.
4. A common target function corresponds to complexation of two substances. In such a case, the level of the result is the minimum of the levels of the two substances. So the target function is min(var(substance1),var(substance2)).
How do I use advanced target functions?
You can also customize the target function, within the limits of the language defined in Bio Model Analyzer. The user has available the following operators: addition, subtraction, multiplication, division, maximum, minimum, ceiling, floor, and average. For example:
1. max(0,floor((var(a)+var(b))/2 – (var(c)+var(d)+var(e))/3)) : this essentially does the average of the positive and negative influences but adds the floor (lower integer value) to ensure that a target of 2.5 does not lead to instabilisation.
2. min(2-var(a),1)*var(b) : this function is calibrated for variables ranging between 0 and 2. It stipulates that if variable a is either 0 or 1 then the target is the value of b but if variable a is 2 then the target is 0. This models a threshold of inhibition by variable a. Where, as long as the level of a is below the maximum, variable b is copied. But once variable a is 2 it inhibits very strongly.
3. max(0,2-((2-var(a))*max(var(b)-1,0)+1)) : this is one of the most complex target functions we have encountered. It is similar to the previous one except that it includes a more complex condition. Again calibrated for the range 0-2. If variable b is 2 and variable a is not 2 then the target is 0, otherwise the target is the value of variable a. This expresses an inhibition that occurs only when b is at its maximum value and when a is not at its maximum value.
It is important to include in target functions only variables that have a relationship with the variable. If multiple variables of the same name have a relationship with the same variable, Bio Model Analyzer assumes that they affect it in a symmetric way. E.g., in var(a) + var(a) the association between the different a’s and the variables they represent is symmetric. In var(a)-var(a) it is not symmetric. Such an a-symmetric function could lead to problems with analysis. Similarly, if a variable has one relationship with one variable named b, then b cannot appear twice in the target function.
What happens with variables with different ranges?
BioModelAnalyzer is built to facilitate the usage of the default target function. What should happen if I have a variable X with range [0,1] activating a variable Y with range [0,2] (and no other influences)? In this case, it makes sense that the maximal value of X should lead to Y having maximal value as well. This means that the ranges of X and Y need to be adjusted when they affect each other. So BioModelAnalyzer does an automatic range conversion when X appears in the target function of Y (or vice versa). If you just use the default target functions this is not something you have to worry about. It essentially means that the entire range of Y will be possible in the example above (and similar cases). However, if you are building your own target functions this may lead to unexpected behaviour.
The exact range conversion that BioModelAnalyzer applies is as follows. If a constant with range [n,n] appears in the target function of a variable with a different range, then no range conversion is applied. If a variable X with range [a,b] appears in the target function of a variable Y with range [c,d], then whenever X appears in the target function of Y it will be modified to (X-a)*(d-c)/(b-a)+c.
If you want to create a model with different ranges that bypasses this automatic range conversion there is a simple solution. You have to define the ranges of all variables to be the same and use the target functions to practically restrict the range to what you want. In the example above, change the range of X to [0,2] and it's target function to be min(1,old_target_function). In general, if the maximal range in the model is [a,b] and you want a range of [c,d], where a<=c<=d<=b you will have to change to use the range [a,b] and the target function min(d,max(c,old_target_function)).
How do I save my work to the model library?
The simple saving that we recommend you do frequently while you work is done by clicking the save icon, second from the top left. To name and save a model more precisely during, or at the end of a model sketch, click the model library icon at the top left. You will see that the model you have started working on is temporarily saved as ‘Default Model’. To change that, simply click this text in the model library (highlighting it) and rewrite the file name of your choice. (To save your work further, see the next question about exporting and importing XML files.)
How do I export and import XML files?
In the model library, there are icons to export and import XML files. This is the best way to save and share models with your colleagues in a secure folder of your choice. Both export and import work like a typical ‘save as’ or ‘open’ function.
How do I move between models in my library?
Once you have developed a comprehensive model library, you can skip between models by clicking them (to highlight), then using the open button.
Bio Model Analyzer freezes while I’m working;
how do I stop this?
Key F5 to refresh the page. Don’t forget to frequently save your work. Please report any bugs via our feedback page.
Is this just a nice drawing tool?
The drawing has an underlying dynamic semantics. Essentially, a drawing describes a system with multiple states with rules on how it changes from state to state. A state corresponds to an assignment to all the variables in the system. From a given state, the system transitions to a new state by updating all the variables simultaneously. In order to determine the new value for a variable the value of its target function is computed based on the values of other variables it is in relation with. Then, if the value of the target function is higher than the value of the variable, it increases by 1. If the value of the target function is lower than the value of the variable, it decreases by 1. If the value of the target function is the same as that of the variable, it does not change.
What kind of analysis does Bio Model Analyzer do?
Bio Model Analyzer checks if the model becomes stable. That is, if regardless of the values the variables start with, there is one stability point that the model always reaches and then remains in. Bio Model Analyzer’s analysis is based on formal methods that were developed for the specification and verification of properties in concurrent software systems. The complexity of this analysis stems from the high number of possible states of such a system. A system with 10 variables, each ranging over 0-3, has 4^10 states, or roughly one million states. A system with 30 variables ranging over 0-1, has over one trillion states. Such large systems are impossible to manually inspect or visually inspect in a comprehendible layout. The formal analysis collects rules about which states of the system can be visited again and again. It uses this information to narrow down the possible states for the system to stabilize in. If the set of possible states to stabilize in collapses to just one state, then the analysis has been able to prove stabilization. If it does not, then the analysis tries to find either multiple sinks or several states that have a cycle between them.
We are also working on adding more types of analysis. We would appreciate your feedback.
Why are there only one variable and one constant icon?
How am I to represent the many different kinds of biological elements?
Bio Model Analyzer is a model that abstracts the biological meanings that differentiate genes, transcription factors, proteins and the like. As the biologist, you need to identify your variables so they make sense to you (e.g. via their naming) but the actual analysis that Bio Model Analyzer provides does not account for differences between variables, beyond how they are named, connected, and given ranges and target functions.
Open Source
The BioModelAnalyzer is an open source project, available under the MIT license. In addition to the web interface, command line tools are available that offer new analyses not currently available through the GUI.