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.
Using model checking for verification of partitioning properties in integrated modular avionics
19th DASC. 19th Digital Avionics Systems Conference. Proceedings (Cat. No.00CH37126) ; 1 ; 1D2/1-1D210 vol.1
2000-01-01
853330 byte
Conference paper
Electronic Resource
English
Using Model Checking for Verification of Partitioning Properties in Integrated Modular Avionics
British Library Conference Proceedings | 2000
|IEEE | 1992
|