This page contains step-by-step instructions to run and work with mbeddr on your machine. They videos are not a complete replacement for the user guide. But they should help with the first steps. Here is an overview:


  Installing MPS (3:06)
  Installing mbeddr (6:00)
  Installing Additional Tools (3:48)

Getting Started

  An Overview over the MPS IDE (6:06)
  Editing Code in MPS (10:00)
  The mbeddr Hello World (10:43)
  A few Differences to C99 (8:07)
  Using the Debugger (4:12)
  Working with Version Control (git) (7:55)
  Command-Line Generation (3:39)
  Importing Header Files (7:45)
  Review of the Generated Code (2:57)
  Formal Verification 101 (7:36)
  Overview over the Tutorial (4:07)

Feature Demos

  Decision Tables (4:21)
  Physical Units (6:19)
  State Machines (8:10)
  Components (12:35)
  Testing (13:08)
  Requirements, Tracing, Use Cases and Scenarios (10:36)
  Product Line Variability (8:18)
  Model-driven Code Checking (14:09)
  Importing Legacy Code

Getting Started with the Extensions


Developing New Extensions





Installing MPS

This video explains how to install JetBrains MPS, which acts as the platform on which mbeddr runs. Note that you also have to install Java to make MPS work. Note: If you run MPS by double-clicking onto the MPS icon, then the mps.vmoptions file is ignored, and you should set the JVM memory options in the info.plist. If you start MPS by running ./mps.sh, then the mps.vmoptions is used.


Installing mbeddr

This video explains how to install mbeddr itself. Essentially you have to download the mbeddr MPS plugins from the download page and then copy the unzipped plugins into MPS' plugins folder.


Installing Additional Tools

To be able to compile C files on Windows, you will have to install the gcc package from cygwin. On the Mac you should install XCode, together with the optional command line tools. On Linux, gcc installed by default. To be able to use the visualizations, you must install graphviz and put it on the path. Finally, to use the verifications, you must install NuSMV, Yices 1 and CBMC. All of these are command-line tools and need to be available on the path. Note: on windows, you have to set an environment variable GRAPHVIZ_DOT that points to graphviz' dot.exe file.


Getting Started


Overview over the IDE

This video is a quick overview over the MPS IDE. It introduces tools, editors, solutions, languages and projects, as well as some of the other terminology used in MPS and mbeddr.


Editing Code in MPS

This video helps you get started with editing code in MPS. MPS, after all, is a projectional editor, so some of the editing gestures are a bit different than in regular text editors.


The mbeddr Hello World

In this video we implement a simple hello world test case, build it, run it from the command line and run it from within MPS, which allows you to directly click on error messages and jump to the failing assert.


A few Differences to regular C

In this video we discuss the few places where mebddr's version of C is different from C99. These places include header files and the preprocessor in general, array and pointer variable declarations as well as the handling of function pointers, function types and lambdas. Note: mbeddr also has a native boolean type, which we forgot to mention in the video.


Using the Debugger

This video briefly shows how to debug mbeddr code on the level of the extensions (exemplified by calling into a component instance).


Working with Version Control

In this video we show how to work with mbeddr, MPS and a version control system. In particular, we demonstrate the git integration. As part of the demo we show how to merge conflicts in MPS, using the projected syntax of the underlying language in the three-way merge dialog.


Command-Line Generation

In this video we show how to generate mbeddr code into C code for compilation, so you can integrate it with build servers or integration servers.


Review of mbeddr Models and Generated C Code (Feature Demo)

This video shows mbeddr's capability to support the manual review of the generated C code.


Formal Verification 101

This video provides an introduction into how to use the verifications supported by mbeddr.


Importing Header Files

In this video we show how to import existing, textual header files so we can call into them from mbeddr code.


Overview over the Tutorial

In this video we provide a quick overview over the tutorial. Subsequent videos will explain the tutorial in more detail.


Feature Demos


Decision Tables (Feature Demo)

In this video we demonstrat decision tables, which are essentially a nicer syntax for nested if statements. We also demonstrate the completeness and consistency checking using the integrated SMT solver.


Physical Units (Feature Demo)

In this video we show the use of physical units, calculating with them, defining new ones and inserting conversions.


State Machines (Feature Demo)

In this video we show state machines, including integration with C, visualization and verification.


Components (Feature Demo)

In this video we show state interfaces (client/server and sender/receiver), components, component instantiation, visualization and verification.


Testing (Feature Demo)

This video explores how mbeddr supports testing. It shows basic test cases, test helper functions, component mocks, interpreting test output, logging, reporting and a custom language that improves testability.


Requirements, Tracing, Use Cases and Scenarios (Feature Demo)

This video shows how we handle requirements in mbeddr including: requirements collection, tracing from code to requirements, embedding business logic in requirements, as well as use cases and scenarios.


Product Line Variability (Feature Demo)

This video shows mbeddr's approch to static (compile-time) and dynamic (runtime) product line variability.


Model-driven Code Checking (Feature Demo)

This video shows the mbeddr support for formal verification using the Model-driven Code Checking approach based on the Spin model checker. We demonstrate the DSLs for the definition of the environment and different tooling aspects.