on: September 12, 2001
to: Program Director, NSF/CISE/CCR/DA
fr: Steven D. Johnson
re: Final Report for grant MIP9610358, System Design with Behavior Tables

Project Status

This project is continuing. The primary objective of building a research tool for investigating interactive design using Behavior Tables has not yet been achieved.

I continue to wonder why my request for a second extension, which was filed in Fastlane on February 5, 2001, was never acted on by NSF. I have heard nothing, positive or negative, on this request. The residual funds would have applied directly to the development effort, bringing us much closer to a disseminable tool prototype.

The main thing hindering progress has been retaining graduate assistants. I have awarded support to 6 students in the course of this project. Four left school with masters degrees; and one transferred to the University of Edinburgh, where I expect a continuing, though less formal, collaboration in this research. For a considerable period, I had an open, unfilled assistantship.

There remains one student, Alex Tsow, who is writing a dissertation on this work. Tsow spent a year on leave for his wife’s PhD field study in Poland. Fortunately, he has been awarded a GSRP Fellowship from NASA that enables him to complete his doctoral work with a full commitment to software development.

In any case this is project was one in a series of projects that has already produced six PhDs, with a seventh pending now, and made significant contributions in formal methods for system design. It will continue to do so.

Published papers

An asterisk marks authors who used travel funding from this project to present conference papers. References [2, 3, 8] describe work directly resulting from this project. References [4, 5] describe collaborative research related to this project. References [6, 7] are reports related to education issues in formal methods which have a direct impact on this research area. Reference [1] is and invited talk that included a review of design derivation research since 1983, including the work of this project. Internet accessable copies of articles are available through:

                http://www.cs.indiana.edu/hmg/bib/iuhmg.html

1. Steven D. Johnson. A View from the Fringe of the Fringe. In T. Margaria and T. Melham (eds.) Correct Hardware Design and Verification Methods, 11th Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 2001, Proceedings, volume 2144 of Lecture Notes in Computer Science, pages 1-12. Springer-Verlag, 2001.

Invited presentation at the joint session of CHARME’01 and the 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’01) at Edinburgh, Scotland, UK.

2. Alex Tsow* and Steven D. Johnson*. Visualizing system factorizations with behavior tables. In Warren A. Hunt, Jr. and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design, Third International Conference, FMCAD 2000, Austin, TX, USA, November 1-3, 2000, Proceedings, volume 1954 of Lecture Notes in Computer Science, pages 523-541, Heidelberg Berlin, 2000. Springer-Verlag.

3. Steven D. Johnson* and Alex Tsow*. Algebra of behavior tables. In C. M. Holloway, editor, Lfm2000: Fifth NASA Langley Formal Methods Workshop, pages 23-34, 2000. NASA Conference Publication NASA/CP-2000-210100.

http://shemesh.larc.nasa.gov/fm/Lfm2000/

4. Steven D. Johnson, Yanhoung A. Liu, and Yuchen Zhang. A systematic incrementalization technique and its application to hardware design. International Journal on Software Tools for Technology Transfer, 2000. Invited for publication, in final review.

5. Steven D. Johnson*, Yanhong A. Liu, and Yuchen Zhang. A systematic incrementalization technique and its application to hardware design. In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods (CHARME’99), volume 1703 of Lecture Notes in Computer Science, pages 334-337, Berlin, 1999. Springer.

6. 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.

7. Steven D. Johnson, Warren P. Alexander, Shiu-Kai Chin, and Ganesh Gopalakrishnan. Report on the 21st century engineering consortium workshop.

http://www.cs.indiana.edu/formal-methods-education/xxiec/report.html, March 1999. Re-

port of the meeting held March 1998 at Melbourne, Florida.

8. Steven D. Johnson*. A tabular language for system design. In C. Michael Holloway and Kelly J. Hayhurst, editors, Lfm97: Fourth NASA Langley Formal Methods Workshop, September 1997. NASA Conference Publication 3356,

http://archive.larc.nasa.gov/shemesh/Lfm97/

System development

The DDD (Digital Design Derivation) research tool was commercialized by students from this research project, who started Derivations Systems, Inc. (www.derivation.com) in 1995. One of these students was an ABD doctoral student whose dissertation topic was behavior tables. After a couple of years it became clear that a collaborative relationship would not form with DSI, and that the ABD student would not continue his doctoral work in a commercial setting.

Hence it became necessary to revive the DDD tool, latent since 1994, and that a new student would inherit responsibility for the graphical front end. Thus, unanticipated development work and training became necessary, setting back new development objectives.

We shall continue the development effort, with one student funded by NASA, and, it is hoped, additional funding. Both Java and Tcl/TK table graphics have been explored and background connections between the GUI and the semantic editor have been developed. I expect a research demonstration tool to be finished in 2003, regardless of additional funding.

Travel

The following travel was funded in whole or in part by this grant.

1. Steven D. Johnson. 4th NASA/Langley Formal Methods Workshop (Lfm’97), Newport, VA, Sep. 9–14, 1997. Paper presentation.

2. Steven D. Johnson. 9th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’97), Montreal, Canada, Oct 16–19, 1997. Paper presentation.

3. Steven D. Johnson. 1998 NASA/Langley Formal Methods Group PVS course. Norfolk, VA, August 3–7, 1998. Attended a tutorial on the PVS theorem prover.

4. Steven D. Johnson. 1998 International Conference on Formal Methods in Computer Aided Design (FMCAD’98 and meeting of IFIP Working Group 10.5. San Jose, CA, August 3–7, 1998. Conference attendance, Working Group 10.5 participation.

5. Steven D. Johnson. International Federation for Information Processing Working Group 10.5 (IFIP/WG10.5) meeting and Design Automation Conference (DAC’99). New Orleans, LA, June 22–23, 1999. Conference attendance (1 day) and Working group participation.

6. Steven D. Johnson. World Congress on Formal Methods, Toulouse, France, September 20–24; and 10th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’99), Bad Herrenalb, Germany, September 26–29. Paper presentation at CHARME’99.

7. Steven D. Johnson and Alex Tsow. 5th NASA/Langley Formal Methods Workshop (Lfm2000), Williamsburg, VA, Jun. 12–16, 1997. Paper presentation.

8. Steven D. Johnson and Alex Tsow. 2000 International Conference on Formal Methods in Computer Aided Design (FMCAD 2000 and meeting of SIG-CHARME special interest group on formal methods for system design. Paper presentation, session chairing. Johnson was conference co-chair with Warren A. Hunt, Jr. with principal duties of Program Chair.

Other relevant items

1. Steven D. Johnson. Formal derivation of a scheme computer. Technical Report 544, Indiana University Computer Science Dept., Bloomington, Indiana, September 2000.

2. Ingo Cyliax, Steven D. Johnson, and Bhaskar Bose. Arriving at FPGA based hardware unix-encription using iterated codesign methods. Technical Report 496, Indiana University Computer Science Dept., Bloomington, Indiana, October 1997.

3. I was on the organization committee and was principal author of the report of the 21st Century Engineering Consortium Workshop, held at Melbourne Florida in March 1998. Hosted by AFOSR, this meeting was devoted to formal methods education, and remains the only meeting on that topic held in the United States, as far as I know.

4. In conjunction with the previous item, Kathryn Fisler and I established the Formal Methods Education Resources information hub hub for educators. Fisler is the maintainer of the web site at

http://www.cs.indiana.edu/formal-methods-education/

5. In September 2001, I was elected Chair of SIG-CHARME, an international interest group for applied formal methods. This organization traces its history to the early 1980s, organizing the first and longest conference series (now called FMCAD/CHARME) in this topic.