9.2. Algorithms for Generating Scenario Graphs
We present two algorithms for generating scenario graphs. The first is based on symbolic model checking and produces counterexamples for only safety properties, as expressed in terms of a computational tree logic. The second is based on explicit-state model checking and produces counterexamples for both safety and liveness properties, as expressed in terms of a linear temporal logic.
Both algorithms produce scenario graphs that guarantee the following informally stated properties:
Soundness: Each path in the graph is a violation of the given property.
Exhaustive: The graph contains all executions of the model that violate the given property.
Succinctness of states: Each node in the graph represents ...
Get Information Assurance now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
