Analyzing and verifying UML models with OCL and Alloy

Nicolas Rouquette (Jet Propulsion Laboratory M/S 301-270 4800 Oak Grove Drive Pasadena, CA 91109)

Modeling · Short Talk

Thursday, 10:10, 10 minutes | Room 209/210 | Download in iCal Format

7
·
8
·
9
·
10
·
11
·
12
·
13
·
14
·
15
·
16
·
17
·
18
·
19

Nicolas Rouquette

This talk will demonstrate a novel approach for verifying complex logical properties in the structural foundations of a metamodel using OCL queries to project the metamodel into a computationally efficient abstraction in a specification for MIT's Alloy analyzer. We will demonstrate how this technique can be effectively used to develop and analyze sub-languages of the UML such as UML profiles for Moore and Mealy state machines. Alloy provides a user-friendly front-end language for analyzing problems using a back-end SAT solver such as SAT4J. We will also demonstrate how this OCL + Alloy technique can, with the right abstraction, scale to analyze complex properties over medium-size metamodels such as one being developed for the "Semantics of a Foundational Subset for Executable UML".

Dr. Rouquette has been involved in applications of state-of-the-art model-driven development technologies at JPL for over a decade. For the 1998 Deep Space One mission, he pioneered a novel approach to spacecraft fault protection system design using the Mathworks' Stateflow toolbox augmenting the breadth of code generation to include the synthesis of telemetry encoding/decoding algorithms. While this technology has been reused for the 2005 Deep Impact mission, Nicolas shifted to JPL's State Analysis methodology where he led the design of the component architecture for the Mission Data System project. Recently, Nicolas has been involved in supporting the NASA Constellation project with an adaptation of Kennedy Carter's iUML exporter to produce <>-profiled UML models based on a lightweight extension of a preliminary version of an OMG specification being developed for a "Semantics of a Foundational Subset for Executable UML".

Floor Plan

Gold sponsors

BEA logo

IBM logo

Wind River logo

Replay Solutions logo

JBoss logo

SOPERA logo

Cloudsmith logo

BIRT Exchange logo

Skyway Software logo

Oracle

BlackBerry logo

AMD logo

Silver sponsors

Sybase

Google

Genuitec

Instantiations

Teamprise

Telelogic

Innoopract

Business Objects

LynuxWorks logo

Hardware sponsor

AMD logo

Media sponsors

Extension Media

Methods and Tools

ACM

Addison-Wesley logo

SD Times logo

Open Systems Publishing

Software Test & Performance logo

SDForum

Be a Sponsor