Taming Living Logic using Formal Methods

Hasan Baig, Jan Madsen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

435 Downloads (Pure)


One of the goals of synthetic biology is to build genetic circuits to control the behavior of a cell for different application domains, such as medical, environmental, and biotech. During the design process of genetic circuits, biologists are often interested in the probability of a system to work under different conditions. Since genetic circuits are noisy and stochastic in nature, the verification process becomes very complicated. The state space of stochastic genetic circuit models is usually too large to be handled by classical model
checking techniques. Therefore, the verification of genetic circuit models is usually performed by the statistical approach of model checking. In this work, we present a workflow for checking genetic circuit models using a stochastic model checker (Uppaal) and a stochastic simulator (D-VASim). We demonstrate with experimentations that the proposed workflow is not only sufficient for the model checking of genetic circuits, but can also be used to design the genetic circuits with desired timings.
Original languageEnglish
Title of host publicationModels, Algorithms, Logics and Tools
Publication date2017
ISBN (Print)9783319631202
Publication statusPublished - 2017
EventKiMfest 2017 - Scandic Hotel, Aalborg Øst, Aalborg, Denmark
Duration: 19 Aug 201720 Aug 2017


ConferenceKiMfest 2017
LocationScandic Hotel, Aalborg Øst
SeriesLecture Notes in Computer Science

Bibliographical note

Larsen Festschrift - Essays dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday.


Dive into the research topics of 'Taming Living Logic using Formal Methods'. Together they form a unique fingerprint.

Cite this