Using partial order techniques to improve performance of data flow analysis based verification
Pages 57 - 65
Abstract
Partial order optimization techniques for distributed systems improve the performance of finite state verification approaches by avoiding redundant exploration of some portions of the state space. Previously, such techniques have been applied in the context of model checking approaches. In this paper we propose a partial order optimization of the program model used by FLAVERS, a data flow based finite state verification approach for checking user-specified properties of distributed software. We demonstrate experimentally that this optimization often leads to significant reductions in the run time of the analysis algorithm of FLAVERS. On average, for those cases where this optimization could be applied, we observed a speedup of 21%. For one of the cases, the optimization resulted in an analysis speedup of 91%.
References
[1]
J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on Software Engineering, 22(3): 161-180, Mar. 1996.
[2]
M. B. Dwyer and L. A. Clarke. Data flow analysis for verifying properties of concurrent programs. In Proceedings of the 2nd ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 62-75, Dec. 1994.
[3]
P. Godefroid. Model checking for programming languages using VeriSoft. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pages 174-186, Jan. 1997.
[4]
P. Godefroid, R. S. Hanmer, and L. J. Jagadeesan. Model checking without a model: an analysis of the Heart-Beat Monitor of a telephone switch using VeriSoft. In Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 124-133, Mar. 1998.
[5]
P. Godefroid, D. Peled, and M. Staskauskas. Using partial-order methods in the formal validation of industrial concurrent programs. IEEE Transactions on Software Engineering, 22(7):496-507, July 1996.
[6]
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proceedings of the 3rd International Workshop on Computer Aided Verification, pages 332-342, July 1992.
[7]
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall Software Series, 1991.
[8]
S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, (6): 107-l 20, 1992.
[9]
G. Naumovich and G. S. Avrunin. A conservative data flow algorithm for detecting all pairs of statements that may happen in parallel. In Proceedings of the 6th ACM SIGSOFT Symposium on the Foundations qf Software Engineering, pages 24-34, Nov. 1998.
[10]
G. Naumovich, G. S. Avrunin, and L. A. Clarke. Data flow analysis for checking properties of concurrent Java programs. In Proceedings of the 2lst International Conference on Software Engineering, pages 399-410, May 1999.
[11]
G. Naumovich, G. S. Avrunin, L. A. Clarke, and L. J. Osterweil. Applying static analysis to software architectures. In Proceedings of the 6th European Software Engineering Conference and 5th ACM SIG- SOFTSymposium on the Foundations of Software Engineering, pages 77-93, Nov. 1997.
[12]
D. Peled. Combining partial order reductions with on-the-fly model checking. In Proceedings of the 6th International Conference on Computer Aided Verification, pages 377-390, June 1994.
[13]
A. Valmari. A stubborn attack on state explosion. In Proceedings of Computer-Aided Verification (CAV'90), pages 156-165, June 1991.
Index Terms
- Using partial order techniques to improve performance of data flow analysis based verification
Recommendations
Using partial order techniques to improve performance of data flow analysis based verification
PASTE '99: Proceedings of the 1999 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineeringPartial order optimization techniques for distributed systems improve the performance of finite state verification approaches by avoiding redundant exploration of some portions of the state space. Previously, such techniques have been applied in the ...
Cluster-Based Partial-Order Reduction
The verification of concurrent systems through an exhaustive traversal of the state space suffers from the infamous state-space-explosion problem, caused by the many interleavings of actions of different processes in the system. Partial-order reduction ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 1999 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 September 1999
Published in SIGSOFT Volume 24, Issue 5
Check for updates
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations8Total Citations
- 354Total Downloads
- Downloads (Last 12 months)68
- Downloads (Last 6 weeks)11
Reflects downloads up to 07 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in