Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is f...Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.展开更多
Model checking is an algorithmic verification technique that checks automatically whether a given finite
state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state s...Model checking is an algorithmic verification technique that checks automatically whether a given finite
state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state space
explosion problem. In this paper, several important approaches have been proposed for dealing with the state
explosion problem. Such approaches are symbolic, abstraction, partial-order reduction, compositional reasoning,
etc. Then,a number of way are proposed for verifying real-time and hybrid systems using model checking. At last,
several approaches combining model checking and other verification techniques or mathematical methods are consid-
ered.展开更多
文摘Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.
文摘Model checking is an algorithmic verification technique that checks automatically whether a given finite
state concurrent system satisfies its temporal specification. The main disadvantage of model checking is state space
explosion problem. In this paper, several important approaches have been proposed for dealing with the state
explosion problem. Such approaches are symbolic, abstraction, partial-order reduction, compositional reasoning,
etc. Then,a number of way are proposed for verifying real-time and hybrid systems using model checking. At last,
several approaches combining model checking and other verification techniques or mathematical methods are consid-
ered.
