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)
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)
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
tbd.
tbd.
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.
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.
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.
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.
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.
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.
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.
This video briefly shows how to debug mbeddr code on the level of the extensions (exemplified by calling into a component instance).
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.
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.
This video shows mbeddr's capability to support the manual review of the generated C code.
This video provides an introduction into how to use the verifications supported by mbeddr.
In this video we show how to import existing, textual header files so we can call into them from mbeddr code.
In this video we provide a quick overview over the tutorial. Subsequent videos will explain the tutorial in more detail.
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.
In this video we show the use of physical units, calculating with them, defining new ones and inserting conversions.
In this video we show state machines, including integration with C, visualization and verification.
In this video we show state interfaces (client/server and sender/receiver), components, component instantiation, visualization and verification.
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.
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.
This video shows mbeddr's approch to static (compile-time) and dynamic (runtime) product line variability.
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.