摘要
为了避免飞机在着陆过程中出现事故,同时又能充分利用机场的跑道资源,对飞机数量多于跑道的情况进行了研究,采用了模型验证的方法。介绍了时间自动机的相关理论,以及基于该理论的验证工具uppaal,在此基础上使用uppaal工具对飞机着陆过程构造了模型,然后对模型的需求规范进行了验证,验证结果表明该模型不存在死锁问题,最终可以保证飞机安全和及时地着陆。
To avoid an accident during landing, at the same time make full use of the airport runway resources, the situation that the number of plane is more than runway is studied, model validation method is used.The theory of timed automata and checking tool named uppaal are introduced, on this basis model for landing is constructed by the tool, then specification of model＇s property is checked, so got the conclusion that there is not dead lock in this model and system assure that plane landing is safe and timely.
出处
《计算机工程与设计》
CSCD
北大核心
2009年第23期5521-5523,共3页
Computer Engineering and Design
关键词
实时系统
模型验证
时间自动机
验证工具
控制系统
real-time systems
model checking
time automata
validation tool
control system
