Some current topics in model checking |
| |
Authors: | Michael Huth |
| |
Affiliation: | (1) Department of Computing, Imperial College London, South Kensington campus, London, SW7 2AZ, United Kingdom |
| |
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. |
| |
Keywords: | Model checking Temporal logic Slicing Game semantics Refinement checking Feature integration Incremental design |
本文献已被 SpringerLink 等数据库收录! |
|