Boeing Bold Stroke Avionics Example
This section illustrates the use of the Alderis language in a case study from the domain of avionics distributed real-time embedded (DRE) systems. Figure 1 shows the component-based architecture of the system, which is built upon the Boeing Bold Stroke real-time middleware. This application is deployed on a non-preemptive multiprocessor platform. As shown in Figure 1, this application is driven by five Timer components deployed on five CPUs.
Figure 1 - Aspects of the Bold Stroke Application
Computations on different processors are driven by their respective timers. Components, however, do not necessarily execute with the timer's rate, as seen in the NAV_DISPLAY component's case. It is executed more often to serve remote requests than to serve local requests on CPU_3.
Compositional Analysis
Figure 3 shows how we modeled the system in the Uppaal model checker tool. The application consits of 11 Task components and 11 event channels, which 5 are local and used only for buffering. The application is deployed on 5 processors. We have to model event channels explicitly (1) when we have to buffer events or (2) on remote event channels which have measureable delays. All the event channels satisfy one of the above conditions, except the timer's event channels that have been abstracted out in the model.
The scheduling policies are represented by Schedulers in the DRE Semantic Domain. Since the Bold Stroke application is deployed on a 5-processor architecture we define 5 schedulers as shown on Figure 3. The schedulers get more complex according to the scheduling policies. The automatic generation of the models provides a safe way to ensure the correct guard conditions and assignments. The timed automata model shown in Figure 3 corresponding to the Bold Stroke system shown in Figure 1 has been shown to be schedulable.
Figure 3 - Generated timed automata models
