Tutorial: Parallel Model Checking

摘要: With the increase in complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality. Various techniques automated and semi-automated analysis verification have been proposed. In particular, model-checking has become a very practical technique due its push-button character. The basic principle behind is build model system under consideration together with description verified property suitable temporal logic. algorithm decision procedure which addition yes/no answer returns trace faulty behaviour case checked not satisfied by model. One additional advantages this approach that can be performed against partial specifications, considering only subset all specification requirements. This allows increased efficiency checking correctness respect most relevant requirements should fulfilled.