Model checking embedded system designs

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

    5 Citations (Scopus)
    37 Downloads (Pure)

    Abstract

    Model checking has established itself as a successful tool supported technique for the verification and debugging of various hardware and software systems [16]. Not only in academia, but also by industry this technique is increasingly being regarded as a promising and practical proposition, especially in the area of hardware verification [22]. Model checking is also being applied with success to the analysis of the control software in embedded systems [37]. Because such systems are often mission critical, in the sense that their failure to operate correctly can be very costly in terms of cost and safety, there is a natural tendency to apply advanced methods to guide and analyse their design. Because model checkers typically trace the behaviour leading to the explored states they can be used not only analytically, i.e. to verify that given control designs are correct, but also synthetically, i.e. to derive or optimize control designs. Examples of such controller synthesis in the context of timed automata can be found in [31, 7]. In this extended abstract we survey the basic principles behind the application of model checking to controller verification and synthesis. Although the development of model checkers for sophisticated models of system behaviour is a nontrivial task, the conceptual ingredients often remain straightforward. The major problem besetting model checking, as with many tools dealing with concurrent systems, is the infamous state space explosion, caused by the fact that the global state space of a system grows exponentially with the local state spaces of its components. The more sophisticated the model of behaviour, the more difficult to control this phenomenon effectively. This makes abstract modelling and state space search techniques decisive practical ingredients of model checking applications, more than the sophistication of the behavioural model that is supported. A promising development is the area of guided model checking, in which the state space search strategy of the model checking algorithm can be influenced to visit more interesting sets of states first. In particular, we will discuss how model checking can be combined with heuristic cost functions to guide search strategies. In the final section of this extended abstract we list a number of current research developments, especially in the area of reachability analysis for optimal control and related issues.
    Original languageUndefined
    Title of host publication6th Int. Workshop on Discrete Event Systems (WODES)
    Place of PublicationLos Alamitos, California
    PublisherIEEE Computer Society
    Pages151-158
    Number of pages8
    ISBN (Print)0-7695-1683-1
    DOIs
    Publication statusPublished - Oct 2002

    Publication series

    Name
    PublisherIEEE Computer Society

    Keywords

    • EWI-2740
    • IR-38268
    • METIS-209589

    Cite this

    Brinksma, H., & Mader, A. H. (2002). Model checking embedded system designs. In 6th Int. Workshop on Discrete Event Systems (WODES) (pp. 151-158). Los Alamitos, California: IEEE Computer Society. https://doi.org/10.1109/WODES.2002.1167682
    Brinksma, Hendrik ; Mader, Angelika H. / Model checking embedded system designs. 6th Int. Workshop on Discrete Event Systems (WODES). Los Alamitos, California : IEEE Computer Society, 2002. pp. 151-158
    @inproceedings{120f6ffb4a644cbe8f0d17cf68dc4fab,
    title = "Model checking embedded system designs",
    abstract = "Model checking has established itself as a successful tool supported technique for the verification and debugging of various hardware and software systems [16]. Not only in academia, but also by industry this technique is increasingly being regarded as a promising and practical proposition, especially in the area of hardware verification [22]. Model checking is also being applied with success to the analysis of the control software in embedded systems [37]. Because such systems are often mission critical, in the sense that their failure to operate correctly can be very costly in terms of cost and safety, there is a natural tendency to apply advanced methods to guide and analyse their design. Because model checkers typically trace the behaviour leading to the explored states they can be used not only analytically, i.e. to verify that given control designs are correct, but also synthetically, i.e. to derive or optimize control designs. Examples of such controller synthesis in the context of timed automata can be found in [31, 7]. In this extended abstract we survey the basic principles behind the application of model checking to controller verification and synthesis. Although the development of model checkers for sophisticated models of system behaviour is a nontrivial task, the conceptual ingredients often remain straightforward. The major problem besetting model checking, as with many tools dealing with concurrent systems, is the infamous state space explosion, caused by the fact that the global state space of a system grows exponentially with the local state spaces of its components. The more sophisticated the model of behaviour, the more difficult to control this phenomenon effectively. This makes abstract modelling and state space search techniques decisive practical ingredients of model checking applications, more than the sophistication of the behavioural model that is supported. A promising development is the area of guided model checking, in which the state space search strategy of the model checking algorithm can be influenced to visit more interesting sets of states first. In particular, we will discuss how model checking can be combined with heuristic cost functions to guide search strategies. In the final section of this extended abstract we list a number of current research developments, especially in the area of reachability analysis for optimal control and related issues.",
    keywords = "EWI-2740, IR-38268, METIS-209589",
    author = "Hendrik Brinksma and Mader, {Angelika H.}",
    note = "Imported from DIES",
    year = "2002",
    month = "10",
    doi = "10.1109/WODES.2002.1167682",
    language = "Undefined",
    isbn = "0-7695-1683-1",
    publisher = "IEEE Computer Society",
    pages = "151--158",
    booktitle = "6th Int. Workshop on Discrete Event Systems (WODES)",
    address = "United States",

    }

    Brinksma, H & Mader, AH 2002, Model checking embedded system designs. in 6th Int. Workshop on Discrete Event Systems (WODES). IEEE Computer Society, Los Alamitos, California, pp. 151-158. https://doi.org/10.1109/WODES.2002.1167682

    Model checking embedded system designs. / Brinksma, Hendrik; Mader, Angelika H.

    6th Int. Workshop on Discrete Event Systems (WODES). Los Alamitos, California : IEEE Computer Society, 2002. p. 151-158.

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

    TY - GEN

    T1 - Model checking embedded system designs

    AU - Brinksma, Hendrik

    AU - Mader, Angelika H.

    N1 - Imported from DIES

    PY - 2002/10

    Y1 - 2002/10

    N2 - Model checking has established itself as a successful tool supported technique for the verification and debugging of various hardware and software systems [16]. Not only in academia, but also by industry this technique is increasingly being regarded as a promising and practical proposition, especially in the area of hardware verification [22]. Model checking is also being applied with success to the analysis of the control software in embedded systems [37]. Because such systems are often mission critical, in the sense that their failure to operate correctly can be very costly in terms of cost and safety, there is a natural tendency to apply advanced methods to guide and analyse their design. Because model checkers typically trace the behaviour leading to the explored states they can be used not only analytically, i.e. to verify that given control designs are correct, but also synthetically, i.e. to derive or optimize control designs. Examples of such controller synthesis in the context of timed automata can be found in [31, 7]. In this extended abstract we survey the basic principles behind the application of model checking to controller verification and synthesis. Although the development of model checkers for sophisticated models of system behaviour is a nontrivial task, the conceptual ingredients often remain straightforward. The major problem besetting model checking, as with many tools dealing with concurrent systems, is the infamous state space explosion, caused by the fact that the global state space of a system grows exponentially with the local state spaces of its components. The more sophisticated the model of behaviour, the more difficult to control this phenomenon effectively. This makes abstract modelling and state space search techniques decisive practical ingredients of model checking applications, more than the sophistication of the behavioural model that is supported. A promising development is the area of guided model checking, in which the state space search strategy of the model checking algorithm can be influenced to visit more interesting sets of states first. In particular, we will discuss how model checking can be combined with heuristic cost functions to guide search strategies. In the final section of this extended abstract we list a number of current research developments, especially in the area of reachability analysis for optimal control and related issues.

    AB - Model checking has established itself as a successful tool supported technique for the verification and debugging of various hardware and software systems [16]. Not only in academia, but also by industry this technique is increasingly being regarded as a promising and practical proposition, especially in the area of hardware verification [22]. Model checking is also being applied with success to the analysis of the control software in embedded systems [37]. Because such systems are often mission critical, in the sense that their failure to operate correctly can be very costly in terms of cost and safety, there is a natural tendency to apply advanced methods to guide and analyse their design. Because model checkers typically trace the behaviour leading to the explored states they can be used not only analytically, i.e. to verify that given control designs are correct, but also synthetically, i.e. to derive or optimize control designs. Examples of such controller synthesis in the context of timed automata can be found in [31, 7]. In this extended abstract we survey the basic principles behind the application of model checking to controller verification and synthesis. Although the development of model checkers for sophisticated models of system behaviour is a nontrivial task, the conceptual ingredients often remain straightforward. The major problem besetting model checking, as with many tools dealing with concurrent systems, is the infamous state space explosion, caused by the fact that the global state space of a system grows exponentially with the local state spaces of its components. The more sophisticated the model of behaviour, the more difficult to control this phenomenon effectively. This makes abstract modelling and state space search techniques decisive practical ingredients of model checking applications, more than the sophistication of the behavioural model that is supported. A promising development is the area of guided model checking, in which the state space search strategy of the model checking algorithm can be influenced to visit more interesting sets of states first. In particular, we will discuss how model checking can be combined with heuristic cost functions to guide search strategies. In the final section of this extended abstract we list a number of current research developments, especially in the area of reachability analysis for optimal control and related issues.

    KW - EWI-2740

    KW - IR-38268

    KW - METIS-209589

    U2 - 10.1109/WODES.2002.1167682

    DO - 10.1109/WODES.2002.1167682

    M3 - Conference contribution

    SN - 0-7695-1683-1

    SP - 151

    EP - 158

    BT - 6th Int. Workshop on Discrete Event Systems (WODES)

    PB - IEEE Computer Society

    CY - Los Alamitos, California

    ER -

    Brinksma H, Mader AH. Model checking embedded system designs. In 6th Int. Workshop on Discrete Event Systems (WODES). Los Alamitos, California: IEEE Computer Society. 2002. p. 151-158 https://doi.org/10.1109/WODES.2002.1167682