Using CPAL to model and validate the timing behaviour of embedded systems

This work presents a solution to the Formal Methods for Timing Verification (FMTV) Challenge 2015 using CPAL. CPAL stands for the Cyber-Physical Action Language and is a novel language to model, simulate and verify cyber-physical systems as those described in the challenge. We believe that the complexity of the challenge mainly stems from the complex interactions of the tasks and processes composing the aerial video tracking system of the challenge. Using CPAL we have derived a complete and unambiguous description of the system that supports timing verification. The different sub-challenges were solved by timing-accurate simulation and/or schedulability analysis. Even though simulation does not provide firm guarantees on the worst-case behaviour, it helps the system designer solve scheduling problems and validate the solutions, where verification tools can not be applied directly due to the complexity of the model as in the 2015 FMTV challenge.