CAJ | 학술논문

采用时间自动机形式化模型检验方法建立了结构分析与设计语言（AADL）调度模型的自动机，实现了从 AADL 模型到时间自动机模型的自动转换与验证。首先，设计了周期、非周期的线程时间自动机模板及抢占、非可抢占的调度器时间自动机模板，建立了 AADL 调度模型到时间自动机模型的语义映射法则。然后，设计了自动化模型转换插件，并将其集成到 OSATE 建模工具中，实现了建模、转换、验证的集成开发环境。最后，利用 UPPAAL 工具对时间自动机模型进行模拟与验证。仿真实验结果表明，所建立的模型转换方法能够有效、实时地将 AADL 模型转换为时间自动机模型，并可在 UPPAAL 中分析原模型的可调度性。
채용시간자동궤형식화모형검험방법건립료결구분석여설계어언（AADL）조도모형적자동궤，실현료종 AADL 모형도시간자동궤모형적자동전환여험증。수선，설계료주기、비주기적선정시간자동궤모판급창점、비가창점적조도기시간자동궤모판，건립료 AADL 조도모형도시간자동궤모형적어의영사법칙。연후，설계료자동화모형전환삽건，병장기집성도 OSATE 건모공구중，실현료건모、전환、험증적집성개발배경。최후，이용 UPPAAL 공구대시간자동궤모형진행모의여험증。방진실험결과표명，소건립적모형전환방법능구유효、실시지장 AADL 모형전환위시간자동궤모형，병가재 UPPAAL 중분석원모형적가조도성。
Automaton of the architecture analysis and design language (AADL)scheduling model is established by using the time automaton formal model checking method to realize automatic conver-sion from the AADL model to the time automaton model and the corresponding verification.First, periodic and aperiodic thread timed automata templates as well as preemptive and non-preemptive scheduler timed automata templates are designed.The mapping semantic from the AADL scheduling model to the timed automata model is put forward.Then,an plug-in of automatic transformation is developed and integrated into the modeling tool—open source AADL tool environment (OSATE) which implements integrated development environment for modeling,transformation and verifica-tion.Finally,the time automaton is simulated and verified in UPPAAL.The simulation results show that the proposed model can efficiently transform the AADL model into the time automaton model in real-time and the schedulability of the original model can be analyzed in UPPAAL.