Article

Free access

Automatically closing open reactive programs

Authors:

Christopher Colby,

Patrice Godefroid,

Lalita Jategaonkar JagadeesanAuthors Info & Claims

PLDI '98: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation

Pages 345 - 357

https://doi.org/10.1145/277650.277754

Published: 01 May 1998 Publication History

Abstract

We study in this paper the problem of analyzing implementations of open systems --- systems in which only some of the components are present. We present an algorithm for automatically closing an open concurrent reactive system with its most general environment, i.e., the environment that can provide any input at any time to the system. The result is a nondeterministic closed (i.e., self-executable) system which can exhibit all the possible reactive behaviors of the original open system. These behaviors can then be analyzed using VeriSoft, an existing tool for systematically exploring the state spaces of closed systems composed of multiple (possibly nondeterministic) processes executing arbitrary code. We have implemented the techniques introduced in this paper in a prototype tool for automatically closing open programs written in the C programming language. We discuss preliminary experimental results obtained with a large telephone-switching software application developed at Lucent Technologies.

References

[1]

A. Aho, R. Sethi, and J. Ullman. Compilers: Princi. ples, Techniques and Tools. Addison-Wesley, 1986.

Digital Library

[2]

D. Callahan. The program summary graph and flowsensitive interprocedural data flow analysis. In Proceedings of the A CM '88 Conference on Programming Lanugage Design and Implementation, pages 47-56, Atlanta, GE, USA, June 1988. ACM Press.

Digital Library

[3]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Proceedings of the jth A CM Symposium on Principles of Programming Languages, Los Angeles, pages 238- 252, New York, NY, 1977. ACM.

Digital Library

[4]

E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. A CM Transactions on Programming Languages and Systems, 8(2):244-263, January 1986.

Digital Library

[5]

K.D. Cooper and K. Kennedy. Interprocedural sideeffect analysis in linear time. In David S. Wise, editor, Proceedings of the SIGPLAN '88 Conference on Programming Lanugage Design and Implementation (SIGPLAN '88), pages 57-66, Atlanta, GE, USA, June 1988. ACM Press.

Digital Library

[6]

C. Colby. Analyzing the communication topology of concurrent programs. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 202-213, New York, NY, USA, June 1995. ACM Press.

Digital Library

[7]

C. Colby. Semantics-based Program Analysis via Symbolic Composition of Transfer Relations. PhD thesis, Carnegie Mellon University, August 1996.

Digital Library

[8]

R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. A CM Transactions on Programming Languages and Systems, 1(15):36- 72, 1993.

Digital Library

[9]

R. Cridlig. Semantic analysis of shared-memory concurrent languages using abstract model-checking. In Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 214-225, New York, NY, USA, June 1995. ACM Press.

Digital Library

[10]

D.R. Chase, M. Wegrnan, and F.K. Zadeck. Analysis of pointers and structures. In Proccedings of Conference on Programming Language Design and Implementation, pages 296-310, June 1990.

Digital Library

[11]

A. Deutsch. Interprocedural May-Alias analysis for pointers: Beyond k-limiting. SIGPLAN Notices, 29(6):230-241, June 1994. Proceedings of the A GM SIGPLAN '9j Conference on Programming Language Design and Implementation.

Digital Library

[12]

J. Ferrante, K. J. Ottenstein, and J. D. Warren. The program dependence graph and its use in optimization. A CM Transactions on Programming Languages and Systems, 9(3):319-349, July 1987.

Digital Library

[13]

P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer-Verlag, January 1996.

Digital Library

[14]

P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of the 2gth A CM Symposium on Principles of Programming Languages, pages 174-186, Paris, January 1997.

Digital Library

[15]

C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

Digital Library

[16]

G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.

Digital Library

[17]

S. Horwitz and T. Reps. The use of program dependence graphs in software engineering. In Proceedings of the lgth International Conference on Software Engineering, pages 392-411, May 1992.

Digital Library

[18]

S. Horwitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs, in David S. Wise, editor, Proceedings of the A GM '88 Conference on Programming Language Design and Implementation, pages 35-46, Atlanta, GE, USA, June 1988. ACM Press.

Digital Library

[19]

D. J. Kuck, R. H. Kuhn, B. Leasure, D. A. Padua, and M. Wolfe. Dependence graphs and compiler optimizations. In Proceedings of the 8th A GM Symposium on Principles of Programming Languages, pages 207- 218, January 1981.

Digital Library

[20]

L.T. Kou. On live-dead analysis for global data flow problems. Journal of the A CM, 23(3):473-483, July 1977.

Digital Library

[21]

W. Landi. Interprocedural aliasing in the presence of pointers. PhD thesis, Rutgers University, 1991.

Digital Library

[22]

D.L. Long and L. A. Clarke. Data flow analysis of concurrent systems that use the rendezvous model of synchronization. In Proceedings of A CM Symposium on Testing, Analysis, and verification (TAVg), pages 21-35, Vancouver, October 1991.

Digital Library

[23]

K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

Digital Library

[24]

R. Milner. Communication and Concurrency. Prentice Hall, 1989.

Digital Library

[25]

T.J. Marlowe and B. G. Ryder. Properties of data flow frameworks. Acts informatica, 28:121-163, 1990.

Digital Library

[26]

S.P. Masticola and B. G. Ryder. Non-concurrency analysis. In Proceedings of Fourth A CM SIGPLAN Symposium on Principles E4 Practice of Parallel programming, pages 129-138, San Diego, May 1993.

Digital Library

[27]

K.E. Martersteck and A.E. Spencer. Introduction to the 5ESS(TM) switching system. ATST Technical Journal, 64(6 part 2):1305-1314, July-August 1985.

[28]

J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. in Proe. 5th Int'l Syrup. on Programming, volume 137 of Lecture Notes in Computer Science, pages 337-351. Springer- Verlag, 1981.

Digital Library

[29]

E. Ruf. Context-insensitive alias analysis reconsidered. In Proceedings of Conference on Programming Language Design and Implementation, New York, NY, USA, June 1995. ACM Press.

Digital Library

[30]

M. Sagiv, T. Reps, and R. Wilhelm. Solving shapeanalysis problems in languages with destructive updating, in Proceedings of the ~3rd A CM Symposium on Principles of Programming Languages, pages 16-31, St. Petersburg, Florida, January 1996. ACM Press.

Digital Library

[31]

R.N. Taylor. A general-purpose algorithm for analyzing concurrent programs. Communications of the A CM, pages 362-376, May 1983.

Digital Library

[32]

F. Tip. Generic techniques for source-level debugging and dynamic program slicing. In Proceedings of TAP- SOFT'95, volume 915 of Lecture Notes in Computer Science. Springer-Verlag, 1995.

Digital Library

[33]

A. Venet. Abstract interpretation of the,r-calculus. In Mads Dam, editor, Analysis and Verification of Multiple-Agent Languages (Proceedings of the Fifth LOMAPS Workshop), volume 1192 of Lecture Notes in Computer Science, pages 51-75. Springer-Verlag, 1997.

Digital Library

[34]

M. Weiser. Program slicing. In Proceedings of the 5th International Conference on Software Engineering, March 1981.

Digital Library

Cited By

Bagherzadeh MKahani NJahed KDingel J(2022)Execution of Partial State Machine ModelsIEEE Transactions on Software Engineering10.1109/TSE.2020.300885048:3(951-972)Online publication date: 1-Mar-2022
https://doi.org/10.1109/TSE.2020.3008850
Carver RLei Y(2018)Stateless techniques for generating global and local test oracles for message-passing concurrent programsJournal of Systems and Software10.1016/j.jss.2017.11.026136:C(237-265)Online publication date: 1-Feb-2018
https://dl.acm.org/doi/10.1016/j.jss.2017.11.026
Godefroid PJalote PBriand LHoek A(2014)Micro executionProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568273(539-549)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568273
Show More Cited By

Index Terms

Automatically closing open reactive programs
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Automatically closing open reactive programs

We study in this paper the problem of analyzing implementations of open systems --- systems in which only some of the components are present. We present an algorithm for automatically closing an open concurrent reactive system with its most general ...
Investigating open data portals automatically: a methodology and some illustrations
dg.o '18: Proceedings of the 19th Annual International Conference on Digital Government Research: Governance in the Data Age

Deploying a suitable open data platform is one of the most important requirements for succeeding in the provision of open data. Currently, there are several platforms available in the market ranging from the commercial ecosystem to free and open source ...
Open source software licenses: Strong-copyleft, non-copyleft, or somewhere in between?

Studies on open source software (OSS) have shown that the license under which an OSS is released has an impact on the success or failure of the software. In this paper, we model the relationship between an OSS developer's utility, the effort that goes ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '98: Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation

May 1998

357 pages

ISBN:0897919874

DOI:10.1145/277650

Chairmen:
Jack W. Davidson
Univ. of Virginia
,
Keith D. Cooper
Rice Univ. Houston, TX
,
Editor:
A. Michael Berman
Rowan Univ. Glassboro, NJ

ACM SIGPLAN Notices Volume 33, Issue 5
May 1998
358 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/277652
Chairmen:
Jack W. Davidson
Univ. of Virginia
,
Keith D. Cooper
Rice Univ., Houston, TX
,
Editor:
A. Michael Berman
Rowan Univ., Glassboro, NJ
Issue’s Table of Contents

Copyright © 1998 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]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

PLDI98

Sponsor:

SIGPLAN

PLDI98: Conference on Programming Language

June 17 - 19, 1998

Quebec, Montreal, Canada

Acceptance Rates

PLDI '98 Paper Acceptance Rate 31 of 136 submissions, 23%;

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

51
Total Citations
View Citations
510
Total Downloads

Downloads (Last 12 months)105
Downloads (Last 6 weeks)14

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bagherzadeh MKahani NJahed KDingel J(2022)Execution of Partial State Machine ModelsIEEE Transactions on Software Engineering10.1109/TSE.2020.300885048:3(951-972)Online publication date: 1-Mar-2022
https://doi.org/10.1109/TSE.2020.3008850
Carver RLei Y(2018)Stateless techniques for generating global and local test oracles for message-passing concurrent programsJournal of Systems and Software10.1016/j.jss.2017.11.026136:C(237-265)Online publication date: 1-Feb-2018
https://dl.acm.org/doi/10.1016/j.jss.2017.11.026
Godefroid PJalote PBriand LHoek A(2014)Micro executionProceedings of the 36th International Conference on Software Engineering10.1145/2568225.2568273(539-549)Online publication date: 31-May-2014
https://dl.acm.org/doi/10.1145/2568225.2568273
Betin-Can AHalle SBultan T(2013)Modular Verification of Asynchronous Service Interactions Using Behavioral InterfacesIEEE Transactions on Services Computing10.1109/TSC.2011.556:2(262-275)Online publication date: 1-Apr-2013
https://dl.acm.org/doi/10.1109/TSC.2011.55
Tkachuk ODwyer M(2010)Environment generation for validating event-driven software using model checkingIET Software10.1049/iet-sen.2009.00174:3(194)Online publication date: 2010
https://doi.org/10.1049/iet-sen.2009.0017
Carver RLei Y(2010)Distributed reachability testing of concurrent programsConcurrency and Computation: Practice and Experience10.1002/cpe.157322:18(2445-2466)Online publication date: 12-Nov-2010
https://doi.org/10.1002/cpe.1573
Ghica DBakewell A(2009)ClippingProceedings of the 2009 24th Annual IEEE Symposium on Logic In Computer Science10.1109/LICS.2009.25(189-198)Online publication date: 11-Aug-2009
https://dl.acm.org/doi/10.1109/LICS.2009.25
Kong STillmann NHalleux J(2009)Automated Testing of Environment-Dependent Programs - A Case Study of Modeling the File System for PexProceedings of the 2009 Sixth International Conference on Information Technology: New Generations10.1109/ITNG.2009.80(758-762)Online publication date: 27-Apr-2009
https://dl.acm.org/doi/10.1109/ITNG.2009.80
Barlas EBultan TStirewalt KEgyed AFischer B(2007)NetstubProceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering10.1145/1321631.1321638(24-33)Online publication date: 5-Nov-2007
https://dl.acm.org/doi/10.1145/1321631.1321638
Hughes GBultan TRosenblum DElbaum S(2007)Interface grammars for modular software model checkingProceedings of the 2007 international symposium on Software testing and analysis10.1145/1273463.1273471(39-49)Online publication date: 9-Jul-2007
https://dl.acm.org/doi/10.1145/1273463.1273471
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents