Model checking: recent improvements and applications

Research output: Contribution to journalArticleAcademicpeer-review

62 Downloads (Pure)

Abstract

Model checking (Baier and Katoen in Principles of model checking, MIT Press, Cambridge, 2008; Clarke et al. in Model checking, MIT Press, Cambridge, 2001) is an automatic technique to formally verify that a given specification of a concurrent system meets given functional properties. Its use has been demonstrated many times over the years. Key characteristics that make the method so appealing are its level of automaticity, its ability to determine the absence of errors in the system (contrary to testing techniques) and the fact that it produces counter-examples when errors are detected, that clearly demonstrate not only that an error is present, but also how the error can be produced. The main drawback of model checking is its limited scalability, and for this reason, research on reducing the computational effort has received much attention over the last decades. Besides the verification of qualitative functional properties, the model checking technique can also be applied for other types of analyses, such as planning and the verification of quantitative properties. We briefly discuss several contributions in the model checking field that address both its scalability and its applicability to perform planning and quantitative analysis. In particular, we introduce six papers selected from the 23rd International SPIN Symposium on Model Checking Software (SPIN 2016).

Original languageEnglish
Pages (from-to)493–497
Number of pages5
JournalInternational Journal on Software Tools for Technology Transfer
Volume20
Issue number5
DOIs
Publication statusPublished - 1 Oct 2018

Keywords

  • Model checking
  • Partial-order reduction
  • Planning
  • Probabilistic model checking
  • Strategy synthesis

Fingerprint Dive into the research topics of 'Model checking: recent improvements and applications'. Together they form a unique fingerprint.

  • Cite this