SDL规范性能自动分析

Automatic Analysis of SDL Specification

重点阐述 SDL 规范性能的自动分析.分两个步骤,首先将 SDL 规范映射到等价的 Petri 网模型,再对 Petri 网模型进行分析(可达性分析和线性不变式分析).分析工作与转换工作由工具 SDLPN 自动完成.

This paper lays emphasis on the description of analysis method for SDL specifica- tions.Two steps are included in the method.First,We map SDL sepcification onto Petri net model.Then,we analyze this Petri net model(reachability analysis and invariants analysis). The work of mapping SDL onto Petri net and the subsequent analysis is done by the support- ing tool SDLPN automatically.