%0 Journal Article %1 amir2003modelchecking %A Pnueli, Amir %A Zuck, Lenore %D 2003 %J Verification, Model Checking, and Abstract Interpretation %K abstraction invariant modelchecking parameterized survey verification %P 4--4 %T Model-Checking and Abstraction to the Aid of Parameterized Systems %U http://dx.doi.org/10.1007/3-540-36384-X_2 %X Parameterized systems are systems that involve numerous instantiations of the same finite-state module. Examples of parameterized systems include tele-communication protocols, bus protocols, cache coherence protocols, and many other protocols that underlycurrent state-of-the-art systems. Formal verification of parameterized systems is known to be undecidable AK86 and thus cannot be automated. Recent research has shown that in many cases it is possible to use abstraction methods to generate a finite-state systems from a parameterized systems. The finite-state system can then be model-checked. If successful,it is possible to conclude that the original parameterized system satisfies its requirements. Otherwise, it is often the casethat the counter-example produced by the model checker can indicate an error in the original parameterized system. This combinedtechnique allows for automatic verification of parameterized systems.

@article{amir2003modelchecking, abstract = {Parameterized systems are systems that involve numerous instantiations of the same finite-state module. Examples of parameterized systems include tele-communication protocols, bus protocols, cache coherence protocols, and many other protocols that underlycurrent state-of-the-art systems. Formal verification of parameterized systems is known to be undecidable [AK86] and thus cannot be automated. Recent research has shown that in many cases it is possible to use abstraction methods to generate a finite-state systems from a parameterized systems. The finite-state system can then be model-checked. If successful,it is possible to conclude that the original parameterized system satisfies its requirements. Otherwise, it is often the casethat the counter-example produced by the model checker can indicate an error in the original parameterized system. This combinedtechnique allows for automatic verification of parameterized systems.}, added-at = {2010-04-20T11:27:44.000+0200}, author = {Pnueli, Amir and Zuck, Lenore}, biburl = {https://www.bibsonomy.org/bibtex/244fe66e4bb41d40616b6ec70ca0bb345/giuliano.losa}, description = {SpringerLink - Book Chapter}, interhash = {5ed34e9f094739720082e2921bc6f7d1}, intrahash = {44fe66e4bb41d40616b6ec70ca0bb345}, journal = {Verification, Model Checking, and Abstract Interpretation}, keywords = {abstraction invariant modelchecking parameterized survey verification}, pages = {4--4}, timestamp = {2010-04-20T11:27:44.000+0200}, title = {Model-Checking and Abstraction to the Aid of Parameterized Systems}, url = {http://dx.doi.org/10.1007/3-540-36384-X_2}, year = 2003 }