mbeddr is a set of integrated and extensible languages for embedded software engineering, plus an IDE. It supports implementation, testing, verification and process aspects. It integrates with command-line build tools and integration servers, as well as file-based version control systems.
mbeddr has support for requirements and product line definition, software documentation, implementation in C and C extensions such as state machines physical units or interfaces and components, as well as testing, mocking, as well as formal verification.
mbeddr comes with a state-of-the-art IDE including syntax coloring, code completion, go to definition, realtime type checks, quick fixes, refactorings, customizable find-usages, automated synchronization between related parts of the code, version control integration and debugging.
A cleaned up version of C99 helps avoid low-level bugs. For example, the preprocessor is not supported and all its legitimate uses are supported by first-class concepts such as a robust module system. mbeddr also supports a native boolean type, enforces the use of the size-aware integral types and also has a cleaned up syntax for function types, function pointers and lambdas.
Reporting and logging is important for embedded applications. mbeddr contains rich frameworks for reporting program events and logging data. While they use stderr by default, both can be retargeted to arbitrary other systems including serial ports or error storage. Log statements can be selectively disabled with zero runtime footprint.
Testing is extremely important in embedded software. In mbeddr, test cases are first class concepts, and they support a set of different assert statements. Tests can be grouped into suites and invoked, from the main function reporting the number of failures to the operating system via main's return value. A special DSL for describing mocks is also available for the components language.
Many embedded systems deal with quantities from the real world, and mbeddr comes with an extension for phyiscal units to help represent such quantities. Types as well as literals can be annotated with units. The seven SI units are predefined, and users can define there own derived or convertible units. The type system computes with these units and reports errors in the IDE. There is zero runtime overhead, since the generated code has no representation of the units.
State-based behavior is ubiquitous in embedded software. mbeddr natively supports state machines that have events, variables, states and transitions with guards. States have entry, exit and do actions, transitions can have actions as well. State machines can be hierarchical and use epsilon transitions. State machines can be triggered from C code and themselves interact with C code in actions. State machines can be edited as text and tables, and can be visualized. Verification is available via model checking.
Modularization is critical for building flexible, testable and maintainable software. To this end, mbeddr supports interfaces with contracts (pre- and postconditions, protocol state machines). Similar to AUTOSAR, Components can provide or require interfaces. Contracts can be verified at runtime or statically. Components support mocks for testing. Translation to C can happen in various ways, some of them with very little overhead. Relationships between interfaces and components can be visualized.
In spite of the goal to describe systems formally, prose still plays an important role. mbeddr supports a language for capturing requirements that looks document-like, but is highly structured. Arbitrary DSLs can be mixed with the requirements in various ways. Tracing from arbitrary design, architecture or implementation elements is supported. A documentation language helps with creating code-integrated documents, exportable as HTML or LaTeX.
Almost all embedded systems are developed in the context of product lines. mbeddr supports describing variability via feature models. Feature model configurations are checked for compliance with the constraints expressed in the feature model. Artifacts can be adapted to the variant statically (via presence conditions) and at runtime (via specialized switch statements). The presence conditions can be overlaid over programs expressed in any language.
mbeddr's high-level DSLs lend themselves to verification. mbeddr integrates several verification tools, among them symbolic model checking of state machines, model checking/data flow analysis of C code for contract analysis as well as SMT solving for decision tables and feature models. The input to the verification tools is generated from mbeddr languages, and the result of the verification is lifted back up to the extension level.
Programs can be executed directly from within the mbeddr IDE. Failing assertions (in test cases) are hyperlinked to the code that caused the failure, simplifying tracking down problems in tests. Debugging is available on the level of the extension; for example, one can step through components or state machines. The low-level implementation of the extension is not shown. The Watch window is aware of mbeddr-specific types.
mbeddr provides state-of-the-art IDE support including syntax coloring, code completion, go to definition, realtime type-system checks, quick fixes (intentions), refactorings, customizable find-usages, and automated synchronization between related parts of the code. These features are available for C, its extensions, the requirements and documentation languages and all languages or extensions developed by users.
All code is stored in XML files, and thereby integrates with mainstream version control systems, among them SVN and git. To be able to see differences and merge conflicts, mbeddr/MPS supports a diff/merge view that uses the projectional editor, it works for any syntax. In addition, the IDE supports the vast majority of version control system operations, such as commit, update or reverting changes. A local history is available as well.
All existing languages can be extended with new language constructs, typing rules, constraints, generators or IDE functionality. In addition, arbitrary new languages can be added and (optionally) integrated with the existing languages. Extensions include the IDE and the debugger. New views, windows, menu items or buttons - and in fact, arbitrary Java libraries - can be added as well.
We believe that users should be able to extend a tool in any way they wish. They should not be limited by some "extension API". To achieve this, mbeddr builds on JetBrains MPS, a tool for efficiently building, extending and composing languages and their IDEs. Third parties can use the same language engineering facilities that the mbeddr team used to build the existing languages.
MPS uses a projectional editor. Consequently, MPS supports non-textual notations such as tables, mathematical symbols and (soon) graphics. By avoiding parser ambiguities, MPS also supports essentially unconstrained language composition and extension. All of the 30+ C language extensions provided by mbeddr are modular extensions, defined without modifying C itself.
mbeddr is structured into 5 layers, and addresses three different concerns (see below). The platform layer consists of the JetBrains MPS language workbench, which enables the overall approach. The core layer includes the base languages used in mbeddr; these are different for each of the three concerns. The default extensions layer consits of a set of predefined extensions of the core languages that can be used out-of-the-box to develop software. The user extension layer is empty, it is intended to be filled by users. The backend layer consists of existing tools compilation and analysis tools which mbeddr uses. A more detailed description of mbeddr can be found in the papers section.
The implementation concern addresses the development of applications based on C. On the core layer, mbeddr comes with an implementation of C99 in MPS. There are a few minor differences to C99, and the preprocessor is not exposed to the user; first-class concepts are provided for the legitimate uses of the preprocessor (including a module system). On the default extensions layer, the implementation concern comes with C extensions for decision tables, interfaces and components, state machines, physical units, testing as well as logging and tracing. The user extensions layer is by definition empty; users can easily extend the C core as well as any of the default extensions. State-of-the-art IDE support is available for all languages, including syntax highlighting, code completion, real-time type checks and refactorings. The implementation concern also ships with an extensible debugger that is able to debug on the level of the extensions, so the abstractions do not break down when debugging becomes necessary. At the backend layer, the implementation concern relies on a C compiler, a C debugger and tools for importing existing C code into mbeddr. By default, mbeddr uses the gcc compiler and the gdb debugger.
The analysis concern provides static analyses (formal verification) for some of the default extensions provided by the implementation concern. The analyses themselves are performed by existing external tools. However, mbeddr integrates the tools tightly by (a) providing language abstractions to conveniently describe behavior that can be analyzed, (b) translating this description to the input of the analysis tool, (c) running the tool, and (d) lifting the output of the tool back to the original abstraction level, to make it easier to understand for the user. The integrated analyses are based on symbolic model checking, SMT solving and C-level model-checking. Specifically, the following analyses are available: State machines can be checked with a symbolic model checker. It verifies a set of default properties and optional user-defined properties. Decision tables can be checked for completeness and consistency. Feature model configurations are checked for consistency. Finally, interface contracts can be checked statically: interfaces can specify pre- and post-conditions as well as protocol state machines that specify the valid invocation order of interface operations. These contracts can be checked for each implementing component via a C-level model checker.
The process concern includes facilities for integrating mbeddr into development processes. These facilities can be used with arbitrary mbeddr languages, such as all the default and user-defined C extensions. The requirements support provides a language for describing requirements. Traces can be attached to any program element expressed in any language. Arbitrary additional data, expressed in any language, can be added to a requirement. The product lines supports defining feature models and configurations. Feature models can be connected to other artifacts by means of presence conditions, While presence conditions are static and work for any language, there is also C-specific support to evaluate variability at runtime. The documentation language aspect supports writing prose documents as part of an mbeddr project, exportable as HTML or LaTeX. It supports close integration with program elements. They can be referenced (with real references that are renamed if the element itself is renamed) and program code can be embedded as text or as an image. The embedded code is updated whenever the document is regenerated. Visualization provides a facility to render diagrams. Reports and assessments are customizable queries over the code.
