Analysis and Verification of Local Properties of Ada Tasking Based on Net Language
基于网语言的Ada程序局部性质的分析和验证

In this paper, the properties of Ada tasking and the correlative state explosion problem are discussed by using the net language. The synchronous composition and decomposition of Ada net is studied, as a result, net language properties are obtained, and the safeness and liveness properties of Ada tasking by using the Ada net language are analyzed and verified, which provide a new and useful way for analyzing and verifying the complex Ada tasking.