![]() Although, for a liveness property, this trace may not be the shortest possible. However, in our experience, the algorithm used by Spin is generally successful in finding a witness trace that is considerably shorter than those created by the first traces mode for safety as well as liveness properties. It is important to note that Spin only guarantees this trace to be the shortest for safety properties. Therefore, shorter traces are commonly easier to understand. It excludes irrelevant steps that may be performed by concurrent components. The shortest witness trace for a property is the minimal behavior the system per- forms for a requirement. ![]() ) 2) Shortest trace: Spin offers an algorithm for iteratively finding the shortest trace. (This assessment corresponds with the findings presented in. While this mode is the fastest, the generated witness traces are often unnecessarily long and complex, since they rep- resent the first violations encountered in a depth-first search. 1) First traces: In this mode, the first x witness traces encountered by the model checker are stored. Therefore, our process offers three modes for generating different witness traces, from which different witness scenarios may be created. Rather, it may be necessary to visualize several witness scenarios to understand how a requirement is modeled in a system. A single witness scenario may not be sufficient to com- pletely understand how the system model captures a requirement, since it only shows a single instance of such a system execution. The modification of the model should be done using our round-trip UML modeling approach, so that the model adheres to its critical properties after the modification is completed. For example, the environment model of the system may need to be extended so that the system ex- hibits the desired witness scenarios. In general, developers may need to revise such a system model. However, if the model checker does not detect a witness trace for the property in the state space, then no trace in the system model adheres to the functional requirement of interest. Since model checkers are most effective in finding and generating violation traces, the model checker commonly finds such traces traversing only a small portion of the model’s state space. If the model checker finds a violation trace of the complementary property, then the uncovered trace is a witness trace of the original property. This complementary property is passed to the model checker. For instance, the complement of Expression 2 is read as “Globally, it is never the case that P followed by S ”. Specifically, we specify the complement of the LTL property. In this paper, we describe how the model checker Spin can be used to create such witness traces for a property. A witness trace, as opposed to a violation trace, represents a sequence of steps executed by the system that adheres to the specified property, instead of violating it. The witness scenarios are created from witness traces generated by the model checker. In contrast to the previous technique, this work presents the generation and visualization of witness scenarios in terms of the original UML model. If a sequence is uncovered that violates the specified property, then the model checker provides this sequence as a violation trace, which may be used by our visualization framework and Theseus for the visualization of a property violation (this process is described in ). Model checkers, in general, search for violations of a property by traversing the complete state space of the system, thereby analyzing every possible execution sequence. Next, the LTL property created with S PIDER is used by a formal analysis tool, i.e. the end of this step, the developer has created a formally analyzable specification of the scenario to be visualized in the UML model.
0 Comments
Leave a Reply. |