A sound theory of real-time scheduling is necessary to support the engineering of real-time software applications. Developing scheduling results using formal methods helps provide the high level of assurance required in safety-critical domains. We propose a formalization methodology relying on state-machine models and on a library of commonly applicable properties. A case study has shown that rigorous and a detailed verification of nontrivial scheduling results can be performed within reasonable time limits, using modern theorem-proving tools such as PVS. It is still necessary to develop and extend such verification efforts to the increasingly complex scheduling algorithms that may one day be used in safety-critical applications. Other aspects relevant to the avionics domain remain insufficiently explored by the formal methods community. For example, little has been done in the analysis of distributed real-time systems, where difficult problems mixing communication, processing, fault tolerance must be addressed. Formal methods are especially valuable in such complex settings, where informal proofs guided by intuition are insufficient and where other validation approaches such as testing are incomplete. Formal methods should become an essential tool for validating the most critical aspects of real-time systems, such as the partitioning mechanisms required for fault isolation in integrated avionics. Real-time scheduling problems are an ideal application area for formal methods since they are subtle and complex, must be certified to the highest degrees of assurance for supporting critical applications, and thus require very precise, detailed, and rigorous verification.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Formal analysis for real-time scheduling


    Contributors:


    Publication date :

    2000-01-01


    Size :

    660407 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English



    Formal Analysis for Real-Time Scheduling

    Dutertre, B. / IEEE / AIAA | British Library Conference Proceedings | 2000


    Formal analysis for real-time scheduling

    Dutertre, B. / Stavridou, V. | Tema Archive | 2000


    Real-Time Adaptive Aircraft Scheduling

    S. E. Kolitz / M. Terrab | NTIS | 1990


    Automated Hard Real-Time Scheduling

    Browne, A. R. / Bass, J. M. / Croll, P. R. et al. | British Library Conference Proceedings | 1995


    Real-time adaptive aircraft scheduling

    Kolitz, Stephan E. / Terrab, Mostafa | NTRS | 1990