Alderis@UCI

Analysis Language for Distributed, Embedded, and Real-time Systems.

Description

Alderis is a project hosted at the Center for Embedded Computer Systems (CECS), part of the Donald Bren School of Information and Computer Sciences (ICS) at the University of California, Irvine.

News

We have released several NuSMV models used for the analysis of a digital camera MPSoC. Click on AMBA to see the models! The results of this analysis were published in the following paper:

Gabor Madl, Sudeep Pasricha, Qiang Zhu, Luis Angel D. Bathen, Nikil Dutt: Formal Performance Evaluation of AMBA-based System-on-Chip Designs, Proceedings of EMSOFT 2006. Bibtex.

The publication is covered by copyright. It is provided for personal use only and may not be distributed.

Introduction

The Alderis project focuses on the application of Domain Specific Modeling Languages (DSMLs) and meta-modeling to specify a common semantic domain for the analysis of distributed real-time embedded (DRE) systems.

The Alderis language has both a visual and textual syntax with formally defined semantics. Alderis models can be verified directly by the open-source Distributed Real-time Embedded Analysis Method (DREAM) tool available for download at http://dre.sourceforge.net.

Motivation

Component-based development is an emerging paradigm for the design of distributed real-time embedded (DRE) systems with hard QoS support. Components refer to reusable pieces of solutions, which can be configured and composed together to provide a service. Alderis plans to support this paradigm shift by providing a language and semantic domain for the model-driven development (MDD) of DRE systems.

Model-Driven Development

The Alderis language is specified using meta-modeling as shown in the figure below. We use the GME modeling environment to specify Alderis. The figure shows a part of the Alderis meta-model with its corresponding concrete syntax. The red arrows show how modeling elements and their relations are specified by the meta-model.

Formal Verification & Analysis

A key property of the Alderis language is that it has formally defined semantics allowing real-time verification using timed automata model checker tools such as UPPAAL and the Verimag IF toolset. The DREAM tool provides a way to automatically generate the timed automata models from the Alderis specification. DREAM also provides a way for random simulations that can be used efficiently to find bugs in designs that are too large and lead to state space explosions.