Grand Unified Modeling of Behavioral Operators (GUMBO)

Model-based systems engineering approaches can provide assurance that the design represented by the model supports the system requirements as specified. One challenge, however, is verifying that the results of the behavioral analysis applied to the model representation also apply to the system as implemented. Enter: Grand Unified Modeling of Behavioral Operators (GUMBO). This contract language, and the supporting tools, provide the foundation for formally verifying that the code-level implementations satisfy model-level specifications. Support includes run-time services, well-defined conceptual semantics, parsing, and validation. AADL is currently directly supported. In the future, additional languages will be supported.

The High Assurance Modeling and Rapid engineering for embedded systems (HAMR) toolset, developed on the DARPA Cyber Assured Systems Engineering (CASE) program, generates deployable code directly from the architectural model in AADL, thereby preserving some forms of traceability between the analytical model results and the deployed system. On the Grand Unified Modeling of Behavioral Operators (GUMBO) Army Phase II SBIR, we extended the HAMR toolchain to automatically insert these model-based behavioral contracts into deployable Slang source code that can be formally (mathematically) verified.

For tool installation: https://github.com/sireum/aadl-gumbo-update-site