Checking Model Specifications with CrossCheck
Abstract
Model simulation frameworks are becoming more common as a way to evaluate the behavior of a complex system prior to its actual implementation. Simulation uncovers design errors early, especially important in embedded environments where post-development errors are costly to fix. While the formalization of a system as a model is becoming more systematized, the characterization of its behavior is still ad hoc. We have applied our dynamic specification checking technology CrossCheck to the CUTS model simulation framework as a way of verifying properties of interest in a model. CrossCheck utilizes a specialized language to express specifications, which are properties about the behavior of the system under check. CrossCheck specifications are compiled to generate a very efficient checking runtime, which receives and processes events from the instrumented CUTS model environment. By combining CrossCheck with the CUTS framework, we were able to develop specifications alongside the model that could be automatically verified during simulation runs.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 2009
- Accession Number
- ADA517556
Entities
People
- James Ezick
- Jonathan Springer
- Matthew Craven
- Rick Buskens