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

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

    2 Citations (Scopus)
    21 Downloads (Pure)


    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
    Number of pages14
    ISBN (Print)978-3-642-29319-1
    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
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011
    Abbreviated titleFSEN
    CountryIran, Islamic Republic of


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


    Dive into the research topics of 'Model checking: one can do much more than you think!'. Together they form a unique fingerprint.

    Cite this