The objective of the Systems Level Design of Embedded Systems project was to develop and analyze Rosetta models describing domain interactions in embedded systems. There were three major outcomes from this project: (i) a co-algebraic semantics for Rosetta facets; (ii) composition mechanisms based on co-algebraic semantics; and (iii) analysis techniques using formal verification and simulation.

The co-algebraic semantics defines each Rosetta facet as a transformation defined over an abstract state. The intellectual advancement involves the treatment of a facet state variables as an observation of the co-algebra's abstract state. This is in contrast to equating the facet state and co-algebra state. The new semantics allows multiple state observations necessary for model composition. The alternative is choosing a single state representation for all facets.

Using the co-algebraic semantics, composition is simply a matter of treating different facets as observations of the same abstract state. Because the state variables within a facet are simply observations of the abstract state and can different semantics in different semantics. Interactions between those state variables can be defined by relating the state variables as observations of the abstract state.

From these concepts we developed simulation and formal verification techniques for Rosetta specifications. The Prufrock generic theorem prover allows static verification of properties over Rosetta facets. It's generic nature allows moving the prover from one abstract syntax to another by defining AST elements as instances of typeclasses. Thus, Prufrock is able to evolve with Rosetta.

A basic simulation capability was developed from the semantics allowing more traditional specification analysis. In conjunction with the ESSENSE effort sponsored by AFRL, we were able to generate simulatable models from Rosetta specifications. Unlike previous simulation capabilities, the Raskell simulator is native to the Rosetta environment and does not require transformation to a new semantics.

The co-algebraic semantics forms the basis of the standard formal semantics for Rosetta. It is being included in the Language Reference Manual in preparation for IEEE standardization. The Raskell simulator serves as the basis for ongoing analysis research and is being commercialized by ITTC and Cadstone, Inc.