@giuliano.losa

Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)

, , , und . Tools and Algorithms for the Construction and Analysis of Systems, (2007)

Zusammenfassung

We give a simple and efficient method 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. Processesmay communicate via broadcast, rendez-vous and shared variables. The method derives an over-approximation of the induced transitionsystem, which allows the use of a simple class of regular expressions as a symbolic representation. Compared to traditionalregular model checking methods, the analysis does not require the manipulation of transducers, and hence its simplicity andefficiency. We have implemented a prototype which works well on several mutual exclusion algorithms and cache coherence protocols.

Beschreibung

Regular Model Checking Without Transducers

Links und Ressourcen

Tags

Community

  • @giuliano.losa
  • @dblp
@giuliano.losas Tags hervorgehoben