MOdel-based DEsign & Verification for Safety-Critical Embedded Systems

MODEVES Project

The MODEVES project introduces a novel framework to support both Static as well as Dynamic Assertion Based Verfication for wide-ranging embedded systems. The major features are:

1. A modeling methodology to embed the verification constraints along with the structural and behavioral aspects of embedded systems at higher abstraction level.

2. A transformation engine to automatically generate System Verilog Register Transfer Level (RTL), Timed Automata model, SystemVerilog Assertions (SVAs) and CTL Assertions from high level model.

3. Supports both Static as well as Dynamic Assertion Based Verification (ABV). Particularly, Dynamic ABV of embedded systems can be performed by using the automatically generated SystemVerilog RTL and assertions code through a UVM-compliance (Universal Verification Methodology) simulator. Static ABV of embedded systems can be performed by using the automatically generated Timed Automata Model and CTL assertions code through UPPAAL Tool.

Overview

The early design verification of safety-critical embedded systems is a key research area due to the complexity of these systems. Model Based System Engineering (MBSE) ...........