Welcome to Telelogic Product Support
  Home Downloads Knowledgebase Case Tracking Licensing Help Telelogic Passport
Telelogic Rhapsody (steve huntington)
Decrease font size
Increase font size
Topic Title: Tools for Model Checking and Model-Based Development
Topic Summary:
Created On: 23-Mar-2006 16:46
Status: Read Only
Linear : Threading : Single : Branch
Search Topic Search Topic
Topic Tools Topic Tools
Subscribe to this topic Subscribe to this topic
E-mail this topic to someone. E-mail this topic
Bookmark this topic Bookmark this topic
View similar topics View similar topics
View topic in raw text format. Print this topic.
 23-Mar-2006 16:46
User is offline View Users Profile Print this message


Brandi Carroll

Posts: 82
Joined: 22-Jul-2004

Tools for Model Checking and Model-Based Development

University of Virginia
Charlottesville, VA USA
[url]http://www.virginia.edu/[/url]

John C. Knight
Professor, Department of Computer Science

Overview
A wide variety of tools exist for assisting developers in building dependable systems. For this seminar, we have chosen two categories of these tools that are gaining increasing prominence and effectiveness:
model checkers and model-based development tools.

The seminar will be based around class projects involving these two types of tools. Each project will include material on the theory behind the tool and an
evaluation of the tool itself.
Model checkers analyze properties of a model of a program by taking a logical model of the system and analyzing what can occur over the different execution paths of that program. The model checker is given a
property to check, and it checks whether that property holds over all execution paths. If the property does not hold, the model checker returns an example path for which it doesn?t hold. The major technical stumbling
block of model checkers is the exponential nature of state space analysis. Different model checkers have addressed this problem in different ways, and the projects in this course will look to discover some of the tools? individual philosophies and, if possible, compare them against one another.

Model-based development is a more vague concept that means different things to different people. A classic example of model-based development is the combination of Simulink, a tool for defining software control
loops, and an automatic code generator. In general, model-based development assumes some analysis on a model of the system rather than on the implemented system itself. In many cases, the model is created in a domain-specific language that experts find easier to use, and its popularity derives from the perception that fewer requirements errors are introduced this way.

The projects in this course will aim to define more carefully the different ways that the term has been used, learn about the advantages and disadvantages of the tools, and find evaluation material in the existing literature.
We aim to publish the projects as a collection, either as a CS tech report or in ACM Computing Surveys.
We also plan to invite guest speakers to provide a little breadth outside our chosen tool topics.

Finally, this is a 3-credit course that will fulfill a CS seminar requirement.
Tool List includes Rhapsody & Statemate.
Report this to a Moderator Report this to a Moderator
Statistics
20925 users are registered to the Telelogic Rhapsody forum.
There are currently 0 users logged in.
You have posted 0 messages to this forum. 0 overall.

FuseTalk Standard Edition v3.2 - © 1999-2009 FuseTalk Inc. All rights reserved.