Some current issues in model checking

File Description SizeFormat 
Some current topics in model checking.pdf182.02 kBAdobe PDFDownload
Title: Some current issues in model checking
Author(s): Huth M
Item Type: Journal Article
Abstract: Model checking is a particular approach to property verification of systems. One describes a system in a mathematical model, expresses the properties one wishes to verify for the system in a formal language, and then checks whether the model satisfies the formal property. Invented 25 years ago, this approach is fully automatic and has therefore gained wide acceptance and is increasingly being used in commercial research and development units. Impediments remain on the road to successful technology transfer. For one, the size of models often increases exponentially in the number of variables or sub-models, preventing scalable automation. Abstracting a model to reduce its size can be a cost-effective way of addressing this. For another, systems and models may be subject to change, e.g. in an incremental design process. One then seeks cost-effective means of ascertaining that property verifications remain to be valid as models evolve. This special section presents current research on such abstraction and change management of model checking. © Springer-Verlag 2007.
Publication Date: 1-Feb-2007
Citation: Int J Softw Tools Technol Transfer Vol.( 9 ) No.( 1 ) pp 25 - 36
Publisher Link:
ISSN: 1433-2779
Start Page: 25
End Page: 36
Copyright Statement: © Springer-Verlag 2006. The original publication is available at
Volume: 9
Appears in Collections:Quantitative Analysis and Decision Science

Items in Spiral are protected by copyright, with all rights reserved, unless otherwise indicated.

Creative Commons