| 摘要: |
| 旨在研究利用网语言讨论Ada程序性质和由此而引起的Ada网的状态爆炸问题.研究了Ada网的同步合成与分解,讨论了它们的语言性质,并利用这一结果分析和验证了Ada程序的安全性和活性,从而为复杂的Ada程序的分析与验证提供了一个新的有效途经. |
| 关键词: Ada网 同步合成 同步分解 网语言 分析 验证 |
| DOI： |
| 分类号: |
| 基金项目:国家自然科学基金资助项目(69973029;69933020);国家高技术研究发展计划资助项目(2001AA413020);国家重点基础研究发展规划973资助项目(G1998030604);国家杰出青年科学基金资助项目(60125205);教育部优秀青年教师教学科研奖励计划资助项目;全国优秀博士论文作者专项基金资助项目(199934);上海市科技发展计划重点基础研究基金资助项目(02DJ14064) |
|
| Analysis and Verification of Local Properties of Ada Tasking Based on Net Language |
|
DING Zhi-jun,JIANG Chang-jun
|
| Abstract: |
| 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. |
| Key words: Ada net synchronous composition synchronous decomposition net language analysis verification |
