A General Framework for Formalizing Object-Oriented Modeling Techniques

Acknowledgements

Slide 3

Overview

Objectives and Results

Domain: Embedded Systems

Background: Embedded Systems

Informal Modeling Notation

Background: UML

UML Class Diagram

UML Metamodel

Example Metamodel

Metamodel - Diagram - System Relationship

Target Formalization Languages

Background: VHDL

Background: Promela  (SPIN)

Background: Promela Example

General Formalization Framework

Homomorphisms

Metamodel mapping

Unified Class/Dynamic Metamodel

Dynamic Model Portion of Unified Metamodel

Example Metamodel Mapping

Introduction to Mapping Rules

Promela Class Diagram Mapping Rules

Promela Dynamic Model Mapping Rules

SPIN Analyses

Summary of Mappings

Tool Support

Tool Support

Architecture of Minerva

Hydra Translation Tool

Industrial Case Study

Smart Cruise Requirements

Class - Context Diagram

Smart Cruise Class Model

High Level Radar Dynamic Model

Car Dynamic Model

High Level Control Dynamic Model

SPIN Analyses Performed

Use of Simulation

State Reachability Analysis

State Reachability for Normal Scenario

SPIN Progress Loop Analysis

 Progress Cycle Analysis of Model

Progress Loop Checks

Model Checking Tests

Ensure Target is Never Missed
Demonstrate Check Works

Related Work

Embedded System Methodologies

Formalization of UML

Other OO Formalizations

Overview of Contributions

Where does this all fit in Big Picture?

Meridian: Automating Development of  IDAs

 Meridian Research goals

 Meridian Practical goals

Meridian Vision

Summary of Contributions

Current and Future Research

Current/Future Research

Discussion…