![]() |
Telelogic Rhapsody (steve huntington) | ![]() |
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 |
![]() |
![]()
|
![]() |
|
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. |
|
![]() |
FuseTalk Standard Edition v3.2 - © 1999-2009 FuseTalk Inc. All rights reserved.