摘要
针对目前航空运输系统中对飞机着陆调度成本效益研究的不足,提出采用价格时间自动机作为形式化描述方法,将飞机着陆过程建模为其相关实体的交互行为,引入时间和价格因素描述各实体的属性和行为,从而将飞机着陆形式化为时间价格的动态交互协作,并分别为相关实体和服务建模,形成彼此独立又相互协作的价格时间自动机网络,将飞机着陆调度成本表示为价格时间自动机网络上的状态转换路径。最后提出一组系统模型需要满足的性质,使用价格时间自动机模拟验证工具UPPAAL CORA仿真并验证其正确性,使用最优成本标准分支算法分析求解飞机着陆调度最优成本的可达性。
For the lack of studies of aircraft landing scheduling(ALS) cost in the field of air transport system currently,this paper develops a method using priced timed automata(PTA) to model the aircraft landing process in which time and price are used to describe the properties and behavior of each entity.The entities and service of ALS are both collaborative and independent of each other.ALS cost is expressed as the state transition path of PTA.Lastly,we present properties that the model should be satisfied with,which are simulated and verified using the model checking tool UPPAAL CORA.The reachability of ALS optimal cost is got by using standard branch and bound algorithm.
出处
《济南大学学报(自然科学版)》
CAS
北大核心
2013年第2期150-153,共4页
Journal of University of Jinan(Science and Technology)
基金
河南省科技攻关计划(122102210518)
关键词
价格时间自动机
最优成本
可达性
飞机着陆
priced timed automata
optimal cost
reachability
aircraft landing