Time partitioning is a crucial property for integrated modular avionics architectures, particularly those in which applications of different criticalities run on the same processor. In a time-partitioned operating system, the scheduler is responsible for ensuring that the actions of one thread cannot affect other threads' guaranteed access to CPU execution time. However, the large number of variables affecting application execution interleavings makes it difficult and costly to verify time partitioning by traditional means. We believe that automated model checking is a promising technique for verifying the correct design of partitioning algorithms. Our experience with modeling the DEOS scheduler shows that expressive models can be produced at a reasonable cost. Using automated model checking can increase design assurance by allowing coverage of a larger range of execution interleavings than can feasibly be covered by traditional testing. Furthermore, model checking can decrease development and testing costs by finding design errors early in the development cycle.


    Access

    Check access

    Check availability in my library

    Order at Subito €


    Export, share and cite



    Title :

    Using model checking for verification of partitioning properties in integrated modular avionics


    Contributors:
    Cofer, D. (author) / Engstrom, E. (author) / Weininger, N. (author) / Penix, J. (author) / Visser, W. (author)


    Publication date :

    2000-01-01


    Size :

    853330 byte




    Type of media :

    Conference paper


    Type of material :

    Electronic Resource


    Language :

    English