Monotonic Abstraction: on Efficient Verification of Parameterized Systems
2009 (English)In: International Journal of Foundations of Computer Science, ISSN 0129-0541, Vol. 20, no 5, 779-801 p.Article in journal (Refereed) Published
We introduce the simple and efficient method of monotonic abstraction to prove safety properties for parameterized systems with linear topologies. A process in the system is a finite-state automaton, where the transitions are guarded by both local and global conditions. Processes may communicate via broadcast, rendez-vous and shared variables over finite domains. The method of monotonic abstraction derives an over-approximation of the induced transition system that allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditional regular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity and efficiency. We have implemented a prototype that works well on several mutual exclusion algorithms and cache coherence protocols
Place, publisher, year, edition, pages
2009. Vol. 20, no 5, 779-801 p.
IdentifiersURN: urn:nbn:se:uu:diva-130930DOI: 10.1142/S0129054109006887ISI: 000272248900002OAI: oai:DiVA.org:uu-130930DiVA: diva2:352097
ProjectsapvUPMARCautomated verification of highly concurrent algorithms