Formal Modeling

A formal model of a system is a mathematical model of it, at some chosen level of abstraction. Its purpose is to permit precise understanding, specification, and analysis of the system.

Flight guidance controllers

The mode logic of flight guidance controllers can be surprisingly complex and can result in safety-critical errors if pilots are surprised by some unexpected consequence of the logic. Accordingly, specifying and analyzing mode logic has become a benchmark problem for the application of mathematical methods. We have already noted our applications of Z [Fun98] and SPIN [Nay98] to this problem. We have also [Gua91] specified code for a flight guidance controller in the Larch/Ada specification language created for the Penelope verification system [Gua90].

Security models

Since its founding, ATC-NY has been involved in the definition of security models. [McC90], for example, introduced the idea of restrictiveness, which was the first composable information-flow property to be discovered. Restrictiveness implies information-flow security: a restrictive system will allow information from one security level to flow only to users of the same or higher levels. In addition, the composition of two restrictive systems is itself restrictive. This work inaugurated a large body of research on modular reasoning about information flow.

Asynchronous circuits

[Bic94] provides a precise formal semantics for the 4-phase protocol of asynchronous circuit design, proves that the composition of 4-phase circuits will also satisfy the 4-phase axioms, and implements an interactive tool for proving basic properties of these circuits. This work provided a rigorous mathematical basis for an important engineering concept.

References

[Fun98] F. Fung and D. Jamsek. Formal Specification of a Flight Guidance System. NASA/CR-1998-206915, January 1998. http://techreports.larc.nasa.gov/ltrs/PDF/1998/cr/NASA-98-cr206915.pdf

[Nay98] D. Naydich and J. Nowakowski: Flight Guidance System Validation Using SPIN. NASA Contractor Report NASA/CR-1998-208434, June 1998. http://techreports.larc.nasa.gov/ltrs/PDF/1998/cr/NASA-98-cr208434.pdf

[Gua90] D. Guaspari, C. Marceau, and W. Polak. Formal verification of Ada programs. IEEE Transactions on Software Engineering, 16(9):1058-1075, September 1990. http://doi.ieeecomputersociety.org/10.1109/32.58790

[McC90] D. McCullough. A Hookup Theorem for Multilevel Security. IEEE Transactions on Software Engineering, vol 16(6) (Jun. 1990), pp. 563-568. http://doi.ieeecomputersociety.org/10.1109/32.55085

[Bic94] M. Bickford. Composable specifications for asynchronous systems using UNITY. In Proceedings International Symposium on Advanced Research in Asynchronous Circuits and Systems (Nov. 1994), 216-227. http://ieeexplore.ieee.org/iel4/5265/14280/00656314.pdf?tp=&isnumber=&arnumber=66314