An industrial application of symbolic model checking
The TWIN elevator case study |
| |
| Authors: | Florian Kammüller and S?ren Preibusch |
| |
| Institution: | (1) IBM Haifa Research Laboratory, Mount Carmel, Haifa, 31905, Israel;(2) Hebrew University, School of Engineering and Computer Science, Jerusalem, 91904, Israel;(3) Department of Computer Science, Rice University, Houston, TX, 77251-1892, U.S.A. |
| |
| 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. |
| |
| Keywords: | |
| 本文献已被 SpringerLink 等数据库收录！ |
|
