Applications of Mathematical Tools and Techniques

We have experience in applying many well-known formal notations and analysis tools, such as

• Z and Z/EVES: [Fun98] specifies the mode logic of a flight guidance controller in Z and uses Z/EVES to verify some of its high-level properties.
• SPIN: [Nay98] analyzes the same mode logic using the SPIN model checker.
• Murphi: [Gua00] generates a representation of an annotated real-time program in the input language of the Murphi model checker and uses Murphi to check that its constraints are satisfied.
• PVS: [Gua98] models UML class diagrams in the higher type logic of PVS and uses the PVS theorem prover to verify properties of the diagrams.

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

[Gua98] D. Guaspari and D. Naydich. Flight-guidance systems: UML design, PVS analysis. Odyssey Research Associates Technical Report, TM-98-0035, November 30, 1998.

[Gua00] Guaspari, D.; Naydich, D. Analysis of real-time code by model checking. In Proceedings of the 19th Digital Avionics Systems Conferences (DASC), vol. 1, pages D5/1 - 1D5/8, 2000. http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=886892

[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