%0 Conference Paper %1 691741 %A Baukus, Kai %A Bensalem, Saddek %A Lakhnech, Yassine %A Stahl, Karsten %B TACAS '00: Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems %C London, UK %D 2000 %I Springer-Verlag %K abstraction concurrent finite_state parameterized verification ws1s %P 188--203 %T Abstracting WS1S Systems to Verify Parameterized Networks %U http://portal.acm.org/citation.cfm?id=691741 %X We present a method that allows to verify parameterized networks of finite state processes. Our method is based on three main ideas. The first one consists in modeling an infinite family of networks by a single WS1S transition system, that is, a transition system whose variables are set (2nd-order) variables and whose transitions are described in WS1S. Then, we present methods that allow to abstract a WS1S system into a finite state system that can be model-checked. Finally, in order to verify liveness properties, we present an algorithm that allows to enrich the abstract system with strong fairness conditions while preserving safety of the abstraction. We implemented our method in a tool, called PAX, and applied it to several examples. %@ 3-540-67282-6

@inproceedings{691741, abstract = {We present a method that allows to verify parameterized networks of finite state processes. Our method is based on three main ideas. The first one consists in modeling an infinite family of networks by a single WS1S transition system, that is, a transition system whose variables are set (2nd-order) variables and whose transitions are described in WS1S. Then, we present methods that allow to abstract a WS1S system into a finite state system that can be model-checked. Finally, in order to verify liveness properties, we present an algorithm that allows to enrich the abstract system with strong fairness conditions while preserving safety of the abstraction. We implemented our method in a tool, called PAX, and applied it to several examples.}, added-at = {2010-01-11T16:24:53.000+0100}, address = {London, UK}, author = {Baukus, Kai and Bensalem, Saddek and Lakhnech, Yassine and Stahl, Karsten}, biburl = {https://www.bibsonomy.org/bibtex/2ae8fa0457ab6a2fc91e197e8b6254ff9/giuliano.losa}, booktitle = {TACAS '00: Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems}, description = {Abstracting WS1S Systems to Verify Parameterized Networks}, interhash = {1468283cf4ca9f6d49e461898952f7fa}, intrahash = {ae8fa0457ab6a2fc91e197e8b6254ff9}, isbn = {3-540-67282-6}, keywords = {abstraction concurrent finite_state parameterized verification ws1s}, pages = {188--203}, publisher = {Springer-Verlag}, timestamp = {2010-01-28T12:12:57.000+0100}, title = {Abstracting WS1S Systems to Verify Parameterized Networks}, url = {http://portal.acm.org/citation.cfm?id=691741}, year = 2000 }