基于网语言的Ada程序局部性质的分析和验证  

Analysis and Verification of Local Properties of Ada Tasking Based on Net Language

作　　者：丁志军[1] 蒋昌俊[1,2] 

机构地区：[1]山东科技大学信息科学与工程学院 [2]同济大学计算机科学与工程系,上海200092

出　　处：《软件学报》2002年第12期2305-2316,共12页Journal of Software

基　　金：国家自然科学基金资助项目(69973029;69933020);国家高技术研究发展计划资助项目(2001AA413020);国家重点基础研究发展规划973资助项目(G1998030604);国家杰出青年科学基金资助项目(60125205);教育部优秀青年教师教学科研奖励计划资助项目;全国优秀博士论文作

摘　　要：旨在研究利用网语言讨论Ada程序性质和由此而引起的Ada网的状态爆炸问题.研究了Ada网的同步合成与分解,讨论了它们的语言性质,并利用这一结果分析和验证了Ada程序的安全性和活性,从而为复杂的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.

关 键 词：网语言 ADA程序 局部性质 同步合成 同步分解 分析 验证 ADA语言 并发程序 程序设计 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]