Systems-Level Design Group

Rosetta

The Rosetta project is focused on developing the Rosetta semantics, language and toolset for modeling and analyzing systems-level requirements. The main Rosetta website overviews the language and the current status of our development and standardization activities. The Raskell project focuses on the development of analysis techniques and tools for Rosetta models. A collection of basic Rosetta tools is available including the Prufrock polytypic theorem prover environment and a Rosetta Expression Interpreter.

Raskell

Raskell is our Haskell-based interpretation and analysis environment for Rosetta specifications. Raskell includes a Parsec-based Rosetta parser that generates both recursive and non-recursive AST structures. The heart of Raskell is a collection of composable interpreters that support type checking, evaluation and abstract interpretation of Rosetta specifications.

Interpreter Libraries

The InterpreterLib utilities support development of composable interpreters. InterpreterLib makes the semantic algebra explicit in the interpreter rather than using polymorphism for selection. InterpreterLib structures interpreters around a Functor and Algebra written for each AST construct. AST elements are defined non-recursively and composed using a Sum type. The actual language is formed by taking the fixed point of the language sum. To interpret an AST element, a catamorphism is applied explicitly specifying an appropriate semantic algebra defining the interpretation.

The LangUtils library predates IntepreterLib and provides a collection of functions and type classes that implement semantic algebras in the style of Hutton and Duponcheel. Development has ceased, but we keep LangUtils available as an introduction to modular, monadic interpreters.

Model Composition

In support of our systems-level design focus, we are developing techniques for composing and analyzing models of different system facets that may potentially use different modeling semantics. We have developed a co-algebraic semantics to support the Rosetta language and continue to develop static and dynamic techniques for analysis. This work is ongoing.

Component Retrieval

A long-term project in our lab is the development of techniques using formal analysis for component retrieval. This effort started with the REBOUND system that used feature generation as a mechanism for weeding out non-matches prior to component comparison. The SOCCER prototype extended this capability using Rosetta as the component modeling language. Our most recent prototype, SPARTACAS, uses adaptation architectures to adapt components in a black box fashion.

Embedded Systems Modeling

Embedded systems has become a focus for our Rosetta modeling activities. We are currently looking specifically at the modeling of cross-cutting concerns in embedded systems using static and dynamic analysis techniques.

We have recently begun a project with our embedded systems group looking at developing a secure infrastructure for embedded systems. We take a systems-level view integrating security enforcement from language-level analysis techniques through a secure virtual machine to runt-time analysis in hardware. This is a new effort with much promise for future activity.

Network Systems Modeling

Network security has become a focus for our Rosetta modeling activities. We are currently looking at the impacts of changing infrastructure on systems-level security requirements and analysis of distributed firewall systems.

Test Vector Generation

A series of projects with EDAptive Computing and TRW have lead to the DVTG, VectorGen and GENISYS tools for generating test vectors from Rosetta requirements.

Dance Representation

Using monadic, compositional interpreter techniques, we have developed a prototype language and tools for representing and analyzing choreography. Because choreography is pre-literate - no written form - this has been a particularly challenging and interesting project.