一种Ada并发程序的模型检测方法

摘要

A model extraction method for Ada concurrent programs is proposed.The model checker SPIN is used to validate the model generated automatically,and it is found that concurrent errors such as deadlock exist in programs written with Ada language.Finally,the extraction method is verified through examples.The experimental results show that this method can successfully detect errors existing in Ada concurrent programs,and give the corresponding error path.%提出了一种针对Ada并发程序的模型提取方法,使用模型检测工具SPIN对生成的模型进行自动化验证,发现Ada语言编写的程序中并发错误。通过实例对提取方法进行验证,实验结果表明,此方法能够成功检测出Ada并发程序中存在的错误,并给出相应的错误路径。