San Francisco Time, UTC -8:00
Saturday, November 20th
00:00-01:00 Session: Introduction and Setup [video]
00:00
Holger Hermanns, Maximilian Köhl
Introduction of Quantitative Modelling with Momba
00:45
Holger Hermanns, Maximilian Köhl
Project Setup
  • Getting started: We walk you through the process of setting up the provided project skeleton such that you can follow along. Please make sure to have prepared your system upfront.
  • Best practices: How to set up a Python project for reproducibility and easy collaboration? We will walk you through the provided project skeleton. You will learn how to manage dependencies in a way that enables reproducibility, prevents version conflicts, and makes collaboration easy. We will demonstrate how to use tools such as auto formatters and linters to ensure a consistent code style and how to use VS Code workspaces to unify the development environment across a project.
  • Running example: We introduce the example you will be working with in more detail.
  • Model construction: We introduce the theory behind Momba and the JANI model format.
01:00-01:30Break
01:30-03:30Session: Hands-on [video]
01:30
Holger Hermanns, Maximilian Köhl

Model Construction: How to construct a formal model with Momba?

We walk you through the API provided by Momba to programmatically construct JANI models. Afterwards, you will have the opportunity to develop a model on your own using the skeleton we provide.
02:25
Holger Hermanns, Maximilian Köhl

Model Validation: How to validate a formal model with Momba?

We walk you through the state space exploration API provided by Momba. You will program an interactive visualization for your model.
03:00
Holger Hermanns, Maximilian Köhl

Model Analysis: How to analyze a formal model with Momba?

We will briefly introduce quantitative model checking. We then walk you through the analysis API provided by Momba. Using this API, you will analyze properties of your model.