TY - GEN
T1 - State space abstraction for parameterized self-stabilizing embedded systems
AU - Liveris, Nikolaos
AU - Zhou, Hai
AU - Dick, Robert P.
AU - Banerjee, Prithviraj
PY - 2008
Y1 - 2008
N2 - Self-stabilizing systems are systems that automatically recover from any transient fault. Proving the correctness of a parameterized self-stabilizing system, i.e., a system composed of an arbitrary number of processes, is a challenging task. For the verification of parameterized systems the method of control abstraction has been developed. However, control abstraction can only be applied to systems in which each process has a fixed number of observable variables. In this article, we propose a technique to abstract a parameterized self-stabilizing system, whose processes have a parameterized number of observable variables, to a system with fixed number of observable variables. This enables the use of control abstraction for verification. The proposed technique targets low-atomicity, shared-memory, asynchronous systems. We establish the completeness of the method under reasonable conditions and demonstrate its effectiveness by applying it on a number of self-stabilizing distributed systems.
AB - Self-stabilizing systems are systems that automatically recover from any transient fault. Proving the correctness of a parameterized self-stabilizing system, i.e., a system composed of an arbitrary number of processes, is a challenging task. For the verification of parameterized systems the method of control abstraction has been developed. However, control abstraction can only be applied to systems in which each process has a fixed number of observable variables. In this article, we propose a technique to abstract a parameterized self-stabilizing system, whose processes have a parameterized number of observable variables, to a system with fixed number of observable variables. This enables the use of control abstraction for verification. The proposed technique targets low-atomicity, shared-memory, asynchronous systems. We establish the completeness of the method under reasonable conditions and demonstrate its effectiveness by applying it on a number of self-stabilizing distributed systems.
KW - Abstraction
KW - Network invariants
KW - Parameterized systems
KW - Self-stabilizing systems
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=70349238974&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70349238974&partnerID=8YFLogxK
U2 - 10.1145/1450058.1450061
DO - 10.1145/1450058.1450061
M3 - Conference contribution
AN - SCOPUS:70349238974
SN - 9781605584683
T3 - Proceedings of the 8th ACM International Conference on Embedded Software, EMSOFT'08
SP - 11
EP - 20
BT - Proceedings of the 8th ACM International Conference on Embedded Software, EMSOFT'08
PB - Association for Computing Machinery (ACM)
T2 - 8th ACM International Conference on Embedded Software, EMSOFT 2008
Y2 - 19 October 2008 through 24 October 2008
ER -