The goal of this task was to investigate how formal methods could be incorporated into a software engineering process for flight-control systems under DO-178B and to demonstrate that process by developing a formal specification for NASA's Guidance and Controls Software (GCS) Experiment. GCS is software to control the descent of a spacecraft onto a planet's surface. The GCS example is simplified from a real example spacecraft, but exhibits the characteristics of realistic spacecraft control software. The formal specification is written in Larch.
Using formal specification in the Guidance and Control Software (GCS) experiment. Formal design and verification technology for life critical systems
1994-04-05
Report
No indication
English
Formal specification and verification of Ada software
AIAA | 1991
|Formal specification and verification of Ada software
NTRS | 1991
|Formal Specification of Software Critical Systems with Agents
British Library Conference Proceedings | 1995
|Formal Verification of Flight Critical Software
AIAA | 2005
|