Equational Abstractions for Software Model Checking
M. Neuhäußer, Th. Noll, L.H. Haß, P. Tawiah
The combinatorial explosion of state spaces is the biggest challenge in applying model-checking methods to concurrent systems. The goal of this project is to develop a new state-space reduction technique that is tailored to system specifications in Rewriting Logic, a unified semantic framework for concurrency which is based on conditional term rewriting modulo equational theories. The idea is to hide "unimportant" details of the system's behavior (such as internal computations) in the equations, and to represent only "interesting" state changes (such as communication operations) by explicit transitions. Our results show that this optimization can be implemented by transforming the Rewriting Logic specification, avoiding the intermediate construction of the full state space. The correctness of our technique can be established by proving that the original and the reduced system are weakly bisimilar.
The usability of this approach was demonstrated by applying it to the concurrent functional programming language Erlang, which is designed for implementing open, distributed telecommunication software. The inherent complexity and nondeterminacy of such systems impedes the use of validation methods which are purely based on testing. Therefore we developed a formalization of this language in the Rewriting Logic framework, employing equations for defining abstraction mappings on the state space of the system. This specification was implemented in the Maude system, and its model checker was employed to verify simple system properties.
M. Neuhäußer, Th. Noll, L.H. Haß, P. Tawiah
The combinatorial explosion of state spaces is the biggest challenge in applying model-checking methods to concurrent systems. The goal of this project is to develop a new state-space reduction technique that is tailored to system specifications in Rewriting Logic, a unified semantic framework for concurrency which is based on conditional term rewriting modulo equational theories. The idea is to hide "unimportant" details of the system's behavior (such as internal computations) in the equations, and to represent only "interesting" state changes (such as communication operations) by explicit transitions. Our results show that this optimization can be implemented by transforming the Rewriting Logic specification, avoiding the intermediate construction of the full state space. The correctness of our technique can be established by proving that the original and the reduced system are weakly bisimilar.
The usability of this approach was demonstrated by applying it to the concurrent functional programming language Erlang, which is designed for implementing open, distributed telecommunication software. The inherent complexity and nondeterminacy of such systems impedes the use of validation methods which are purely based on testing. Therefore we developed a formalization of this language in the Rewriting Logic framework, employing equations for defining abstraction mappings on the state space of the system. This specification was implemented in the Maude system, and its model checker was employed to verify simple system properties.
