Model checking embedded system designs

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

5 Citations (Scopus)
31 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