=Paper=
{{Paper
|id=Vol-1294/paper16
|storemode=property
|title=Compositional Schedulability Analysis of An Avionics System Using UPPAAL
|pdfUrl=https://ceur-ws.org/Vol-1294/paper16.pdf
|volume=Vol-1294
|dblpUrl=https://dblp.org/rec/conf/icaase/BoudjadarKLN14
}}
==Compositional Schedulability Analysis of An Avionics System Using UPPAAL==
https://ceur-ws.org/Vol-1294/paper16.pdf
ICAASE'2014 Compositional Schedulability Analysis of An Avionics System Using UPPAAL
Compositional Schedulability Analysis of
An Avionics System Using UPPAAL
Abdeldjalil Boudjadar, Jin Hyun Kim, Kim G. Larsen, Ulrik Nyman
Institute of Computer Science, Aalborg University, Denmark
Abstract—We propose a compositional framework for analyz- _ L_
TimingN
ing the schedulability of hierarchical scheduling systems. The requirements
_
ConcreteNtaskNbehavior
framework is realized using Parameterized Stopwatch Automata ResourceNSharing UPPAALN
Nprotocols
to describe tasks, whereas the schedulability analysis is per- NetworkNofNHybrid
ConcreteNtaskNbehavior
formed using UPPAAL. The concrete behavior of each periodic HierarchicalN TimedNAutomata
architecture
preemptive task is given as a list of timed actions to which
resources are assigned by SIRAP protocol. Our framework is S SchedulabilityN
analysis
reconfigurable in which the hierarchical structure, the scheduling )modelNchecking:
policies, the concrete task behavior and the shared resources can C1 C2
all be reconfigured. Finally, we use our framework to analyze
the schedulability of a real-time avionics system. T1 T2 T3 T4
Schedulable:N
Keywords-Hierarchical scheduling systems, Parameterized NyesN/Nno
stopwatch automata, Compositional analysis, Uppaal.
Fig. 1. Overview of the analysis framework
I. I NTRODUCTION
In the area of real-time embedded systems, like avionics and Our framework is implemented using parameterized stop-
automotive, it is primordial to ensure the continually correct watch automata models. To enable and manage resource shar-
behavior of such systems. Avionics and automotive systems ing between tasks, we use the SIRAP (Subsystem Integration
consist of both safety-critical and non safety-critical features, and Resource Allocation Policy) protocol [4]. System tasks
which are implemented in components that might share re- are instances of the same timed automaton with different
sources (e.g. processors). Resource utilization represents a input parameters. A special parameter of the task model is
common challenge for both academics and practitioners, and a list of timed actions [10], specifying the concrete behavior
thus it is important to have an efficient and reliable scheduling of the given task. This list includes abstract computation
policy for the individual parts of the system. Scheduling is steps, locking and unlocking resources. Fig. 1 summarizes our
a widely used mechanism for guaranteeing that the different approach, where the system aspects are separately specified
components of a system will be provided with the correct in three profiles: timing requirements, resource sharing and
amounts of resources. system architecture. This separation of concerns leads our
A scheduling system consists of a set of concurrent tasks framework to be reconfigurable and flexible in the way that
(processes) competing resources according to a scheduling updating a profile does not necessary affect the other two
policy. Each task has a set of timing requirements to fulfill. A profiles [15].
hierarchical scheduling system consists of multiple scheduling Thanks to the parameterization, the framework can easily be
systems in a hierarchical structure. A scheduling system is said instantiated for a specific hierarchical scheduling application.
to be schedulable if all its tasks achieve their jobs without Similarly, each scheduling policy (e.g. EDF: Earliest Deadline
missing any deadline. First, FPS: Fixed Priority Scheduling, RM: Rate Monotonic) is
Compositional analysis has been introduced [9], [14], as a separately modeled and can be instantiated for any component.
key model-checking technology, to deal with state space explo- We analyze the model in a compositional manner, so that
sion caused be the parallel composition of components. In this the schedulability of each component is analyzed together with
paper, we propose a model-based approach for analyzing the the interface specifications of the level directly below it. In
schedulability of hierarchical scheduling systems. We profit this analysis, we non-deterministically supply the required re-
from the technological advances made in the area of model- sources of each component, i.e. each component is guaranteed
checking to analyze the schedulability of real-time systems. to be provided its required resources for each period. This fact
While schedulability is a liveness property, it can be checked is viewed by the component entities as a contract by which
in U PPAAL as a reachability property. In fact, this done by the component has to supply the required resources, provided
adding to the behavior of each task an Error state. Such by the component parent level, to its sub entities. The main
a state is immediately reachable from any other state of the contribution of this paper combines:
given task once the deadline is missed. • a compositional analysis approach where the schedula-
The research presented in this paper has been partially supported by EU bility of a system relies on the recursive schedulability
Artemis Projects CRAFTERS and MBAT. analysis of its individual subsystems.
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 140
ICAASE'2014 Compositional Schedulability Analysis of An Avionics System Using UPPAAL
System deadline (d), priority (prio) and preemption (p). The execu-
EDF
tion time (et) specifies the CPU usage time required by the
task execution for each period (prd). Deadline parameter (d)
represents the latest point in time at which the task execution
EDF RM
Component1 Component2 must be done. The parameter prio specifies the user priority
(100,37) (70,25) associated to the task. Finally, p is a Boolean flag stating
whether or not the task is preemptive. The task behavior is a
sequence of timed actions consuming CPU time and resources.
task1 task2 task3 task4 task5
(300,30)
Moreover, task and component parameters prd, budget and et
(250,40) (400,50) (140,7) (150,7)
can be single values or time intervals.
Fig. 2. Example of hierarchical scheduling system. An example of a hierarchical scheduling system is depicted
in Fig. 2. For the sake of simplicity, we omit task deadlines
• a reconfigurable schedulability framework where a sys- and consider them the same as periods. Moreover, we only
tem structure can be instantiated in different configura- consider single parameter values instead of time intervals.
tions to fit different applications. In this example, the top level System schedules Component1
• modeling of concrete task behavior as a sequence of
and Component2 with the EDF scheduling algorithm. The
timed actions requiring CPU and resources. components are viewed by the top level System as tasks having
• Resource sharing between tasks which is managed by a
timing requirements. Component1, respectively Component2,
U PPAAL implementation of SIRAP protocol. has the interface (100, 37), respectively (70, 25), as period
and execution time. The system shown through this example
The rest of the paper is organized as follows: Section II is an is schedulable if each component, including the top level, is
informal description of our compositional analysis technique schedulable. Thus, for the given timing requirements Com-
using a running example. Section III includes both the back- ponent1 and Component2 should be schedulable by the top
ground and the modeling theory of hierarchical scheduling level System according to the EDF scheduling policy. The
systems. In section IV, we give the U PPAAL models of our tasks task1 and task2 should be schedulable, with respect to
framework where we consider concrete behavior of tasks. the timing requirement of Component1 (100, 37), also under
Moreover, we show how the compositional analysis can be the EDF scheduling policy. Similarly, task3, task4 and task5
applied on the models using the U PPAAL verification engine. should be schedulable, with respect to the timing requirements
Section V shows the applicability of our framework, where we of Component2, under the RM scheduling policy.
analyze the schedulability of an avionics system. Section VI For a given system structure, we can have many different
introduces related work. Finally, section VII concludes our system configurations. A system configuration consists of an
paper and outlines the future work. instantiation of the model where each parameter has a specific
value. Fig. 2 shows one such instantiation.
II. C OMPOSITIONAL S CHEDULABILITY A NALYSIS In order to design a framework that scales well for the
analysis of larger hierarchical scheduling systems, we have
In this paper, we structure our system model as a set decided to use a compositional approach [5], [6]. Fig. 3 shows
of hierarchical components. Each component, in turn, is the how the scheduling system, depicted in Fig. 2, is analyzed
parallel composition of a set of entities (components or tasks) using three independent analysis steps. These steps can be
together with a local scheduler. Namely, each component is performed in any order.
specified with a period (prd), a budget (budget) stating the
execution time that the component should be provided with, A
and a scheduling policy (s) to manage the CPU allocation System
to the component child entities. The real-time interface of a EDF
component consists of prd and budget.
A parent component treats the real-time interface of each A1 A2
Component1 Component2
one of its child components as a single task with the given
EDF RM
real-time interface. The component supplies its child entities
with CPU and resource allocation according to their real-
time interfaces. The analysis of a component (scheduling unit)
task1 task2 task3 task4 task5
consists of checking that its child entities can be scheduled
within the component budget according to the component
EDF,.RM:.scheduling.policies..A,.A1,.A2:.analysis.processes.
scheduling policy. A component can be also parameterized
by a set of typed resources (R) which serve as component Fig. 3. Compositional analysis
local resources. One can remark that the CPU can be managed
by any scheduling policy s, whereas the sharing of the other The schedulability of each component, including the top
resources will be managed by S IRAP. level, is analyzed together with the interface specifications of
Tasks represent the concrete behavior of the system. They the level directly below it. Accordingly, we will never analyze
are parameterized with period (prd), execution time (et), the whole hierarchy at once. In Fig. 3, the analysis process A
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 141
ICAASE'2014 Compositional Schedulability Analysis of An Avionics System Using UPPAAL
consists of checking whether the two components Component1 Fig. 1 summarizes our approach. Information on the
and Component2 are schedulable under the scheduling policy scheduling requirements of the system is combined with the
EDF. In this analysis step, we only consider the interfaces of hierarchical structure of the system together with a detailed
components in the form of their execution-time (budget) and description of the tasks behavior. A timed action can be
period, so that we consider the component as an abstract task specified to execute on a specific piece of hardware such as
when performing the schedulability analysis of the level above the CPU, Input or Output units. All of this information is
it. In this way, we consider the component-composition prob- used as parameters for Stopwatch Automata templates that
lem similarly to [21] but using a non-deterministic supplier are part of the framework. Once a specific instance of the
model for the interfaces. When performing an analysis step framework has been created, its schedulability can be checked
like A1, the resource supplier is not part of the analysis. In compositionally using U PPAAL.
order to handle this, we add a non-deterministic supplier to The isolation of components in hierarchical scheduling
the model. The supplier will guarantee to provide the amount systems and the separation of profiles in our framework have
of execution time, specified in the interface of Component1, the advantage of making systems flexible, where components
before the end of the component period. We check all possible can be reused, upgraded and analyzed individually.
ways in which CPU and resources can be supplied to the
subsystem in A1. The supplier of each component provides
A. Resource Sharing in Hierarchical Scheduling Systems
CPU resource to the child entities of that component in a non-
deterministic way. During the analysis of A1, the supplier non- The limitation of resources represents a strong factor in the
deterministically decides to start or stop supplying, while still setting of any software system, because resources cannot be
guaranteeing to provide the required amount to its sub entities duplicated due to their cost. So that the concurrent processes
before the end of the period. The analysis A2 is performed in of a system compete to gain the access to resources in order
the same way as A1. to perform their jobs, and only one process is allowed to use
Our compositional analysis approach results in an over- the resource at a time. The mechanism to ensure that only
approximation i.e. when performing the analysis of a subsys- one process gains the use of a resource at time is known
tem, we over-approximate the behavior of the rest of the sys- as mutual exclusion. However in the area of hierarchical
tem. This can result in specific hierarchical scheduling systems scheduling systems, due to the hierarchy the classical mutual
that could be schedulable if one considers the entire system exclusion mechanisms cannot operate fairly. Resource sharing
at once, but that is not schedulable using our compositional protocols have been designed to reasonably share (non-CPU)
approach. We consider this fact as a design choice which resources between system tasks where the system architecture
ensures separation of concerns, meaning that small changes is hierarchical. Some popular resource sharing protocols are:
to one part of the system does not effect the behavior of other Priority Inheritance Protocol (P IP) [18], the Priority Ceiling
components. In this way, the design of the system is more Protocol (P CP) [17], the Stack Resource Policy (S RP) [2],
stable which in turn leads to predictable system behavior. and Subsystem Integration and Resource Allocation Policy
This over-approximation, which is used as a design choice, (S IRAP) [4]. Roughly speaking, a resource sharing protocol for
should not be confused with the over-approximation used hierarchical systems is equivalent to the set of local schedulers
in the verification algorithm inside the U PPAAL verification that components use to arbitrate their tasks on CPU.
engine. Due to hierarchy, we have chosen to use the S IRAP protocol
Thanks to the parameterization of system entities; schedul- [4] to manage resource sharing in our framework. In fact,
ing policies, preemptiveness, execution times, periods and S IRAP has been developed as a way to integrate different
budgets can all easily be changed. In order to estimate the subsystems, endowed with different scheduling policies, in one
performance and schedulability of our running example, we hierarchical scheduling system with the presence of shared
have evaluated a number of different configurations of the resources. Subsystems can be isolated from each other, even
system. This allows us to choose the best of the evaluated though they share mutually exclusive resources, for composi-
configurations of the system. tional verification, validation and unit testing.
III. BACKGROUND AND T HEORY
B. Modeling Theory
Hierarchical scheduling systems are structured to be one
or more components running on the same execution platform. A task has a concrete behavior performing a sequence of
Each component, in turn, consists of a set of entities that can timed actions. Each timed action can either be a computation
be developed independently and a local scheduler. Component step (Compute), access or release of a shared resource
entities are known by the component workload, and are either (Lock, Unlock) or particular statements marking the end
components or tasks. The execution platform we consider in of the period (Pend) or the end of the task execution (End).
our framework is a single processor (CPU). We specify the Definition 1 (Timed action): Given a set of action names
behavior of each task by a sequence of timed actions (com- Acts = {Compute, Lock, Unlock, Pend, End}, a
putation steps, input, output, etc) that use CPU and resources. CPU and a set of resources R, a timed action A is a one step
The CPU resource is arbitrated by different scheduling policies computation given by the tuple hAct, P roc, BCET, W CET i
such as EDF, RM and FPS, whereas the resource sharing is where:
managed by a resource sharing protocol. • Act ∈ Acts is the action name,
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 142
ICAASE'2014 Compositional Schedulability Analysis of An Avionics System Using UPPAAL
• P roc ⊆ {CP U }∪R specifies the identifiers of processor the execution time of preemptable tasks. This section gathers
and resources that the timed action A requires for its the Parameterized Stopwatch Automata (PSA) models of our
execution, framework, as well as the U PPAAL analysis. Due to space
• BCET and W CET are respectively best case and worst limitations, we only explain important features.
case execution times,
By A we denote the set of all timed actions. In fact, the A. PSA Resource Model
CPU and resources can be viewed as a multi-core execution
The hierarchical scheduling system structure is a set of
platform. Likewise, we define the behavior B of a task as a
scheduling components, each one includes a single specific
transition system hL, l0 , →i specifying the sequence of timed
scheduling algorithm and a set of entities (tasks or com-
actions performed by that task, where L is a set of states,
ponents). To analyze a single component by means of a
l0 ∈ L is the initial state and →⊆ L × A × L is the transition
compositional manner, it is necessary to consider the inter-
relation. States can be interpreted in the semantic level as
rupted behavior of that component by the other concurrent
valuations of the task variables together with the state of
components within the same system. However, it is hard to
each task (ready, waiting, preempted, done, etc). The behavior
capture the interrupting behavior of the other components that
of a component is given by the parallel composition of the
influence the component under analysis. For this reason, we
transition systems of its nested tasks.
introduce a non-deterministic supplier to model all scenarios
Definition 2 (Task structure): A task T is given by
that the component under analysis can run. Such a non-
hP rd, BCET, W CET, P ri, B, Dlni where P rd is the task
deterministic fact simulates the influence of the other system
period, BCET and W CET are respectively best case and
components on the execution of the component under analysis.
worst case execution times of T , P ri is the priority level
The scheduling policy within the component then allocates the
associated to task T , B is the task behavior stated above and
Dln is the deadline.
Therefore, the task specification is given by an interface
P rd, BCET, W CET, Dln stating the time constraints, a be-
havior B expressed by a sequence of timed actions and a
priority P ri that will be applied for each timed action of the
task in question.
Roughly speaking, a component is given by an interface
stating its timing requirements and a local policy for schedul-
ing its nested entities (workload). The interface of a component
C 0 can be viewed by its parent component C as resource
requirements that must be supplied by C to C 0 , and it is viewed
by the child entities of C 0 as a contract that the component C 0 Fig. 4. PSA model of supplier template
will provide the amount of resources specified in its interface
to its workload. For the sake of simplicity, we do not consider CPU resource to tasks. It also abstracts the possibility that a
local resources for each component, i.e. all resource are global task from another component of the system (not part of the
and shared by all of the system components. current analysis step) could preempt the execution of tasks of
Definition 3 (Component): A component C is a tuple the current component.
hP rd, Budget, P ri, s, he1 , .., en ii where: Fig. 4 shows the PSA model of supplier. supply-
• P rd and P ri are the same as for tasks, ing time[supid] is a stopwatch that measures the CPU time
• Budget is the amount of CPU time that the component provided by supplier during each period, so that it only
guarantees to provide to its workload, progresses when the supplier is at location Supplying. In
• s ∈ {EDF, F P, RM, ..} is a scheduling policy, fact, the supplier keeps traveling between locations Supply-
• he1 , .., en i are component entities (workload), either tasks ing and NotSupplying while the budget is not fully pro-
or other components. vided (supplying time[supid]≤ sup[supid].budget) and the slack
Similarly, a system is the top level component without tim- time (curTime ≤ sup[supid].prd -sup[supid].budget + supply-
ing requirements (P rd, Budget, P ri). We emphasize the fact ing time[supid]) is not expired, until the component budget is
that our framework can be instantiated for any combination of fully provided (supplying time[supid]≥ sup[supid].budget) and
scheduling algorithms. then starts a new period from location Done.
IV. UPPAAL M ODELING AND A NALYSIS B. PSA Model of Tasks
The U PPAAL verification suite provides both symbolic A task model is depicted in Fig. 5. After being started
and statistical model checking (SMC). The models which at location Idle, the task joins location WaitingOffset waiting
in practice can be analyzed statistically, using the U PPAAL until the task offset is expired. From that location, the task
SMC verification engine, are larger and can contain more moves to location ReadingOP where it can read a PEND
features. Stopwatches [8] are clocks that can be stopped and command and thus joins ClosingPeriod to finalize a period
resumed without a reset. They are very practical to measure execution, and then moves to the location PeriodDone. At
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 143
ICAASE'2014 Compositional Schedulability Analysis of An Avionics System Using UPPAAL
location ReadingOP, the task can also read operations COM-
PUTE, LOCK SIRAP, and UNLOCK SIRAP from its concrete
behavior description. By reading a COMPUTE command, the
task checks it own status if it is either READY or RUNNING.
A READY status means that the task is ready to run using the
CPU, whereas RUNNING means that the task is still scheduled
to use CPU. From location ReqSched, the task updates its
status to RUNNING and inserts its Id into the CPU queue. From
location CheckingSupply, the task checks whether the supplier
is providing the CPU resource. If the supplier is currently
providing CPU resource, the task moves to location Execut- Fig. 7. PSA model of CPU template
ing, otherwise it moves to location Suspended. At location
Executing, the task checks if it has been assigned a CPU via checks whether the requesting task is the current scheduled
function isTaskSched(). If so, the stopwatch proTime[tid] keeps one (sel tid(rid) == req tid(rid)) or not.
progressing while the wcet and deadline are not reached yet. If it is not the case, the status of the requesting task
The task may keep traveling between locations Executing and will be updated to PENDING RESOURCE and the protocol
Suspended according to whether or not the CPU is supplied. joins the initial location. Otherwise, the protocol checks that
The task joins location MissDeadline whenever the deadline is the time left from the component budget of the current
missed. task (sup[tstat[sel tid(rid)].pid].budget) covers the amount of
The task execution can be delayed due to the resource resource requested by the task in question. If the budget of the
managed by S IRAP, once the task requests a resource via current task supplier is greater than the sum of time supplied
command LOCK SIRAP. Such a delay can be one of the by that supplier to its tasks and the resource usage time of
followings: the current request (sup[tstat[sel tid(rid)].pid].budget ≥ supply-
ing time[tstat[sel tid(rid)].pid] + tstat[sel tid (rid)] .rc time) then
• At location GlobalWaiting, the task is locally (designated
at the component level) allocated to use the resource, but the resource request will be satisfied for the current task,
it is not globally allocated for the same resource, i.e. a otherwise the current requesting task has to wait for the next
task from another component is using the resource. supply (tstat[sel tid(rid)].status = PENDING BUDGET).
• At location LocalWaiting, the task is not locally allocated
to use the resource. D. PSA CPU Model
• At location SIRAPWaiting, the task is delayed due to The PSA model of the CPU template is depicted in Fig. 7.
S IRAP protocol, i.e. in the case of a deficit of the After receiving a request r req[rid] from a task, the CPU
remaining resource of the supply for a period. template activates the component scheduling policy policy in
From location CheckTaskPendingStatus, the task either order to determine to which task the CPU resource should be
moves to LocalWaiting by losing the resource allocation, or to assigned. rid is the CPU resource identifier. Once the CPU
location SIRAPWaiting by a deficit of the supplied resource. is assigned to a task, at location Assign, such a task keeps
By reading a UNLOCK SIRAP command at location using the CPU resource until it is done (finished[rid]?) or a new
ReadingOP, the task withdraw its identifier tid from the request (r req[rid]?) to reschedule the CPU appears. Whenever
resource queue managed by S IRAP. a CPU schedule is done (finished[rid]) and the CPU waiting
The schedulability of a task can be checked via the reach- list is not empty (rq[rid].length>0), the CPU resource moves
ability of location MissDeadline using the query: to location ReqSched and restarts the scheduling process,
E<>MissDeadline. otherwise it keeps waiting at location Idle until a task requests
In order to avoid checking the schedulability of each task the CPU resource.
separately, we introduce a global variable error that can be
updated to true by any task missing its deadline, so that
V. C ASE S TUDY
the schedulability of a component can be checked using the
following query: A[] error!=1. To show the applicability of our compositional framework,
we have modeled the avionics system introduced in [16],
[12], and analyzed its schedulability. In fact, this system is a
C. PSA Model of Resource Sharing Protocol partial specification for a hypothetical avionics mission control
To share resources between the tasks of a hierarchical computer (MCC) system dedicated to combat and attack
scheduling system, we use S IRAP protocol. In fact, S IRAP aircrafts. The application is a composition of 15 tasks declared
enables the isolation of system components from each other with different priorities and timing requirements, together with
even in the presence of mutually exclusive shared resources. shared resources to perform input and output communications.
We have modeled S IRAP protocol as shown in Fig. 6. Initially, We have used S IRAP protocol [4] to assign the input and
the protocol holds in the initial location, WaitSchedReq, wait- output communication resources to the competing tasks of the
ing for a resource request from one of the candidate tasks. By different components.
the reception of a new resource request run schedu[SIRAP][I] A brief description of the avionics system tasks is given
where I is the identifier of the requested resource, S IRAP below:
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 144
ICAASE'2014 Compositional Schedulability Analysis of An Avionics System Using UPPAAL
Fig. 5. PSA model of task template
Fig. 6. PSA model of SIRAP protocol
• Weapon release (T1 ): this task checks periodically if the task.
bomb button is being pressed or the time of a scheduled • HOTAS Bomb Button (T5 ): a target is designated as an
release is reached to drop a weapon. attack target by activating the Hands-On Throttle And
• Radar tracking (T2 ): it explores a ground map, or per- Stick switch.
forms a ground search or a single-target track. • Aircraft Flight data (T6 ): it determines the best available
• Target tracking (T3 ): this task captures the target position estimates of aircraft position, velocity, attitude, motion
relative to the aircraft. The radar keeps tracking a target through air-mass, etc.
if it is already spotted, and also designated by the aircrew • HUD display (T7 ): the Head-Up Display shows the aircraft
for a potential attack. flight data (airspeed, heading, etc.), the strike point and/or
• Target sweetening (T4 ): no description provided for this seeker position.
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 145
ICAASE'2014 Compositional Schedulability Analysis of An Avionics System Using UPPAAL
TABLE I Avionics
G ENERIC AVIONICS TASK ATTRIBUTES
S
Tasks Prd Exec Dln Prio Input Msg Output Msg
T1 10 1 5 1 3, 1 1 Control & Display Sensor & Navigation Fire & Stores Background
T2 40 2 40 2 24, 1 3 (10000, 7419 ) ( 10000, 6982) ( 10000, insuf) ( 10000, 442)
T3 40 4 40 3 1, 4, 1, 3 6, 3
T4 40 2 40 4 1 FPS FPS FPS FPS
T5 40 1 40 5 4 11
HUD Display (T7) Flight Data (T6) AUTO/CCIP Toggle(T12) Reinitiate Traject (T14)
T6 50 8 50 6 5, 12, 1 3, 25, 18, 18
T7 50 6 50 7 18, 3, 4 7
MPD Display (T8) Steering (T9) Weapon Traject (T10) Periodic BIT (T15)
T8 50 8 50 8 1, 20, 20, 7, 3, 3 5
T9 80 6 80 9 6, 1, 6, 3 3 HOTAS Button (T5) Weapon Release (T1)
Poll RWR (T13)
T10 100 7 100 10 17, 3, 1, 1, 1 6
T11 100 3 100 11 1, 1 Threat Display (T11) Radar Tracking (T2)
T12 200 1 200 12 4 11
T13 200 2 200 13 20 2 Target Tracking (T3)
T14 400 6 400 14 17, 3, 1, 1, 1 6 insuf : insufficient budget
T15 1000 5 400 15 1, 1, 1, 1, 1, 1 2 Target Sweetening (T4)
Fig. 8. Architecture of the Avionics System
• MPD display (T8 ): the Multi-Purpose Display shows the
tactical situation, the threat data, a display of stores components interfaces are shown in Fig. 8. In fact, as commu-
remaining, radar display information, etc. nication times are given in microseconds we convert the task
• Steering (T9 ): it computes the steering cues for display timing requirements from milliseconds to microseconds. Thus,
based either on way-point steering or target attack steer- the interface of each component is given in terms of period and
ing. budget specified in microseconds. Tasks are gathered together
• Weapon trajectory (T10 ): it computes the weapon trajec- within components based on their features. Component 1
tory (ballistics) one minute before its release based on (Control and Display) includes 4 tasks concerning the graphical
aircraft speed, target range, etc. display of information. Component 2 (Sensor and Navigation)
• Threat response display (T11 ): once the radar warning re- encapsulates 6 tasks concerning the navigation system and
ceiver detects a potential target, the current task analyzes external sensors. Component 3 (Fire and Stores) includes 3
that warning and displays the information for the aircrew. tasks. It manages the firing system and checks periodically the
• AUTO/CCIP toggle (T12 ): the weapon release modes weapons store. Component 4 (Background) encapsulates two
include automatic (AUTO) and continuously computed tasks to check the aircraft devices and potentially reinitiate the
impact point (CCIP) delivery. trajectory. Each of these component has a local FPS scheduling
• Poll RWR (T13 ): the Radar Warning Receiver warns the policy.
aircrew of hostile radar energy being beamed at the To perform the schedulability analysis of each individual
aircraft. component of the avionics system, we have introduced a non-
• Reinitiate trajectory (T14 ): this task updates the trajectory deterministic supplier and estimated the minimum budget of
of aircraft based on radar status, aircrew actuation, etc. each supplier. A model-based technique for the computation of
• Periodic BIT (T15 ): the Built-In Test task periodically the supplier (minimum) budget has been introduced in [5] [6].
queries each aircraft device and analyzes responses to It consists of finding a budget candidate using U PPAAL SMC
determine if a failure has occurred. (statistical model checking), then ckecking the schedulability
The task attributes of the avionics systems are depicted in of the concerned component against that budget candidate
Table I. The task timing requirements are given in millisec- using symbolic model checking of U PPAAL.
onds. To each task is assigned a priority level, where lower Following the analysis method described in section II, our
numbers indicate lower priorities. Tasks may perform Input compositional analysis shows that each component is individ-
and Output actions to communicate messages on the dedicated ually schedulable, except component Fire and Stores which
input and output resources, respectively. The sequence of cannot be schedulable on a single-core execution platform.
messages that are sent or received by a task are specified Accordingly, the top level component (Avionics system) can-
in columns ”Input Msg” and ”Output Msg” respectively, not be schedulable under any scheduling policy S. Obviously,
where each number corresponds to a certain class of words it is easy to remark that the CPU utilization of the avionics
(messages). Each class has a specific length of messages as system exceeds 100% (75% + 69% + 4.4%), which means that
well as a unique transfer time to communicate any of its this system can never be schedulable on a single CPU.
messages. The sequence of numbers state how many messages By seeing the counter-example generated by U PPAAL model
are communicated by a given task during one period. Thus, checker, we can investigate the scenarios showing when one
the communication time of each task depends on how many of the tasks of component Fire and Stores misses its deadline.
messages are communicated and the type of each message. Compared to analytical methods, our approach generates a
These data are exploited by the resource sharing protocol to counter-example that is quite useful to update the task at-
assign Input and Output communication resources. tributes in order to achieve the schedulability of the system. We
The architecture of the whole avionics system as well as the keep the way how to exploit the counter-example in updating
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 146
ICAASE'2014 Compositional Schedulability Analysis of An Avionics System Using UPPAAL
the timing requirements of tasks as a future work. system when analyzing an individual component, we intro-
A challenge encountered during this application is the duced a non-deterministic supplier where the resource supply
estimation of both period and budget of each supplier such of one budget can be given on several chunks, simulating
that 1) each supplier provides enough resources to its child then the preemption that the rest of system may perform
tasks; 2) the parallel composition of all suppliers is schedulable on the behavior of the component under analysis. We also
according to the system level scheduling policy. considered resource sharing between system components and
used S IRAP protocol to manage such a sharing. We have
VI. R ELATED W ORK applied our schedulability analysis framework on an avionics
system where components are analyzed separately even they
Hierarchical scheduling systems were introduced in [13],
share communication resources.
[11]. An analytical compositional framework for hierarchical
scheduling systems was presented in [20] as a formal way to R EFERENCES
elaborate a compositional approach for schedulability analysis [1] T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, and W. Yi. Times: A
of hierarchical scheduling systems [22]. In the same way, the tool for schedulability analysis and code generation of real-time systems.
authors of [19] dealt with a hierarchical scheduling framework In K. G. Larsen and P. Niebert, editors, Proceedings of FORMATS 2003,
volume 2791 of LNCS, pages 60–72. Springer, 2003.
for multiprocessors based on cluster-based scheduling. They [2] T. P. Baker. Stack-based scheduling for realtime processes. Real-Time
used analytical methods to perform analysis, however both ap- Syst., 3(1):67–99, Apr. 1991.
proaches [20], [19] have difficulty in dealing with complicated [3] M. Behnam, T. Nolte, I. Shin, M. Åsberg, and R. Bril. Towards
hierarchical scheduling in VxWorks. In OSPERT, pages 63–72, 2008.
behavior of tasks. [4] M. Behnam, I. Shin, T. Nolte, and M. Nolin. Sirap: a synchronization
Recent research within schedulability analysis increasingly protocol for hierarchical resource sharingin real-time open systems. In
uses model-based approaches, because this allows for mod- Proceedings of EMSOFT 07, pages 279–288. ACM, 2007.
[5] A. Boudjadar, A. David, J. H. Kim, K. G. Larsen, M. Mikučionis,
eling more complicated behavior of systems. The rest of the U. Nyman, and A. Skou. Hierarchical scheduling framework based
related work presented in this section focuses on model-based on compositional analysis using Uppaal. In Proceedings of FACS 2013,
approaches. LNCS Volume 8348. Springer, 2013.
[6] A. Boudjadar, A. David, J. H. Kim, K. G. Larsen, M. Mikučionis,
In [3], the authors analyzed the schedulability of hierarchical U. Nyman, and A. Skou. Widening the schedulability of hierarchical
scheduling systems, using a model-based approach with the scheduling systems. In FACS 2014, To appear. Springer, 2014.
TIMES tool [1], and implemented their model in VxWorks [3]. [7] L. Carnevali, A. Pinzuti, and E. Vicario. Compositional verification
for hierarchical scheduling of real-time systems. IEEE Transactions on
They constructed an abstract task model as well as scheduling Software Engineering, 39(5):638–657, 2013.
algorithms, where the schedulability analysis of a component [8] F. Cassez and K. G. Larsen. The impressive power of stopwatches.
does not only consider the timing attributes of that component In C. Palamidessi, editor, CONCUR, volume 1877 of Lecture Notes in
Computer Science, pages 138–152. Springer, 2000.
but also the timing attributes of the other components that can [9] E. M. Clarke, D. E. Long, and K. L. Mcmillan. Compositional model
preempt the execution of the component under analysis. checking. MIT Press, 1999.
In [10], the authors introduced a model-based framework [10] A. David, K. G. Larsen, A. Legay, and M. Mikučionis. Schedulability
of herschel-planck revisited using statistical model checking. In ISoLA
using U PPAAL for the schedulability analysis of flat systems. (2), volume 7610 of LNCS, pages 293–307. Springer, 2012.
They modeled the concrete task behavior as a sequence of [11] Z. Deng and J. W.-S. Liu. Scheduling real-time applications in an open
timed actions, each one represents a command that uses environment. In RTSS, pages 308–319. IEEE Computer Society, 1997.
[12] R. Dodd. Coloured petri net modelling of a generic avionics missions
processing and system resources and consumes time. computer. Technical report, Department of Defence, Australia, Air
The authors of [7] provided a compositional framework Operations Division, 2006.
for the verification of hierarchical scheduling systems using [13] X. A. Feng and A. K. Mok. A model of hierarchical real-time virtual
resources. In Proceedings of RTSS 2002. IEEE Computer Society, 2002.
a model-based approach. They specified the system behavior [14] J. Lind-Nielsen, H. R. Andersen, H. Hulgaard, G. Behrmann, K. J.
in terms of preemptive time Petri nets and analyzed the system Kristoffersen, and K. G. Larsen. Verification of large state/event systems
schedulability using different scheduling policies. using compositionality and dependency analysis. Formal Methods in
System Design, 18(1):5–23, 2001.
We combine and extend these approaches [7], [10] by [15] G. Lipari, P. Gai, M. Trimarchi, G. Guidi, and P. Ancilotti. A hierarchical
considering hierarchy, resource sharing and concrete task framework for component-based real-time systems. Electronic Notes in
behavior, while analyzing hierarchical scheduling systems in a Theoretical Computer Science, 116(0):253 – 266, 2005.
[16] C. D. Locke, D. R. Vogel, L. Lucas, and J. B. Goodenough. Generic
compositional way. Moreover, our model can easily be recon- avionics software specification. Technical report, DTIC Document,
figured to fit any specific application. Comparing our model- 1990.
based approach to analytical ones, our framework enables to [17] R. Rajkumar, L. Sha, and J. Lehoczky. Real-time synchronization
protocols for multiprocessors. In Real-Time Systems Symposium, 1988.,
describe more complicated and concrete systems. Proceedings., pages 259–269, Dec 1988.
[18] L. Sha, J. P. Lehoczky, and R. Rajkumar. Task scheduling in distributed
real-time systems. In SPIE, volume 0857, pages 909–917, 1987.
VII. C ONCLUSION [19] I. Shin, A. Easwaran, and I. Lee. Hierarchical scheduling framework for
We have introduced a compositional framework for the virtual clustering of multiprocessors. In ECRTS, pages 181–190. IEEE
Computer Society, 2008.
schedulability analysis of hierarchical real-time systems. Sys- [20] I. Shin and I. Lee. Periodic resource model for compositional real-time
tem tasks are modeled using Parameterized Stopwatch Au- guarantees. In RTSS, pages 2–13. IEEE Computer Society, 2003.
tomata (PSA) of U PPAAL. To perform the schedulability [21] I. Shin and I. Lee. Compositional real-time scheduling framework with
periodic model. ACM Trans. Embed. Comput. Syst., 7(3):30:1–30:39,
analysis, we profit from the advances of model-checking tech- May 2008.
nology. The schedulability has been verified as a reachability [22] I. Shin and I. Lee. Compositional real-time scheduling framework with
property. In order to mitigate the behavior of the rest of periodic model. ACM Trans. Embedded Comput. Syst., 7(3), 2008.
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 147