AUTOMATIC VERIFICATION OF TIMING CONSTRAINTS FOR SAFETY CRITICAL SPACE SYSTEMS

摘要

In this paper is presented an automatic process of verification.rnWe focus in the verification of scheduling analysisrnparameter. This proposal is part of process based onrnModel Driven Engineering to automate a Verification andrnValidation process of the software on board of satellites.rnThis process is implemented in a software control unitrnof the energy particle detector which is payload of SolarrnOrbiter mission. From the design model is generatedrna scheduling analysis model and its verification model.rnThe verification as defined as constraints in way of FiniternTimed Automatas. When the system is deployed on targetrnthe verification evidence is extracted as instrumentedrnpoints. The constraints are fed with the evidence, if anyrnof the constraints is not satisfied for the on target evidencernthe scheduling analysis is not valid.