Automatic verification of component-based real-time CORBA applications

Distributed real-time embedded (DRB) systems often need to satisfy various time, resource and fault-tolerance constraints. To manage the complexity of scheduling these systems many methods use rate monotonic scheduling assuming a time-triggered architecture. This paper presents a method that captures the reactive behavior of complex time- and event-driven systems, can provide simulation runs and can provide exact characterization of timed properties of component-based DRE applications that use the publisher/subscriber communication pattern. We demonstrate our approach on real-time CORBA avionics applications.