Schedulability verification of AADL model based on UPPAAL
Luo Lei · Journal of Computer Applications · 2009
A formal analytical and verification method was proposed to solve the schedulability problem of Architecture Analysis and Design Language(AADL) model.It used model checker UPPAAL to model external environment and to verify AADL thread component's schedulability under non-preempt dispatch strategy.Moreover,a tool for model's translation from AADL to UPPAAL was implemented.Experiment demonstrates that analyzing and verifying the schedulability of AADL models by UPPAAL is feasible.This method produces more precise results than other informal verification method.