江苏大学学报（自然科学版）
江囌大學學報（自然科學版）
강소대학학보（자연과학판）
JOURNAL OF JIANGSU UNIVERSITY(NATURAL SCIENCE EDITION)
2013年
5期
548-555
,共8页
代飞%王黎霞%谢仲文%张璇%朱锐
代飛%王黎霞%謝仲文%張璇%硃銳
대비%왕려하%사중문%장선%주예
软件过程验证%行为验证%代数推导%Petri网%ACP%公理系统
軟件過程驗證%行為驗證%代數推導%Petri網%ACP%公理繫統
연건과정험증%행위험증%대수추도%Petri망%ACP%공리계통
software process verification%behavior verification%algebraic reasoning%Petri Nets%ACP%axiom system
针对现有软件过程验证主要以结构验证和性质验证为主,缺乏行为验证的不足,提出了一种验证软件演化过程行为的代数方法.该方法使用通信进程代数ACP对软件演化过程元模型EPMM进行扩展,提出软件演化过程元模型代数EPMM-A.针对EPMM建模产生的软件演化过程模型,一方面使用EPMM-A形式定义软件演化过程模型的行为规约,另一方面在其公理系统的支持下,基于等式推导验证软件演化过程模型的行为与行为规约是否一致,使行为验证方式从模型推导(非形式化)变为代数推导(形式化).为了说明代数推导的正确性,证明了软件演化过程元模型代数的公理系统具有可靠性.
針對現有軟件過程驗證主要以結構驗證和性質驗證為主,缺乏行為驗證的不足,提齣瞭一種驗證軟件縯化過程行為的代數方法.該方法使用通信進程代數ACP對軟件縯化過程元模型EPMM進行擴展,提齣軟件縯化過程元模型代數EPMM-A.針對EPMM建模產生的軟件縯化過程模型,一方麵使用EPMM-A形式定義軟件縯化過程模型的行為規約,另一方麵在其公理繫統的支持下,基于等式推導驗證軟件縯化過程模型的行為與行為規約是否一緻,使行為驗證方式從模型推導(非形式化)變為代數推導(形式化).為瞭說明代數推導的正確性,證明瞭軟件縯化過程元模型代數的公理繫統具有可靠性.
침대현유연건과정험증주요이결구험증화성질험증위주,결핍행위험증적불족,제출료일충험증연건연화과정행위적대수방법.해방법사용통신진정대수ACP대연건연화과정원모형EPMM진행확전,제출연건연화과정원모형대수EPMM-A.침대EPMM건모산생적연건연화과정모형,일방면사용EPMM-A형식정의연건연화과정모형적행위규약,령일방면재기공리계통적지지하,기우등식추도험증연건연화과정모형적행위여행위규약시부일치,사행위험증방식종모형추도(비형식화)변위대수추도(형식화).위료설명대수추도적정학성,증명료연건연화과정원모형대수적공리계통구유가고성.
