小型微型计算机系统
小型微型計算機繫統
소형미형계산궤계통
MINI-MICRO SYSTEMS
2013年
7期
1468-1473
,共6页
陈曙%毋国庆%叶俊民%陈明楷
陳曙%毌國慶%葉俊民%陳明楷
진서%무국경%협준민%진명해
需求分析%多视点%软件行为%模型验证
需求分析%多視點%軟件行為%模型驗證
수구분석%다시점%연건행위%모형험증
software requirement%muliti view point%software behavior%model checking
软件需求分析是软件开发生命周期中最重要的步骤之一.模型驱动的需求分析方法将需求模型作为需求规格说明的补充,从一个或多个角度对非形式化的需求信息进行正确性验证以发现需求规格中的不一致和不完整性等.本文在一种新型的,基于软件行为和多视点的需求建模方法基础上,依据其构造特点,提出需求模型的分析以及验证方法.该方法主要通过构造模型待验证性质的行为时序逻辑规约,以需求模型对应的有穷状态迁移系统为基础,结合On-The-Fly的方法验证性质规约是否语义满足该状态迁移系统.此外,从命题抽象的角度对该验证方法进行优化.针对该方法实现了模型验证工具原型.
軟件需求分析是軟件開髮生命週期中最重要的步驟之一.模型驅動的需求分析方法將需求模型作為需求規格說明的補充,從一箇或多箇角度對非形式化的需求信息進行正確性驗證以髮現需求規格中的不一緻和不完整性等.本文在一種新型的,基于軟件行為和多視點的需求建模方法基礎上,依據其構造特點,提齣需求模型的分析以及驗證方法.該方法主要通過構造模型待驗證性質的行為時序邏輯規約,以需求模型對應的有窮狀態遷移繫統為基礎,結閤On-The-Fly的方法驗證性質規約是否語義滿足該狀態遷移繫統.此外,從命題抽象的角度對該驗證方法進行優化.針對該方法實現瞭模型驗證工具原型.
연건수구분석시연건개발생명주기중최중요적보취지일.모형구동적수구분석방법장수구모형작위수구규격설명적보충,종일개혹다개각도대비형식화적수구신식진행정학성험증이발현수구규격중적불일치화불완정성등.본문재일충신형적,기우연건행위화다시점적수구건모방법기출상,의거기구조특점,제출수구모형적분석이급험증방법.해방법주요통과구조모형대험증성질적행위시서라집규약,이수구모형대응적유궁상태천이계통위기출,결합On-The-Fly적방법험증성질규약시부어의만족해상태천이계통.차외,종명제추상적각도대해험증방법진행우화.침대해방법실현료모형험증공구원형.
