TY - GEN

T1 - An efficient state space generation for analysis of real-time systems

AU - Kang, Inhye

AU - Lee, Insup

N1 - Publisher Copyright:
© 1996 ACM.

PY - 1996/5/1

Y1 - 1996/5/1

N2 - State explosion is a well-known problem that impedes analysis and testing based on state-space exploration. This problem is particularly serious in real-time systems because unbounded time values cause the state space to be infinite. In this paper, we present an algorithm that produces a compact representation of reachable state space of a real-time system. The algorithm yields a small state space, but still retains enough timing information for analysis. To avoid the state explosion which can be caused by simply adding time values to states, our algorithm first uses history equivalence and transition bisimulation to collapse states into equivalent classes. In this approach, equivalent states have identical observable events although transitions into the states may happen at different times. The algorithm then augments the resultant state space with timing relations that describe time distances between transition executions. For example, the relation @ (tr"1) + 3 ≤ @ (tr"2) ≤ @ (tr"1) + 5 means that transition tr"2 is taken 3 to 5 time units before transition tr"2 is taken. This is used to analyze timing properties such as minimum and maximum time distances between events. To show the effectiveness of our algorithm, we have implemented the algorithm and are currently comparing it to other existing techniques which generate state space for real-time systems.

AB - State explosion is a well-known problem that impedes analysis and testing based on state-space exploration. This problem is particularly serious in real-time systems because unbounded time values cause the state space to be infinite. In this paper, we present an algorithm that produces a compact representation of reachable state space of a real-time system. The algorithm yields a small state space, but still retains enough timing information for analysis. To avoid the state explosion which can be caused by simply adding time values to states, our algorithm first uses history equivalence and transition bisimulation to collapse states into equivalent classes. In this approach, equivalent states have identical observable events although transitions into the states may happen at different times. The algorithm then augments the resultant state space with timing relations that describe time distances between transition executions. For example, the relation @ (tr"1) + 3 ≤ @ (tr"2) ≤ @ (tr"1) + 5 means that transition tr"2 is taken 3 to 5 time units before transition tr"2 is taken. This is used to analyze timing properties such as minimum and maximum time distances between events. To show the effectiveness of our algorithm, we have implemented the algorithm and are currently comparing it to other existing techniques which generate state space for real-time systems.

UR - http://www.scopus.com/inward/record.url?scp=85011809633&partnerID=8YFLogxK

U2 - 10.1145/229000.226297

DO - 10.1145/229000.226297

M3 - Conference contribution

AN - SCOPUS:85011809633

T3 - Proceedings of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1996

SP - 4

EP - 13

BT - Proceedings of the 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1996

A2 - Tracz, Will

A2 - Zeil, Steve J.

PB - Association for Computing Machinery, Inc

T2 - 1996 ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 1996

Y2 - 8 January 1996 through 10 January 1996

ER -