Non-Standard Analysis and Embedded Software
Richard Platek, Odyssey Research Associates,
richard@oracorp.com
Summary
One model for computing in the future is ubiquitous, embedded
computational devices analagous to embedded electrical motors. Many
of these computers will control physical objects and processes. Such
hidden computerized environments introduce new safety and correctness
concerns whose treatment go beyond present Formal Methods. In
particular, one has to begin to speak about Real Space software in
analogy with Real Time software. By this we mean, computerized
systems which have to meet requirements expressed in the real geometry
of space. How to translate such requirements into ordinary software
specifications and how to carry out proofs is a major challenge. In
this talk we propose a research program based on the use of
non-standard analysis. Much detail remains to be carried out. The
purpose of the talk is to inform the Formal Methods community that
Non-Standard Analysis provides a possible avenue of attack which we
believe will be fruitful.
Slides