青岛农业大学学报（自然科学版）
青島農業大學學報（自然科學版）
청도농업대학학보（자연과학판）
Journal of Qingdao Agricultural University（Ziran Kexueban)
2015年
3期
228-234
,共7页
形式化模型%集成方法%元模型
形式化模型%集成方法%元模型
형식화모형%집성방법%원모형
formal model%integration method%meta model
MARTE为实时嵌入式软件的构造提供了基础,为了克服MARTE缺乏精确的语义、无法有效地分析、验证软件系统模型的问题,结合Object-Z和PTA在形式化建模中的优点,提出一种集成的形式化方法,该集成模型PTA-OZ能够分别对软件系统的静态结构和动态语义进行验证和分析.在MDA架构下,基于XMI建立了MARTE模型和集成模型之间静态结构的转换框架.最后,通过实例分析了MARTE模型和PTA-OZ模型之间的转换.结果表明,该方法有利于实现图形化模型和形式化模型之间的转换,便于软件开发人员的使用.
MARTE為實時嵌入式軟件的構造提供瞭基礎,為瞭剋服MARTE缺乏精確的語義、無法有效地分析、驗證軟件繫統模型的問題,結閤Object-Z和PTA在形式化建模中的優點,提齣一種集成的形式化方法,該集成模型PTA-OZ能夠分彆對軟件繫統的靜態結構和動態語義進行驗證和分析.在MDA架構下,基于XMI建立瞭MARTE模型和集成模型之間靜態結構的轉換框架.最後,通過實例分析瞭MARTE模型和PTA-OZ模型之間的轉換.結果錶明,該方法有利于實現圖形化模型和形式化模型之間的轉換,便于軟件開髮人員的使用.
MARTE위실시감입식연건적구조제공료기출,위료극복MARTE결핍정학적어의、무법유효지분석、험증연건계통모형적문제,결합Object-Z화PTA재형식화건모중적우점,제출일충집성적형식화방법,해집성모형PTA-OZ능구분별대연건계통적정태결구화동태어의진행험증화분석.재MDA가구하,기우XMI건립료MARTE모형화집성모형지간정태결구적전환광가.최후,통과실례분석료MARTE모형화PTA-OZ모형지간적전환.결과표명,해방법유리우실현도형화모형화형식화모형지간적전환,편우연건개발인원적사용.
