Model checking: one can do much more than you think!

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)
8 Downloads (Pure)

Abstract

Model checking is an automated verification technique that actively is applied to find bugs in hardware and software designs. Companies like IBM and Cadence developed their in-house model checkers, and acted as driving forces behind the design of the IEEE-standardized temporal logic PSL. On the other hand, model checking C-, C#- and .NET-program code is an intensive research topic at, for instance, Microsoft and NASA. In this short paper, we briefly discuss three non-standard applications of model checking. The first example is taken from systems biology and shows the relevance of probabilistic reachability. Then, we show how to determine the optimal scheduling policy for multiple-battery systems so as to optimize the system’s lifetime. Finally, we discuss a stochastic job scheduling problem that —thanks to recent developments— can be solved using model checking.
Original languageEnglish
Title of host publicationFundamentals of Software Engineering
Subtitle of host publicationfourth IPM International Conference, FSEN 2011
Place of PublicationBerlin
PublisherSpringer
Pages1-14
Number of pages14
ISBN (Print)978-3-642-29319-1
DOIs
Publication statusPublished - 2012
Event4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011 - Teheran, Iran, Islamic Republic of
Duration: 20 Apr 201222 Apr 2012
Conference number: 4

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume7141
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011
Abbreviated titleFSEN
CountryIran, Islamic Republic of
CityTeheran
Period20/04/1222/04/12

Fingerprint

Model checking
Scheduling
Temporal logic
Software design
NASA
Hardware
Industry

Keywords

  • EWI-22519
  • METIS-293192
  • IR-83410

Cite this

Katoen, J. P. (2012). Model checking: one can do much more than you think! In Fundamentals of Software Engineering: fourth IPM International Conference, FSEN 2011 (pp. 1-14). (Lecture Notes in Computer Science; Vol. 7141). Berlin: Springer. https://doi.org/10.1007/978-3-642-29320-7_1
Katoen, Joost P. / Model checking: one can do much more than you think!. Fundamentals of Software Engineering: fourth IPM International Conference, FSEN 2011. Berlin : Springer, 2012. pp. 1-14 (Lecture Notes in Computer Science).
@inproceedings{95109cafd212477790bb73cb89898253,
title = "Model checking: one can do much more than you think!",
abstract = "Model checking is an automated verification technique that actively is applied to find bugs in hardware and software designs. Companies like IBM and Cadence developed their in-house model checkers, and acted as driving forces behind the design of the IEEE-standardized temporal logic PSL. On the other hand, model checking C-, C#- and .NET-program code is an intensive research topic at, for instance, Microsoft and NASA. In this short paper, we briefly discuss three non-standard applications of model checking. The first example is taken from systems biology and shows the relevance of probabilistic reachability. Then, we show how to determine the optimal scheduling policy for multiple-battery systems so as to optimize the system’s lifetime. Finally, we discuss a stochastic job scheduling problem that —thanks to recent developments— can be solved using model checking.",
keywords = "EWI-22519, METIS-293192, IR-83410",
author = "Katoen, {Joost P.}",
note = "Revised Selected Papers",
year = "2012",
doi = "10.1007/978-3-642-29320-7_1",
language = "English",
isbn = "978-3-642-29319-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "1--14",
booktitle = "Fundamentals of Software Engineering",

}

Katoen, JP 2012, Model checking: one can do much more than you think! in Fundamentals of Software Engineering: fourth IPM International Conference, FSEN 2011. Lecture Notes in Computer Science, vol. 7141, Springer, Berlin, pp. 1-14, 4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011, Teheran, Iran, Islamic Republic of, 20/04/12. https://doi.org/10.1007/978-3-642-29320-7_1

Model checking: one can do much more than you think! / Katoen, Joost P.

Fundamentals of Software Engineering: fourth IPM International Conference, FSEN 2011. Berlin : Springer, 2012. p. 1-14 (Lecture Notes in Computer Science; Vol. 7141).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Model checking: one can do much more than you think!

AU - Katoen, Joost P.

N1 - Revised Selected Papers

PY - 2012

Y1 - 2012

N2 - Model checking is an automated verification technique that actively is applied to find bugs in hardware and software designs. Companies like IBM and Cadence developed their in-house model checkers, and acted as driving forces behind the design of the IEEE-standardized temporal logic PSL. On the other hand, model checking C-, C#- and .NET-program code is an intensive research topic at, for instance, Microsoft and NASA. In this short paper, we briefly discuss three non-standard applications of model checking. The first example is taken from systems biology and shows the relevance of probabilistic reachability. Then, we show how to determine the optimal scheduling policy for multiple-battery systems so as to optimize the system’s lifetime. Finally, we discuss a stochastic job scheduling problem that —thanks to recent developments— can be solved using model checking.

AB - Model checking is an automated verification technique that actively is applied to find bugs in hardware and software designs. Companies like IBM and Cadence developed their in-house model checkers, and acted as driving forces behind the design of the IEEE-standardized temporal logic PSL. On the other hand, model checking C-, C#- and .NET-program code is an intensive research topic at, for instance, Microsoft and NASA. In this short paper, we briefly discuss three non-standard applications of model checking. The first example is taken from systems biology and shows the relevance of probabilistic reachability. Then, we show how to determine the optimal scheduling policy for multiple-battery systems so as to optimize the system’s lifetime. Finally, we discuss a stochastic job scheduling problem that —thanks to recent developments— can be solved using model checking.

KW - EWI-22519

KW - METIS-293192

KW - IR-83410

U2 - 10.1007/978-3-642-29320-7_1

DO - 10.1007/978-3-642-29320-7_1

M3 - Conference contribution

SN - 978-3-642-29319-1

T3 - Lecture Notes in Computer Science

SP - 1

EP - 14

BT - Fundamentals of Software Engineering

PB - Springer

CY - Berlin

ER -

Katoen JP. Model checking: one can do much more than you think! In Fundamentals of Software Engineering: fourth IPM International Conference, FSEN 2011. Berlin: Springer. 2012. p. 1-14. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-29320-7_1