View from the Fringe of the Fringe
Formal analysis remains outside the mainstream of system design practice. Interactive methods and tools are regarded by some to be on the margin of useful research in this area. Although it may seem relatively academic to some, it is vital that this the so-called “theorem proving approach” continue to be as vigorously explored as approaches favoring highly automated reasoning. Design derivation, a term for design formalisms based on transformations and equivalence, represents just a small twig on the theorem-proving branch of formal system analysis. A perspective on current trends is presented from this remote outpost, including a review of the author’s work since the early 1980s.
KeywordsModel Checker Formal Method Theorem Prove Recursive Equation Proof Assistant
- 5.A. J. C. Hurkens, Monica McArthur, Yiannis M. Moschovakis, Lawrence S. Moss, and Glen T. Whitney. The logic of recursive equations. The Journal of Symbolic Logic, 63(2):451–478, June 1998.Google Scholar
- 6.Steven D. Johnson. The Indiana University System Design Methods Laboratory home page. http://www.cs.indiana.edu/hmg/hmg.html.
- 7.Steven D. Johnson. Manipulating logical organization with system factorizations. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, pages 260–281. LNCS 408, 1989.Google Scholar
- 8.Steven D. Johnson. A workshop on formal methods education: an aggregation of opinions. International Journal on Software Tools for Technology Transfer, 2(3):203–207, November 1999.Google Scholar
- 9.Steven D. Johnson and Paul S. Miner. Integrated reasoning support in system design: design derivation and theorem proving. In Hon F. Li and David K. Probst, editors, Advances in Hardware Design and Verification (CHARME’97), pages 255–272. Chapman-Hall, 1997.Google Scholar
- 10.Lawrence S. Moss. Recursion and corecursion have the same equational logic. Theoretical Computer Science, to appear in 2002. http://math.indiana.edu/home/moss/home.html.
- 11.Amir Pnueli. These quotations are extracted from transparencies for invited talks at PODC’90, FM’99, and CAV’00. They can be found at http://www.wisdom.weizmann.ac.il/amir/invited-talks.html.