Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs

[en] VeriSoft is a tool for systematically exploring the state spaces of systems composed of several concurrent processes executing arbitrary C (or C++) code. VeriSoft can automatically detect coordination problems between the concurrent processes of a system. In this paper, we present a method to synthesize a finite-state machine that simulates all the sequences of visible operations of a given process that were observed during a state-space exploration performed by VeriSoft. The examination of this machine makes it possible to discover the dynamic behavior of the process in its environment and to understand how it contributes to the global behavior of the system.

Disciplines :

Computer science

Author, co-author :

Boigelot, Bernard ; Université de Liège - ULiège > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique

Godefroid, Patrice

Language :

English

Title :

Automatic Synthesis of Specifications from the Dynamic Observation of Reactive Programs

Publication date :

1997

Event name :

Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop (TACAS '97)

Event place :

Enschede, Netherlands

Audience :

International

Journal title :

Lecture Notes in Computer Science

ISSN :

0302-9743

eISSN :

1611-3349

Publisher :

Springer, Berlin, Germany

Volume :

1217

Pages :

321-333

Peer reviewed :

Peer reviewed

Funders :

F.R.S.-FNRS - Fonds de la Recherche Scientifique
Bell Laboratories

Available on ORBi :

since 03 November 2010

Statistics

Number of views

49 (4 by ULiège)

Number of downloads

131 (1 by ULiège)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

publications

supporting

mentioning

contrasting

Smart Citations

Citing PublicationsSupportingMentioningContrasting

View Citations

See how this article has been cited at scite.ai

scite shows how a scientific paper has been cited by providing the context of the citation, a classification describing whether it supports, mentions, or contrasts the cited claim, and a label indicating in which section the citation was made.

Bibliography

A. W. Biermann and J. A. Feldman. On the synthesis of finite state machines from samples of their behavior. IEEE Transactions on Computers, 21(6):592-597, June 1972.
B. Boigelot and P. Godefroid. Model checking in practice: An analysis of the ACCESS. bus protocol using SPIN. In Proceedings of Formal Methods Europe’96, volume 1051 of Lecture Notes in Computer Science, pages 465-478, Oxford, March 1996. Springer-Verlag.
E. H. Chikofsky and J. H. Cross. Reverse engineering and design recovery: A taxonomy. IEEE Software, 7(1):13-17, January 1990.
E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ cache coherence protocol. In Proceedings of the Eleventh International Symposium on Computer Hardware Description Languages and Their Apllications. North-Holland, 1993.
J.-D. Choi, B. P. Miller, and R. H. B. Netzer. Techniques for debugging parallel programs with flowback analysis. ACM Transactions on Programming Languages and Systems, pages 491-530, October 1991.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM Transactions on Programming Languages and Systems, 1(15):36-72, 1993.
J. E. Cook and A. L. Wolf. Automatic Process Discovery through Event-Data Analysis. In Proceedings of the 17th Conference on Software Engineering, Seatle, April 1995.
D. L. Dill, A. J. Drexler, A. J. Hu, and C. H. Yang. Protocol verification as a hardware design aid. In 1992 IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522-525, Cambridge, MA, October 1992. IEEE Computer Society.
S. Das and M. C. Mozer. A Unified Gradient-Descent/Clustering Architecture for Finite-State Machine Induction. Advances in Neural Information Processing Systems, 6:19-26, 1994.
J. C. Fernandez, H. Garavel, L. Mounier, A. Rasse, C. Rodriguez, and J. Sifakis. A toolbox for the verification of LOTOS programs. In Proc. of the Ufth International Conference on Software Engineering ICSE’14, Melbourne, Australia, May 1992. ACM.
R. Flora-Holmquist and M. Staskauskas. Formal validation of virtual finite state machines. In Proc. Workshop on Industrial-Strength Formal Specification Techniques (WIFT’95), pages 122-129, Boca Raton, April 1995.
P. Godefroid. Model Checking for Programming Languages using VeriSoft. In Proceedings of the 2Jfth ACM Symposium on Principles of Programming Languages, pages 174-186, Paris, January 1997.
Z. Har’El and R. P. Kurshan. Software for analytical development of communication protocols. AT&T Technical Journal, 1990.
J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
L. Miclet and J. Quinqueton. Learning from Examples in Sequences and Grammatical Inference. In Syntactic and Structural Pattern Recognition, volume 45 of NATO ASI Series F - Computer and Systems Science, pages 153-171. Springer-Verlag, 1988.
R. H. B. Netzer and B. P. Miller. Optimal Tracing and Replay for Debugging Message-Passing Parallel Programs. In Proceedings of Supercomputing’92, pages 502-511, Minneapolis, 1992.
Rudin. Protocol development success stories: Part I. In Proc. 12th IFIP WG 6.1 International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida, June 1992. North-Holland.
R. S. Side and G. C. Shoja. A debugger for distributed programs. Software Practice and Experience, 24(5):507-525, May 1994.
L. Wills, Ph. Newcomb, and E. Chikofsky, editors. Proceedings of the Second Working Conference on Reverse Engineering, Toronto, July 1995. IEEE.