Steven D. Johnson


Work: Home:
Computer Science Department 615 N. Plymouth Rd.
215 Lindley Hall Bloomington, IN 47408
Indiana University  
Bloomington, IN 47405-4101  
     
NET: sjohnson@cs.indiana.edu jrdeam@cs.indiana.edu
TEL: 812-855-2567 812-332-6960
FAX: 812-855-4829  
WWW: www.cs.indiana.edu/~sjohnson

Biographical Sketch

Steven D. Johnson is a professor of computer science in the Indiana University College of Arts and Sciences. He received a B.A.  in mathematics and Russian from Depauw University in 1970, an M.A. in mathematics from Indiana University in 1977, and the Ph.D. in computer science from Indiana University in 1983. His Ph.D. dissertation, Synthesis of Digital Designs from Recursion Equations, was an ACM Distinguished Dissertation in 1984. His research since 1983 has been in the area of formal methods applied to systems. He is a member of the Association for Computing Machinery (ACM), the Institute of Electrical and Electronics Engineers (IEEE) Computer Society, the International Federation for Information Processing (IFIP) Working Group 10.5 on Electronic System Engineering, and the SIG-CHARME special interest group on formal methods (which he currently chairs). Johnson is on the editorial board of Formal Methods for System Design; and he has served on the program committees of the IEEE International Conference on Computer Design (ICCD), the IFIP Conferences on Computer Hardware Description Languages and their Applications (CHDL) and Correct Hardware Methods (CHARME), The International Conference on Formal Methods in Computer Aided Design (FMCAD), and numerous other forums in the area of formal methods for systems. He was Program Chair of CHDL'95 and Conference Cochair of FMCAD 2000. Dr. Johnson was born October 11, 1948. He is married to Jennifer R. Deam and has a son, Matthew, and a daughter, Verity.

Education

Ph.D 1983 Indiana University (Computer Science)
M.S. 1976 Indiana University (Computer Science)
M.A. 1972 Indiana University (Mathematics)
B.A. 1970 DePauw University (Mathematics and Russian)

Experience

2001-now Professor of Computer Science, Indiana University
 2003 (3 wks.) Visiting Scientist, National Aeronautics Institute, Hampton VA.
1990-2001 Associate Professor of Computer Science, Indiana University
1996-1997 Visiting Scholar, ECE/CS Department, University of Cincinnati
1993-1995 Chairman of Computer Science Department, Indiana University
1984-1990 Assistant Professor of Computer Science, Indiana University
1983-1984 Visiting Assistant Professor of Computer Science, Indiana University
1982-1983 Visiting Lecturer, Department of Computer Science, Indiana University
1977-1979 Member of Technical Staff, Bell Telephone Laboratories, Holmdel, NJ

Refereed and invited publications

[42]
Steven D. Johnson. Formal methods in embedded design. Computer, 36:104-106, November 2003.

[41]
Danko D. Antolovic, Bryce Himebaugh, and Steven D. Johnson. Skeyeball: Real-time vision system for an autonomous model airplane. In Proceedings of the 22nd Digital Avionics Systems Conference (DASC'03), October 2003. Indianapolis, Indiana. (PDF)

[40]
Danko Antolovic, Bryce Himebaugh, and Steven D. Johnson. The Skeyeball tracking project. 16th Florida Conference on Recent Advances in Robotics (FCRAR'2003), small tt http://www.eng.fau.edu/conf/fcrar2003/i, May 2003. 8-9 May 2003, Florida Atlantic University Seatech campus, Dania Beach, Florida. (PDF)

[39]
Steven D. Johnson. View from the fringe of the fringe. In Tiziana Margaria and Thomas Melham, editors, 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001, Livingston, Scotland, Proceedings, volume 2144 of Lecture Notes in Computer Science, pages 1-12. Springer-Verlag, 2001. Invited paper. (PDF)

[38]
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, 4, 2003. (PDF)

[37]
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. (PDF)

[36]
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. Proceedings of the 5th NASA Langley Formal Methods Workshop, Williamsburg, Virginia, 13-15 June, 2000, http://shemesh.larc.nasa.gov/fm/Lfm2000/. (PDF)

[35]
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. 10th IFIP WG 10.5 Advanced Research Working Conference, CHARME '99, Bad Herrenalb, Germany, September 1999, Proceedings. (PDF)

[34]
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.

[33]
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. Report of the meeting held March 1998 at Melbourne, Florida.

[32]
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. IFIP TC10 WG 10.5 International Conference on Correct Hardware and Verification Methods, 16-18 October 1997, Montreal, Canada.

[31]
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, Proceedings of the 4th NASA Langley Formal Methods Workshop, Hampton, Virginia 10-12 September, 1997, http://archive.larc.nasa.gov/shemesh/Lfm97/.

[30]
Paul S. Miner and Steven D. Johnson. Verification of an optimized fault-tolerant clock synchronization circuit. In Mary Sheeran and Satnam Singh, editors, Designing Correct Circuits, Electronic Workshops in Computing, http://www.ewic.org.uk/ewic/workshop/view.cfm/DCC-96. Springer, September 1996. (PDF)

[29]
Steven D. Johnson, Gerard Allwein, and K. Jon Barwise. Toward the rigorous use of diagrams in reasoning about hardware. In Gerard Allwein and Jon Barwise, editors, Logical Reasoning with Diagrams. Oxford University Press, 1996.

[28]
Kathryn Fisler and Steven D. Johnson. Integrating design and verification envrionments through a logic supprting hardware diagrams. In Procedings of the 1995 IFIP International Conference on Computer Hardware Description Languages and Their Applications, pages 669-674. IEEE Cat. No. 95TH8102, September 1995.

[27]
M. Esen Tuna, Kamlesh Rath, and Steven D. Johnson. Specification and synthesis of bounded indirection. In Proceedings of the Fifth Great Lakes Symposium on VLSI (GLSVLS I'95), pages 86-89. IEEE, March 1995.

[26]
Steven D. Johnson, Paul S. Miner, and Albert Camilleri. Studies of the single pulser in various reasoning systems. In Ramayya Kumar and Thomas Kropf, editors, Theorem Provers in Circuit Design, Theory Practice and Experience (TPCD'94), volume 901 of Lecture Notes in Computer Science, pages 209-227. Springer, 1995. Second International Conference, TPCD '94, Bad Herrenalb, Germany, September 26-28, 1994, Proceedings. (PDF)

[25]
Paul S. Miner, Shyamsundar Pullela, and Steven D. Johnson. Interaction of formal design systems in the development of a fault-tolerant clock synchronization circuit. In  13th Symposium on Reliable Distributed Systems (RDS'94), pages 128-137, 1994. (PDF)

[24]
M. Esen Tuna, Steven D. Johnson, and Bob Burger. Continuations in hardware-software codesign. In Proceedings of the 1994 IEEE International Conference on Computer Design (ICCD'94), pages 264-269. IEEE Cat. No. 94CH35712, October 1994.

[23]
Zheng Zhu and Steven D. Johnson. Capturing synchronization specifications for sequential compositions. In Proceedings of the 1994 IEEE International Conference on Computer Design (ICCD'94), pages 117-121. IEEE Cat. No. 94CH35712, October 1994.

[22]
Kamlesh Rath, Venkatesh Choppella, and Steven D. Johnson. Decomposition of sequential behavior using interface specification and complementation. VLSI Design, 3(3-4):347-358, 1995.

[21]
Kamlesh Rath, M. Esen Tuna, and Steven D. Johnson. Behavior tables: A basis for system representation and transformational system synthesis. In Proceedings of the IEEE/ACM International Conference on Computer Aided Design (ICCAD'93), pages 736-740. IEEE Cat. No. 93CH3344-9, November 1993.

[20]
Kamlesh Rath, Bhaskar Bose, and Steven D. Johnson. Derivation of a DRAM memory interface by sequential decomposition. In Proceedings of the International Conference on Computer Design (ICCD'93), pages 438-441. IEEE Cat. No. 93CH3335-7, October 1993.

[19]
Bhaskar Bose, M. Esen Tuna, and Steven D. Johnson. System factorization in codesign: A case study of the use of formal techniques to achieve hardware-software decomposition. In Proceedings of the International Conference on Computer Design (ICCD'93), pages 458-461. IEEE Cat. No. 93CH3335-7, October 1993.

[18]
Bhaskar Bose, Steven D. Johnson, and Shyam Pullela. Integrating boolean verification with formal derivation. In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications (CHDL'93), volume A-32 of IFIP Transactions, pages 127-134. North-Holland, 1993. Proceedings of the 11th IFIP WG 10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL'93, sponsored by IFIP WG 10.2 and incooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26-28 April, 1993.

[17]
Bhaskar Bose and Steven D. Johnson. DDD-FM9001: Derivation of a verified microprocessor. an exercise in integrating verification with formal derivation. In G. Milne and L. Pierre, editors, Correct Hardware Design and Verification Methods (CHARME'93), volume 683 of Lecture Notes in Computer Science, pages 191-202. Springer, 1993. IFIP WG 10.2 Advanced Research Working Conference, CHARME'93, Arles, France, May 24-26, 1993, Proceedings.

[16]
Zheng Zhu and Steven D. Johnson. Automatic synthesis of sequential synchronizations. In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications (CHDL'93), volume A-32 of IFIP Transactions, pages 285-301. North-Holland, 1993. Proceedings of the 11th IFIP WG 10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL'93, sponsored by IFIP WG 10.2 and incooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26-28 April, 1993.

[15]
Kamlesh Rath and Steven D. Johnson. Toward a basis for protocol specification and process decomposition. In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications (CHDL'93), volume A-32 of IFIP Transactions, pages 169-186. North-Holland, 1993. Proceedings of the 11th IFIP WG 10.2 International Conference on Computer Hardware Description Languages and their Applications - CHDL'93, sponsored by IFIP WG 10.2 and incooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 26-28 April, 1993.

[14]
Steven D. Johnson and Bhaskar Bose. A system for mechanized digital design derivation. In IFIP and ACM/SIGDA International Workshop on Formal Methods in VLSI Design, 1991. IFIP WG 10.2 conference series. Available as Indiana University Computer Science Department Technical Report No. 323 (rev. 1997).

[13]
Zheng Zhu and Steven D. Johnson. An example of interactive hardware transformation. In P. A. Subramanyam, editor, IFIP and ACM/SIGDA International Workshop on Formal Methods in VLSI Design, January 1991. IFIP WG 10.2 conference series.

[12]
Zheng Zhu and Steven D. Johnson. An algebraic framework for data abstraction in hardware description. In Garaint Jones and Mary Sheeran, editors, Designing Correct Circuits (DCC'90), Workshops in Computing. Springer, 1990. Workshop jointly organised by the Universities of Oxford and Glasgow, 26-28 September 1990, Oxford.

[11]
John Franco, Daniel P. Friedman, and Steven D. Johnson. Multi-way streams in scheme. Computer Languages, 15(2):109-125, 1990.

[10]
Steven D. Johnson, R.M. Wehrmeister, and B. Bose. On the interplay of synthesis and verification: Experiments with the FM8501 processor description. In Claesen, editor, Formal VLSI Specification and Synthesis, VLSI Design Methods - I, pages 385-404. North-Holland, 1990. Proceedings of the IFIP WG 10.2/WG 10.5 International Worksho p on Applied Formal Methods for Correct VlSI Design, Sponsored by IMEC, Houtha len, Belgium, 13-16 November, 1989.

[9]
Zheng Zhu and Steven D. Johnson. An algebraic characterization of structural synthesis for hardware. In L.J.M. Claesen, editor, Formal VLSI Specification and Synthesis, VLSI Design Methods - I. North-Holland, 1990. Proceedings of the IFIP WG 10.2/WG 10.5 International Workshop on Applied Formal Methods for Correct VlSI Design, Sponsored by IMEC, Houthalen, Belgium, 13-16 November, 1989.

[8]
C.D. Boyer and Steven D. Johnson. Using the digital design derivation system: case study of a VLSI garbage collector. In Darringer and Ramming, editors, Ninth International Symposium on Computer Hardware Description Languages (CHDL'89), Amsterdam, 1989. IFIP WG 10.2, Elsevier.

[7]
Steven D. Johnson. Manipulating logical organization with system factorizations. In M. Leeser and G. Brown, editors, Hardware Specification, Verification and Synthesis: Mathematical Aspects, volume 408 of Lecture Notes in Computer Science, pages 260-281. Springer, July 1989. Mathematical Sciences Institute Workshop, Cornell University, Ithaca, New York, USA, July 1989, Proceedings. (PDF)

[6]
Steven D. Johnson and C.D. Boyer. Modelling transistors applicatively. In G.J. Milne, editor, The Fusion of Hardware Design and Verification, pages 397-420. North-Holland, 1988. Proceedings of the IFIP WG 10.2 Working Conference on The Fusion of Hardware Design and Vierification, Glasgow, Scotland, 4-6 July, 1988.

[5]
Steven D. Johnson, B. Bose, and C.D. Boyer. A tactical framework for digital design. In Birtwistle and Subramanyam, editors, VLSI Specification, Verification and Synthesis, pages 349-383. Kluwer, Boston, 1988.

[4]
Steven D. Johnson. Digital design in a functional calculus. In G. Milne and P.A. Subramanyam, editors, Formal Aspects of VLSI Design, pages 153-178. North-Holland, Amsterdam, 1986. Proceedings of tthe 1985 Edingurgh Workshop on VLSI, Edinburgh, Scotl and, U.K.

[3]
Steven D. Johnson. Applicative programming and digital design. In Proc. Eleventh Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming (POPL'84), pages 218-227, 1984.

[2]
Steven D. Johnson. Synthesis of Digital Designs from Recursion Equations. MIT Press, Cambridge, 1984.

[1]
Steven D. Johnson. Circuits and systems: Implementing communication with streams. IMACS Transactions on Scientific Computation, II:311-319, 1983.

Books and collections

[3]
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, Heidelberg Berlin, 2000. Springer-Verlag.

[2]
Steven D. Johnson, editor. Computer Hardware Description Languages and Their Applications (CHD L'95). IFIP WG 10.2/5, IEEE Cat. No. 95TH8102, August 1995. Proceedings of the IFIP International Conference held in conjunction with ASP-DAC'95 and VLSI'95, August 29-Sept 1, Makuhari Messe, Chiba, Japan.

[1]
Steven D. Johnson. Synthesis of Digital Designs from Recursion Equations. MIT Press, Cambridge, 1984.

Other publications and reports

[20]
Steven D. Johnson. Photograph, Contexts 2(2):70.

[19]
Steven D. Johnson and Eric Jeschke. Modeling with streams in daisy/the schemengine project. In M. Sheeran and T. Melham, editors, Designing Correct Circuits, (DCC'02). ETAPS 2002, 2002. Presentation at the Workshop on Designing Correct Circuits, held on 6-7 April 2002 in Grenoble, France. (PDF)

[18]
Steven D. Johnson. Formal derivation of a scheme computer. Technical Report 544, Indiana University Computer Science Dept., Bloomington, Indiana, September 2000. http://www.cs.indiana.edu/ftp/techreports/.

[17]
Caleb Hess, Steven D. Johnson, Robert W. Wehrmeister, and Ingo Cyliax. Logic engine user manual. Electronically published for various Indiana University Computer Science Department courses. Revised yearly.

[16]
Steven D. Johnson, Caleb Hess, Bryce Himebaugh, Franklin Prosser, David Winkel, and David Wilson. B441/541 laboratory experiments. Electronically published for Indiana University Computer Science Department courses. Revised yearly.

[15]
Steven D. Johnson. Franklin Prosser. In In Honor of Retiring Faculty: April 14, 1999. Indiana University, 1999.

[14]
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.

[13]
Steven D. Johnson, Gary B. Parker, Ingo Cyliax, and David Braun. Using cyclic genetic algorithms to reconfigure hardware controlers for robots. Technical Report 494, Indiana University Computer Science Department, Bloomington, Indiana, US, December 1993.

[12]
Kamlesh Rath, M. Esen Tuna, and Steven D. Johnson. An introduction to behavior tables. Technical Report 392, Indiana University Computer Science Department, Bloomington, Indiana, US, December 1993.

[11]
Steven D. Johnson et. al. Computer science department handbook. Indiana University Computer Science Department. 1993-1994 edition revised with Leslie Ortquist and Dedaimia Whitney; 1992-1993 edition revised with Dedaimia Whitney; 1991-1992 edition cowritten with Pam Larson, Pam Milam and Dedaimia Whitney.

[10]
Kamlesh Rath, Ignacio Celis, R. M. Wehrmeister, and Steven D. Johnson. RTBA: A generic bit-sliced bus architecture for data path synthesis. Technical Report 321, Indiana University Computer Science Department, Bloomington, Indiana, US, December 1990.

[9]
Steven D. Johnson and Bhaskar Bose. A system for digital design derivation. Technical Report 289, Indiana University Computer Science Department, Bloomington, Indiana, US, August 1989.

[8]
Steven D. Johnson. Daisy, DSI and LiMP: Issues in architecture for suspending construction. Technical Report 288, Indiana University Computer Science Department, Bloomington, Indiana, US, August 1989.

[7]
Steven D. Johnson. How Daisy is lazy: Suspending construction at target levels. Technical Report 286, Indiana University Computer Science Department, Bloomington, Indiana, US, August 1989.

[6]
Steven D. Johnson. Daisy programming manual. http://www.cs.indiana.edu/hyplan/sjohnson/dsi/.

[5]
Steven D. Johnson. Storage allocation for list multiprocessing. Technical Report 168, Indiana University Computer Science Department, Bloomington, Indiana, US, March 1985.

[4]
Steven D. Johnson. Synthesis of digital designs from recursion equations. Technical Report 141, Indiana University Computer Science Department, Bloomington, Indiana, US, May 1983. Revision published by MIT Press in 1984.

[3]
A. T. Kohlstaedt and Steven D. Johnson. DSI program description. Technical Report 120, Indiana University Computer Science Department, Bloomington, Indiana, US, November 1981.

[2]
Steven D. Johnson. Connection networks for output-driven list multiprocessing. Technical Report 114, Indiana University Computer Science Department, Bloomington, Indiana, US, 1981.

[1]
Steven D. Johnson. An interpretive model for a language based on suspended construction. Technical report, Indiana University Computer Science Department, Bloomington, Indiana, US, 1977. MS thesis.

Systems

1.
The Digital Design Derivation System. A transformation system for deriving hardware system descriptions from functional expressions. Implemented in Scheme, Emacs, and Tcl/TK.

2.
The Daisy/DSI Programming System. A concurrent functional list-processing language. Implemented in C under Unix/Linux.

3.
Research prototypes and case studies. Artifacts b-f were implemented using the Digital Design Derivation system to demonstrate formal methods research.

g.
Skeyeball airborne vision system (2002) http://www.cs.indiana.edu/hmg/skeyeball/.

f.
Schemachine computer (1994), CPU, hardware garbage collector, and custom memory architecture, realized in FPGAs and PLDs; functioned as a stand-alone computer, and tested against its own executable specification.

e.
FM9001 microprocessor (1993), realized in Actel FPGAs; tested against the LSI gate-array version developed by Warren Hunt.

d.
Hardware garbage collector (1989), realized in VLSI using PLAs; partially tested on a testbench.

e.
SECD computer (1988), realized in MSI and PLD, with CPU and hardware garbage collector; functioned as a stand-alone computer.

b.
Hardware garbage collector (1988), realized in MSI and PLD, and tested against a production implementation of Scheme.

a.
Parallel DSI/Daisy (1987), implemented in C on a 32-node BBN Butterfly multiprocessor, including a parallelized heap allocator, garbage collector, and Daisy language implementation. The purpose of the system was performance measurement of a truly parallel computational model.

4.
Instructional laboratories and platforms.

d.
Visual tracking laboratory for a course entitled Real-Time and Embedded Systems, based on an XESS XSV Virtex 800 development board and a PC operating under RTLinux.

c.
Servobot hexapod controller (1997) realized in reconfigurable FPGAs. A robotics exhibit introducing K-12 students to robotics and control.

b.
TrCAS instructional lab (2000), hardware infrastructure for a symmetric collision avoidance system, mounted on HO-guage model railroad engines; realized with PIC microprocessor, Xilinx FPGA, and infra-red range-finding sensor.

a.
The Logic Engine. Originally developed by Franklin P. Prosser and David E. Winkel, I am doing a fourth-generation redesign. An environment for hardware prototyping, including a project board providing power, clocking, microprogram sequencing, and I/O for hardware development; and connectivity to a software environment for design development and testing. Instructional version includes a series of laboratories for a full-year course on digital design. Also used in research. http://www.cs.indiana.edu/hmg/le/LEv4/

Invited talks and competitive presentations

Colloquia

Other meetings attended

Public Presentations

Grants

18.
Xilinx Corporation Educational Program donation, 2002. Components valued at $225,000.

17.
A design tool based on behavior tables (a NASA/GSRP fellowship), NASA NGT-1-01009, 2002-2004. Faculty supervisor. $66,000.

16.
Daisy/Patmos Connection Machine Pilot Project Patmos International Corporation, Principal Investigator, $37,000.

15.
Hardware System Design with Behavior Tables. NSF MIP96-10358, 1997-2000, Principal Investigator. $282,000.

13.
Assistantship for a Pilot Project in Electronic Application to Graduate School. Indiana University Office of Research and the University Graduate School, 1993-1995. Project Director. $22,000.

12.
Graduate Research Traineeship Initiative in Robotics and Intelligent Control. NSF GER93-54898, 1993-1998. Project Director with co-director Jonathan W. Mills. $557,500 plus $41,250 cost sharing.

11.
An Infrastructure for Conceptualization and Visualization of Computation (PI: David S. Wise). NSF CDA 93-03189, 1993-1998. Faculty participant, (PI: D. S. Wise) departmental CISE research infrastructure project, $1.7 million.

10.
Decomposing digital-system specifications into interacting sequential processes. NSF MIP92-08745, 1992-1995. Principal Investigator. $142,000.

9.
The Derivation of a Verified Microprocessor FM8502 (a NASA fellowship), NASA NGT-50861, 1991-1994. Faculty supervisor $66,000.

8.
SIGDA library grant, 1990. $1,000.

7.
Algebra for digital design derivation. NSF MIP89-21842, 1990-1992. Principal Investigator. $203,000.

6.
Digital design derivation. NSF MIP87-07067, 1987-1989. co-Principal Investigator with David E. Winkel. $206,000.

5.
A conduit from theory to practice. NSF DCR85-21497, 1985-1990, departmental CER project, 1985-1991, Participating faculty member (PI: E. R. Robertson), proposal coordinator and editor. $2,853,313 plus cost sharing.

4.
Methods and architectures for applicative programming. NSF DCR84-05241, 1984-1987, co-Principal Investigator with David S. Wise. Approximately $175,000.

3.
Applicative Programming for Indeterminate Systems. MCS82-03978, 1982-1984. Research Assistant (co-PIs Daniel P. Friedman and David S. Wise),

2.
Applicative Programming for Systems. MCS77-22325 1978-1982. Research Assistant (co-PIs Daniel P. Friedman and David S. Wise),

1.
Structured Recursion: Its Properties, Translation, and Implementation. MCS75-08145, 1975-1978. Research Assistant (co-PIs Daniel P. Friedman and David S. Wise),

Students directed

Seminars taught

Formal methods in System Design (1998);     Hardware derivation (1992, 1993);     Logic Synthesis, with Jonathan W. Mills (1991);     Laboratory in lisp: Experiments in functional multiprocessing, with David S. Wise and Eric Jeschke (1990);     Hardware derivation (1989);     Daisy, DSI and LiMP: Topics in functional multiprogramming (1988);     Applicative system description (1987);     Daisy and DSI (1985).

Courses taught

Computer Organization. Digital Design I-II. Discrete Structures for Computer Science Introduction to Verification. Logic and Program Verification. Mathematical Foundations of Computer Science. Microelectronic Computer-Aided Design. Operating Systems I-III. Real-Time and Embedded Systems. Theory of Operating Systems.

Professional activities, affiliations and honors

Research interests

Formal methods. Design derivation. Heterogeneous reasoning systems. Hardware synthesis and verification. Programming and hardware description languages. Real-time and embedded systems. Parallel symbolic processing.

Research statement

My main research area is formal methods for systems, and my approach stems from earlier studies in applicative programming languages and methods. Although it involves formalism, this research is applied in nature. I formalize design activities with the twofold purpose of gaining insight into conceptual aspects and implementing better software design tools. My methodology centers on algebraic manipulation of functional modeling expressions, which I have investigated in depth. I am particularly interested in exploring how this reasoning formalism interacts with other formalisms (e.g. predicate logic, temporal logic, etc.) and decision procedures (e.g. linear arithmetic, equivalence checking, etc.). The overriding goal is to create heterogeneous reasoning environments for software and hardware design.

A thesis of my work is that design involves orthogonal aspects whose synthesis must be reflected formalization through its syntax and reasoning rules. My metaphor for this thesis is a tetrahedron whose four facets are labeled by the principal aspects of system design: architecture, behavior, coordination (time), and data:

DDD tetrahedron

One can view any facet straight on, but a balanced view of any two or three facets distorts each of them, and seeing all at the same time is impossible. Neither is it possible to subsume all these aspects in one conceptual framework, nor, consequently, a single design notation. Software's traditional emphasis on behavior and data has lead to object oriented programming languages, while hardware description languages reflect an emphasis on behavior and architecture. I do not think it will prove fruitful to blend all four aspects into a monolithic notation. Instead, a foundation is needed which allows different aspects to be brought out at different times, as one might turn the tetrahedron to expose the faces.

I want my work to contribute to and be informed by practice, so I devote a substantial portion of my research effort to implementing the formalisms I study, integrating them with lower level tools, and gaining experience with them through case studies and tutorial demonstrations.

Teaching Philosophy

My two guiding principles as a computer science educator are juxtaposing abstraction with realization and emphasizing individual discovery. My own background is my motivation. I came into computer science from a background in mathematics and so could easily absorb much of the pedagogy about ``abstraction.'' But it was not until I was confronted with the physical basis of computation, to hardware and computer architecture, that I could begin to understand what was behind classroom concepts and programming constructs. I think it is vital for students to experience this connection individually. One cannot judge the quality of an abstraction without knowing what it abstracts from.

In my courses I strive to create an environment and circumstances in which my students can make discoveries and draw their own conclusions from direct experience. I develop laboratory components in which the participants are confronted with devices rather than models, and with the snowballing complexities of large design problems. My approach is dialectic: in the classroom, I present an orderly progression of topics and techniques, while knowing the laboratory experience requires a holistic approach from the outset.

In my lower level classes I address computing as a physical science, the phenomenon under study being the devices that compute and the systems in which they are embedded. Most students are very curious about these objects and I try to exploit that curiosity by creating opportunities to observe and measure, following up with models and methods. Of course, there is aways a reflective ``twist'' in the story (e.g. a compiler written in its own language, a microprocessor simulating itself, etc.) that motivates interesting theory.

rev. January 8, 2004

Steve Johnson
2004-01-08