About 4mlWare Development And Tools Project News

The goal of the 4mlWare project is a suite of experimental software tools for formally modeling computer-based systems. These tools implement our latest research on the formal basis of domain specific modeling languages.

The 4mlWare tools take advantage of the long history of modeling tools developed at ISIS, and are designed to work together with much of the existing ISIS software including GME, MetaGME, GReAT, and UDM.

 

FORMULA is our analysis and verification tool for DSMLs and DSML transformations. It works for domains and transformations defined in Horn logic.

The GME4mlizer exports  and imports models and meta-models into a formal representation suitable for analysis and transformation.

The GREAT4mlizer converts graph transformations into Horn transformations. Properties of the transformation can be verified with FORMULA.

The ISIS summer internship program, CIPHER, will use SMOLES to teach undergraduates about models of computation (MoCs) and embedded systems design.

They will spend the summer designing synchronous reactive controllers for Lego Mindstorm robots. They will not only design dynamically interesting controllers, but they will learn how to verify that these controllers are correct.

The results of their progress will be posted here.

Due to the experimental nature of this software, it will not be released en masse in the near future. However, we am happy to supply research versions to those who are interested. Feel free to contact Ethan Jackson or Kai Chen with any questions or comments:

ejackson@isis.vanderbilt.edu

chenk@isis.vanderbilt.edu

Methods for specifying models of computation (MoCs) with ASML. Includes a growing library of MoC specifications.

SMOLES is a DSML for building synchronous reactive systems in GME. It uses aspects, generative constraints, and design time rules to produce correct models at design time.

This tool will generate real-time embeddable model storage and manipulation APIs for embedded systems with dynamic models.