Schedulability verification of AADL model based on UPPAAL
基于UPPAAL的AADL模型可调度性验证

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 pre...