The applicability of the model checker Mule was illustrated based on four multilevel/multiscale computational models of biological systems published in the literature.

For reproducibility purposes the computational models (modified only when explicitly specified), the script and (Linux x64) modules for simulating the model and translating the simulation output to MSTML, the resulting datasets of MSTML files, the formal PBLMSTL specifications and the multiscale architecture graphs are made available below.

Rat cardiovascular system dynamics

Description
File Size (bytes)
Computational model *
BaroCV_Merged_Valsalva.proj 71,070
Simulation and translation to MSTML
stm_cardiovascular_vpr.7z 1,454,662
Dataset of MSTML files
cardiovascular_vpr_mstml_dataset.zip 1,684,101
Formal PBLMSTL specification specification_pblmstl_cardiovascular_vpr.in 4,959
Multiscale architecture graph
multiscale_architecture_graph_cardiovascular_vpr.xml 346

* The authors made the employed computational model available online and described how it was constructed in the following publication:

D. A. Beard, M. L. Neal, N. Tabesh-Saleki, C. T. Thompson, J. B. Bassingthwaighte, M. Shimoyama, and B. E. Carlson, “Multiscale Modeling and Data Integration in the Virtual Physiological Rat Project,” Ann Biomed Eng, vol. 40, no. 11, pp. 2365–2378, Nov. 2012.

Remark: The rat cardiovascular system dynamics computational model was simulated using JSim version 2.13.

Uterine contractions of labour

Description
File Size (bytes)
Computational model **
UterineContractionsModel.m 12,449
Simulation and translation to MSTML
stm_uterine_contractions.7z 1,425,677
Dataset of MSTML files
uterine_contractions_mstml_dataset.zip 22,470
Formal PBLMSTL specification specification_pblmstl_uterine_contractions.in 4,093
Multiscale architecture graph multiscale_architecture_graph_uterine_contractions.xml 589

** The authors made the employed computational model available online and described how it was constructed in the following publication:

R. C. Young and P. Barendse, “Linking Myometrial Physiology to Intrauterine Pressure; How Tissue-Level Contractions Create Uterine Contractions of Labor,” PLoS Comput Biol, vol. 10, no. 10, p. e1003850, Oct. 2014.

Remark: The uterine contractions of labour computational model was modified to output the simulation results to a file and was simulated using Mathematica version 10.0 for Linux x86.

Xenopus laevis oocytes cell cycle

Description
File Size (bytes)
Computational model ***
XenopusLaevisCellCycle.xml 6,216
Simulation and translation to MSTML
stm_xenopus_laevis_cell_cycle.7z 1,425,196
Dataset of MSTML files
xenopus_laevis_cell_cycle_mstml_dataset.zip 55,655,709
Formal PBLMSTL specification specification_pblmstl_xenopus_laevis_cell_cycle.in 8,475
Multiscale architecture graph multiscale_architecture_graph_xenopus_laevis_cell_cycle.xml 565

*** The authors made the employed computational model available online and a description of the considered intracellular reactions is provided in the following publication:

J. E. Ferrell Jr., T. Y.-C. Tsai, and Q. Yang, “Modeling the Cell Cycle: Why Do Certain Circuits Oscillate?,” Cell, vol. 144, no. 6, pp. 874–885, Mar. 2011.

Remark: The Xenopus laevis cell cycle computational model was modified such that simulations are run over a longer simulation time interval ([0, 1.02] instead of [0, 1.00]) and was simulated using Morpheus version 1.1.1.

Acute inflammation of the gut and lung

Description
File Size (bytes)
Computational model ****
GutLungAxis2.1.nlogo 58,674
Simulation and translation to MSTML
stm_acute_inflammation_of_gut_and_lung.7z 1,435,007
Dataset of MSTML files
acute_inflammation_of_gut_and_lung_mstml_dataset.zip 124,733,399
Formal PBLMSTL specification specification_pblmstl_acute_inflammation_of_gut_and_lung.in 3,550
Multiscale architecture graph multiscale_architecture_graph_acute_inflammation_of_gut_and_lung.xml 1,205

**** The author made the employed computational model available online and described how it was constructed in the following publication:

G. An, “Introduction of an agent-based multi-scale modular architecture for dynamic knowledge representation of acute inflammation,” Theoretical Biology and Medical Modelling, vol. 5, no. 1, p. 11, May 2008.

Remark: The acute inflammation of the gut and lung computational model was modified to employ the new NetLogo 5.0.5 syntax and to output the simulation results to a file, respectively it was simulated using NetLogo 3D version 5.0.5.