Experimental Computation Laboratory

Bruce McMillin - Director

Welcome!

The Experimental Computation Laboratory (ECL) is an organization in the

Computer Science Department at the University of Missouri - Rolla

dedicated to research in advanced methods of distributed and parallel computation.

Our main research interest is in Formal Methods for High Assurance Concurrent Software
Past Research areas have included
The current focus is on the use of rigorous mathematics through formal methods to create fault-tolerant and secure real-time distributed computing systems. Additional work is done in computational sciences. Interdisciplinary research is the cornerstone for the success of the ECL.

Graduate students and faculty are supported by several grants from the National Science Foundation which utilize the ECL

Our technical reports are available as abstracts and full-text (.ps format) from Computer Science Tech Reports.

Project Specifics

Formal Methods for High Assurance Concurrent Software

Sponsored by NSF

High Assurance Software is software under which the application will perform according to important properties of its specification under all reasonable circumstances. Important properties for concurrent programs include safety and liveliness properties, fault tolerance, and security. Software engineering provides one of the most important techniques, program verification, as a way of showing, formally, that a program satisfies these particular properties with respect to its specification. However, most verification methods do not, in of themselves, account for changes in the running system due to failures or reconfiguration.

Executable assertions, embedded into a distributed computing system, can provide this run-time assurance. However, generation of these assertions for distributed memory systems is not straightforward. This work proposes a system to transform a program's proof outline into an optimal set of distributed executable assertions that provide the necessary run-time assurance for distributed computing systems.

There is always a link back to our main research interests list.

Available Software:

CCSP:

CCSP (C-CSP) provides an execution environment for CSP programs. CCSP consists of two parts, a parser and a run-time system using Berkeley sockets. The parser takes a CSP program as input and produces a C program as output. These C programs are then run as individual processes on a network of UNIX workstations. CCSP's run-time system contains procedures for operationally evaluating globally-specified axiomatic assertions embedded in the CCSP programs.

Availability:

The actual software, code, examples and documentation, can be retrieved under the name CCSP.

Reference:

How to Program in CCSP {\it UMR Department of Computer Science Technical Report CSC-94-20} (B. McMillin, E. Arrowsmith)

CCSP - A Formal System for Distributed Program Debugging, {\it UMR Department of Computer Science Technical Report CSC-94-30} (B. McMillin, H. Lutfiyya, E. Arrowsmith and C. Serban)

Recent Publications:

History Clipping in Event-Driven Distributed Systems - by M. Chittajulu and Bruce McMillin (to appear in PDCS 2000 USING TEMPORAL SUBSUMPTION TO GENERATE EFFICIENT ERROR-DETECTING DISTRIBUTED ALGORITHMS, Journal of Systems and Software, May 2000 (M. Schollmeyer and B. McMillin)

Run-Time Security Evaluation ({RTSE}) for Distributed Applications, Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, May 1996 (C. Serban, B. McMillin). The code for the Boots System prototype can be retrieved from our gopher, under the name Boots and the manual for the Boots System is also available is postscript format.

Ensuring the Satisfaction of a Temporal Specification at Run-Time, Proceedings of the First IEEE International Conference on Engineering of Complex Computer Systems,} Ft. Lauderdale, FL, November 1995 (G. Tsai, M. Insall, B. McMillin) (also as UMR Department of Computer Science Technical Report Number CSC 93-20).

\XP``CCSP - A Formal System for Distributed Program Debugging,'' {\it Proceedings of the Software for Multiprocessors and Supercomputers, Theory, Practice, Experience,} Moscow, Russia, September 21-23, 1994 (B. McMillin, E. Arrowsmith) (also as UMR Department of Computer Science Technical Report Number CSC-94-13).

\XP``A General Method for Maximizing the Error-Detecting Ability of Distributed Algorithms,'' {\it Proceedings PARLE '94 Parallel Architectures and Languages Europe,} Athens, Greece,July 1994 (B. McMillin, M. Schollmeyer) (also as UMR Department of Computer Science Technical Report Number CSC 93-16).

\XP ``Fault-Tolerant Distributed Deadlock Detection/Resolution,'' {\it Proceedings of the 17th International COMPSAC}, November, 1993, pp. 224-230, (B. McMillin, P. Li). (Also as {\it UMR Department of Computer Science Technical Report Number CSC 92-04}).

\XP ``Formal Derivation of an Error-Detecting Distributed Data Scheduler Using CHANGELING,'' {\it Formal Methods in Programming and their Applications,} Springer-Verlag, Lecture Notes in Computer Science Series 735, July, 1993, pp. 363-376. (B. McMillin, H. Lutfiyya and A. Su). (Also as a Poster in the 15th ICSE, Baltimore, MD, May, 1993).

\XP``Teaching the Practice of Formal Methods in Distributed Computing Systems - A Module'' {\it Teaching Formal Methods: Curriculum Development Workshop,} Hamilton College, Clinton, N.Y., July 30 - Aug 5, 1994.

\XP``Efficient Run-Time Assurance in Distributed Systems Through Selection of Executable Assertions,'' {\it UMR Department of Computer Science Technical Report Number CSC 94-01} (B. McMillin, M. Schollmeyer)

\XP``Using Temporal Subsumption for Developing Efficient Error-Detecting Distributed Algorithms,'' {\it UMR Department of Computer Science Technical Report Number CSC 93-28} (B. McMillin, M. Schollmeyer)

\XP``Formal model and specification of deadlock,'' {\it UMR Department of Computer Science Technical Report CSC-93-31} (B. McMillin, P. Li).

\XP``Formal verification of distributed deadlock detection algorithm using a time-dependent proof technique,'' {\it UMR Department of Computer Science Technical Report Number CSC-94-06} (B. McMillin, P. Li).

\XP``An Algorithm for Generating Executable Assertions for Fault Tolerance,'' {\it UMR Department of Computer Science Technical Report Number CSC 92-01} (B. McMillin, H. Lutfiyya and M. Schollmeyer).

\XP``A Run-Time Decision Procedure for Responsive Computing Systems'' {\it UMR Department of Computer Science Technical Report Number CSC 93-29}, (B. McMillin, M. Insall and B. McMillin)

\XP``Constructing an Interval Temporal Logic for Real-Time Systems'' {\it UMR Department of Computer Science Technical Report Number CSC 93-25}, (G. Tsai, M. Insall and B. McMillin) (submitted to Journal of Applied Non-Classical Logic).

\XP``Ensuring the Satisfaction of a Temporal Specification at Run-Time'' {\it UMR Department of Computer Science Technical Report Number CSC 93-20}, (G. Tsai, M. Insall and B. McMillin)

\XP``Fault-Tolerant Distributed Sort Generated from a Verification Proof Outline,'' {\it Responsive Computer Systems - Dependable Computing and Fault-Tolerance,} Vol. 7, 1992, Springer-Verlag, H. Kopetz and Y. Kakuda eds, pp. 71-96. (B. McMillin, H. Lutfiyya and M. Schollmeyer). (Also as a Short Talk in the 14th ICSE, Melbourne, Australia May, 1992).

\XP``Fault-Tolerant Concurrent Branch and Bound Algorithm Derived from Program Verification'' {\it Proceedings of the 16th International COMPSAC}, September, 1992, pp. 182-187, (B. McMillin, A. Sun and H. Lutfiyya).

\XP``Fault-Tolerant Matrix Multiplication with One-Iteration Fault Latency,'' {\it Proceedings of the 15th International COMPSAC}, September, 1991, pp. 665-672, (B. McMillin, C. Hong).

\XP ``Reliable Parallel Sorting Through the Application-Oriented Fault Tolerance Paradigm'' {\it IEEE Transactions on Parallel and Distributed Computing}, Vol. 3, No. 4, pp. 411-420, (B. McMillin, L. Ni). (also appeared in {\it Proceedings of the 9th International DCS}, 1989).

Computational Aerospace Science on Scalable Multicomputers

Sponsored by NASA

Computational Fluid Dynamics (CFD) problems, such as those that arise in application such as modeling hypersonic propulsion systems, require enormous amounts of CPU time to solve.

ARPA-sponsored work, as in the Touchstone project, has created physical hardware, such as the Intel Paragon and Thinking Machines CM-5, scalable to the TERRAFLOPS range which can, potentially, alleviate this computational time burden.

However, little effort is still placed on parallel-specific numerical and algorithmic techniques. Even straightforward, synchronous, parallelization of CFD problems does not yield the best performance due to synchronization overheads between the processors.

The goals of this research are to:

The proposed work extends a pilot project in three-dimensional hypersonic flow in which linear speedup results were obtained on an Intel iPSC/2 multicomputer. The proposed research will enable consideration of real-world problems through parallel processing.

There is always a link back to our main research interests list.

Recent Publications:

\XP``Relaxing Synchronization in Distributed Simulated Annealing,'' {\it IEEE Transactions on Parallel and Distributed Systems} (B. McMillin, C. Hong) (to appear).

\XP ``An Enhanced Reconfigurable Embedding Scheme for Rings in Hypercubes,'' {\it Proceedings of the 1992 International Conference on Parallel and Distributed Systems,} (B. McMillin, J. Liu), pp. 298-305, December, 1992.

\XP``The Computation of Supersonic Combustor Flows using Multi-Computers,'' {\it American Institute of Aeronautics and Astronautics (AIAA)}, AIAA paper number 93-0060, Reno, NV, January, 1993, (B. McMillin, D. Riggins, M. Underwood, L. Reeves, and E. Lu).

\XP ``Modeling of Supersonic Combustor Flows Using Parallel Computing,'' {\it Computer Systems in Engineering,} Pergamon Press Ltd., Great Britain, Vol. 3, Nos 1-4, pp. 217-229, 1992, (B. McMillin, D. Riggins, M. Underwood, L. Reeves, and E. Lu).

\XP ``A Divide and Conquer Ring Embedding Scheme on Hypercubes with Efficient Recovery Capability,'' {\it Proceedings of the 21st International Conference on Parallel Processing,} pp. III-38-III-45, August, 1992 (B. McMillin, J. Liu).

Identification and Control of Nonlinear Systems Using Recurrent Neural Networks

Sponsored by NSF and EPRI

Control of three-dimensional end milling operations is a fundamental aspect of manufacturing complex-contoured parts. Controlling the cutting force, as the tool wears, while maintaining high production yields, is a difficult (nonlinear) control task. While neural networks provide a promising approach to adaptive control, their training time can be prohibitive.

This research seeks to develop a methodology to use recurrent neural networks for identification and control of nonlinear systems in a parallel computing environment. A recursive least squares (RLS) algorithm will be developed and implemented on the nCUBE multicomputer to ensure that off-line learning will be accomplished in a reasonable time frame. Validation of the concept using three-dimensional end milling is valuable to assure the efficacy of the research to the problems of advanced manufacturing.

There is always a link back to our main research interests list.

Recent Publications:

\XP ``A Neural Controller for Force Control in End Milling,'' {\it 1994 International Mechanical Engineering Congress and Exposition,} (B. McMillin, K. Krishnamurthy, Q. Xu, and W. Lu), November, 1994, (to appear).

\XP ``A Recursive Least Squares Training Algorithm for Multilayer Recurrent Neural Networks,'' {\it Proc. of the American Control Conference,} (B. McMillin, K. Krishnamurthy, Q. Xu, and W. Lu), June, 1994, (to appear).

\XP ``Parallel Implementation of a Recursive Least Squares Neural Network Training Method on the Intel iPSC/2,'' {\it Journal of Parallel and Distributed Computing}, Vol. 18(1993), pp. 89-93 (B. McMillin, J. Steck, K. Krishnamurthy, M. Ashouri, and G. Leininger). (Also appeared in {\it Proceedings of International Joint Conference on Neural Networks,} 1990).

Department of Computer Science, University of Missouri-Rolla
For suggestions/problems/questions, send email to ff@umr.edu.
Last updated 10/13/99