A Model Checking Method for Ada Concurrent Program
Jiang Guohua · Electronic Science and Technology · 2012
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.