Formal Validation of Realtime Middleware
John P. Enright, David W. Miller · Journal of Aerospace Computing Information and Communication · 2007
Distributed terrestrial computer systems employ middleware software to provide communications abstractions and reduce software interface complexity. Embedded applications are adopting the same approaches, but must make provisions to ensure that hard real-time temporal performance can be maintained. This thesis presents the development and validation of a middleware system tailored to spacecraft flight software development. OurmiddlewarerunsontheGeneralizedFlightOperationsProcessingSimulator(GFLOPS) and is called the GFLOPS Rapid Real-time Development Environment (GRRDE). GRRDE provides publish-subscribe communication services between software components. These services help to reduce the complexity of managing software interfaces. The hard real-time performance of these services has been verified with General Timed Automata modelling demonstrating the usefulness of formal analysis techniques for flight software applications.