The role of model checking in software engineering

Anil Kumar Karna, Yuting Chen, Haibo Yu, Hao Zhong, Jianjun Zhao

Research output: Contribution to journalReview article

2 Citations (Scopus)

Abstract

Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts. This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems. The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.

Original languageEnglish
Pages (from-to)642-668
Number of pages27
JournalFrontiers of Computer Science
Volume12
Issue number4
DOIs
Publication statusPublished - Aug 1 2018

Fingerprint

Model checking
Software Engineering
Model Checking
Software engineering
Software Development
Software System
Computer debugging
Constraint Solving
Malware
Software
Network Protocols
Formal Verification
Debugging
Service-oriented
Graphical user interfaces
Life Cycle
Web-based
Computer hardware
Life cycle
Safety

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

The role of model checking in software engineering. / Karna, Anil Kumar; Chen, Yuting; Yu, Haibo; Zhong, Hao; Zhao, Jianjun.

In: Frontiers of Computer Science, Vol. 12, No. 4, 01.08.2018, p. 642-668.

Research output: Contribution to journalReview article

Karna, Anil Kumar ; Chen, Yuting ; Yu, Haibo ; Zhong, Hao ; Zhao, Jianjun. / The role of model checking in software engineering. In: Frontiers of Computer Science. 2018 ; Vol. 12, No. 4. pp. 642-668.
@article{d58601d87a7a4f3a88dd26b0b3101e40,
title = "The role of model checking in software engineering",
abstract = "Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts. This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems. The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.",
author = "Karna, {Anil Kumar} and Yuting Chen and Haibo Yu and Hao Zhong and Jianjun Zhao",
year = "2018",
month = "8",
day = "1",
doi = "10.1007/s11704-016-6192-0",
language = "English",
volume = "12",
pages = "642--668",
journal = "Frontiers of Computer Science",
issn = "2095-2228",
publisher = "Springer Science + Business Media",
number = "4",

}

TY - JOUR

T1 - The role of model checking in software engineering

AU - Karna, Anil Kumar

AU - Chen, Yuting

AU - Yu, Haibo

AU - Zhong, Hao

AU - Zhao, Jianjun

PY - 2018/8/1

Y1 - 2018/8/1

N2 - Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts. This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems. The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.

AB - Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts. This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems. The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.

UR - http://www.scopus.com/inward/record.url?scp=85046025714&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85046025714&partnerID=8YFLogxK

U2 - 10.1007/s11704-016-6192-0

DO - 10.1007/s11704-016-6192-0

M3 - Review article

AN - SCOPUS:85046025714

VL - 12

SP - 642

EP - 668

JO - Frontiers of Computer Science

JF - Frontiers of Computer Science

SN - 2095-2228

IS - 4

ER -