We present a formal basis for the design of a Checker used in validating safe schedules and in selecting error recovery schedules for satellite control systems. This design includes a high-level specification of Checker behavior and properties (called flight rules) of safe schedules. Specifications are written in Timed Linear Logic (TLL). Validation of schedules is performed in terms of real-time telemetry and deduction system proof rules. Telemetry (state information for satellite subsystems) serves as input to the Checker. Detection of violation of a flight rule by the Checker results in the selection of a contingency plan (error recovery schedule). The Checker is illustrated in terms of the TOPEX/Poseidon Oceanographic Satellite System.


    Access

    Access via TIB

    Check availability in my library


    Export, share and cite



    Title :

    Verifying command sequences for satellite systems


    Contributors:


    Publication date :

    1992-10-01



    Type of media :

    Miscellaneous


    Type of material :

    No indication


    Language :

    English