publication . Part of book or chapter of book . Other literature type . 2000

Abstracting WS1S Systems to Verify Parameterized Networks

Baukus, Kai; Bensalem, Saddek; Lakhnech, Yassine; Stahl, Karsten;
  • Published: 01 Jan 2000
  • Publisher: Springer Berlin Heidelberg
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 imple...
Download fromView all 2 versions
Other literature type . 2000
Provider: Datacite
Part of book or chapter of book . 2007
Provider: Crossref
Powered by OpenAIRE Research Graph
Any information missing or wrong?Report an Issue