Generating Scenarios by Multi-Object Checking |
| |
Authors: | Maik Kollmann Yuen Man Hon |
| |
Affiliation: | aInstitute of Information Systems, Technical University Braunschweig, Mühlenpfordtstraße 23, 38106 Braunschweig, Germany;bInstitute for Railway Systems Engineering and Traffic Safety, Technical University Braunschweig, Pockelsstraße 3, 38106 Braunschweig, Germany |
| |
Abstract: | These days, many systems are developed applying various UML notations to represent the structure and behavior of (technical) systems. In addition, for safety critical systems like Railway Interlocking Systems (RIS) the fulfillment of safety requirements is demanded. UML-based Railway Interlocking (UML-based RI) is proposed as a methodology in designing and developing RIS. It consists of infrastructure objects and UML is used to model the system behavior. This design is validated and demonstrated by using simulation with Rhapsody. Automated verification techniques like model checking have become a standard for proving the correctness of state-based systems. Unfortunately, one major problem of model checking is the state space explosion if too many objects have to be taken into account. Multi-object checking circumvents the state space explosion by checking one object at a time. We present an approach to enhance multi-object checking by generating counterexamples in a sequence diagram fashion providing scenarios for model-based testing. |
| |
Keywords: | Scenario Generation Counterexample Generation State Modeling Multi-Object Checking UML-based Railway Interlocking System |
本文献已被 ScienceDirect 等数据库收录! |
|