The UPPAAL Model for the paper "A Modeling Framework for Schedulability Analysis of Distributed Avionics Systems"

January 11, 2018

UPPAAL Version: UPPAAL 4.1.19


IMASched.xml is a UPPAAL modeling framework for schedulability analysis of distributed avionics systems. It provides the ARINC-653 
and AFDX features in the models, and performs the schedulability analysis by symbolic model checking(MC) and statistical model 
checking(SMC). A sample avionics workload has been encoded into the framework.

A compositional analysis is performed by MC. Each ARINC-653 partition including its communication environment can be checked 
independently. On the basis of the timed selection simulation relation, a set of message interface automata is built to model 
the environment for a partition. The schedulability constraints are verified in the form of the safety property:

A[] not (error == true).

The partition under analysis can be changed by only instantiating the processes in this partition via the following steps:

1) Uncomment the lines of the partition under analysis in the section "Processes-->Compositional analysis" of System declarations.

2) Comment the lines of all the other partitions in the section "Processes-->Compositional analysis" of System declarations.

A global analysis is executed by SMC with better scalability. In this analysis, the whole system model is checked as the following query:

Pr[<= M](<> error) <= b,

where M is the time bound on the simulations and b is a very low probability.

The global SMC analysis can be enabled by instantiating all the processes in the system. Given the sample system, one need to uncomment 
the lines in the section "Processes-->Global analysis" of System declarations.

For latest news, helpful tips, answers to frequently asked questions, and other support, visit the page at the website:

http://ulrik.blog.aau.dk/schedulability/


*********************************** Models ***********************************

PartitionSupply		- The ARINC-653 compliant partition scheduler on a fixed cyclic basis.

TaskScheduler		- The ARINC-653 compliant task scheduler based on the preemptive fixed priority policy.

PeriodicTask		- The periodic task model.

SporadicTask		- The sporadic task model.

IPTx			- The IP layer model in the sending direction.

IPRx			- The IP layer model in the receiving direction.

VLinkTx			- The model of a virtual link in a transmitting end system.

VLinkRx			- The model of a virtual link in its reception network.

PMsgSender		- The message interface for periodic messages that originate from a perioidc task.

PMsgReceiver		- The test automaton for a PMsgSender to check the existence of the timed selection simulation relation.

SMsgSender		- The message interface for sporadic messages that originate from a sporadic task.

SMsgReceiver		- The test automaton for a SMsgSender to check the existence of the timed selection simulation relation.

*****************************************************************************