Modelling the behaviour of Ada tasks and verifying its safety

This paper models the behavior of Ada tasks with Petri nets according to the semantics and the syntax of them, and this net is called an Ada net. Moreover our Ada net can improve the rendezvous model proposed by the S.M. Shatz as well as describing the task type. At the same time, we present the semantics and the syntax of computation tree logic with the transition relations of the Ada net´s transition system, and provide an approach to model check the safety not upon the transition system, but rather directly upon the Ada net. At the end of this paper, a prototype system under this approach is implemented, and our experimental results demonstrate that the complexity of model checking with computation tree logic is polynomial.