NDLI: Exploiting transition locality in automatic verification of finite-state concurrent systems

Content Provider	Springer Nature Link
Author	Della Penna, Giuseppe Intrigila, Benedetto Melatti, Igor Tronci, Enrico Venturini Zilli, Marisa
Copyright Year	2004
Abstract	In this paper we show that statistical properties of the transition graph of a system to be verified can be exploited to improve memory or time performances of verification algorithms.We show experimentally that protocols exhibit transition locality. That is, with respect to levels of a breadth-first state space exploration, state transitions tend to be between states belonging to close levels of the transition graph. We support our claim by measuring transition locality for the set of protocols included in the Murϕ verifier distribution .We present a cache-based verification algorithm that exploits transition locality to decrease memory usage and a disk-based verification algorithm that exploits transition locality to decrease disk read accesses, thus reducing the time overhead due to disk usage. Both algorithms have been implemented within the Murϕ verifier.Our experimental results show that our cache-based algorithm can typically save more than 40% of memory with an average time penalty of about 50% when using (Murϕ) bit compression and 100% when using bit compression and hash compaction, whereas our disk-based verification algorithm is typically more than ten times faster than a previously proposed disk-based verification algorithm and, even when using 10% of the memory needed to complete verification, it is only between 40 and 530% (300% on average) slower than (RAM) Murϕ with enough memory to complete the verification task at hand. Using just 300 MB of memory our disk-based Murϕ was able to complete verification of a protocol with about 109 reachable states. This would require more than 5 GB of memory using standard Murϕ .
Starting Page	320
Ending Page	341
Page Count	22
File Format	PDF
ISSN	14332779
Journal	International Journal on Software Tools for Technology Transfer
Volume Number	6
Issue Number	4
e-ISSN	14332787
Language	English
Publisher	Springer Berlin Heidelberg
Publisher Date	2004-07-06
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Automatic verification Model checking Explicit state space exploration Software Engineering Software Engineering/Programming and Operating Systems Theory of Computation
Content Type	Text
Resource Type	Article
Subject	Information Systems Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Exploring very large state spaces using genetic algorithms

Finite horizon analysis of Markov Chains with the Murϕ verifier

Domain-specific regular acceleration

Regular model checking

Parallel search for LTL violations

Introductory Paper

Directed explicit-state model checking in the validation of communication protocols

LTL generalized model checking revisited

BMC via on-the-fly determinization

Exploiting transition locality in automatic verification of finite-state concurrent systems

Similar Documents

Exploring very large state spaces using genetic algorithms

Finite horizon analysis of Markov Chains with the Murϕ verifier

Domain-specific regular acceleration

Regular model checking

Parallel search for LTL violations

Introductory Paper

Directed explicit-state model checking in the validation of communication protocols

LTL generalized model checking revisited

BMC via on-the-fly determinization

Exploiting transition locality in automatic verification of finite-state concurrent systems