An industrial application of symbolic model checking |
| |
Authors: | Florian Kammüller and S?ren Preibusch |
| |
Affiliation: | (1) Technische Universit?t Berlin, Franklinstra?e 28/29, 10587 Berlin, Germany;(2) German Institute for Economic Research (DIW Berlin), Berlin, Germany |
| |
Abstract: | Model checking techniques are recognized to provide reliable and copious results. Instead of examining a few cases only – as it is done in testing – model checking includes the whole state space in mathematical proofs of correctness. Yet, this completeness is seen as a drawback as the state explosion problem is hard to handle. In our industrial case study, we apply automated model checking techniques to an innovative elevator system, the TWIN by ThyssenKrupp. By means of abstraction and nondeterminism, we cope with runtime behaviour and achieve to efficiently prove our specification’s validity. The elevator’s safety requirements are exhaustively expressed in temporal logic along with real-world and algorithmic prerequisites, consistency properties, and fairness constraints. Beyond verifying system safety for an actual installation, our case study demonstrates the rewarding applicability of model checking at an industrial scale. CR subject classification D.2.4; F.3.1; J.7 ; C.3 |
| |
Keywords: | Symbolic Model Checking Mechanical Verification Industrial Case Study State Based Systems Safety SMV |
本文献已被 SpringerLink 等数据库收录! |
|