Abstract
VeriSoft [God97] 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.
“Aspirant” (Research Assistant) for the National Fund for Scientific Research (Belgium). The work of this author was done while visiting Bell Laboratories.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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 14th International Conference on Software Engineering ICSE'14, Melbourne, Australia, May 1992. ACM.
A. 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 24th 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.
G. 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.
H. 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.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boigelot, B., Godefroid, P. (1997). Automatic synthesis of specifications from the dynamic observation of reactive programs. In: Brinksma, E. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1997. Lecture Notes in Computer Science, vol 1217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035397
Download citation
DOI: https://doi.org/10.1007/BFb0035397
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62790-6
Online ISBN: 978-3-540-68519-7
eBook Packages: Springer Book Archive