摘要
为了解决MARTE(Modeling and Analysis of Real Time and Embedded systems)在建立嵌入式软件模型时不够精确的问题,结合Object-Z和PTA(Probabilistic Timed Automation)的优点,本文提出了一种集成的形式化建模方法——PTA-OZ.该方法不仅能够对嵌入式软件模型的静态语义和动态语义进行精确描述,而且通过模型转换规则,能够将MARTE模型转换为PTA-OZ模型.并对模型转换的语义一致性进行了验证,证明本文方法在转换过程能够保持结构语义和行为语义的一致性.最后通过实例模型描述从嵌入式软件建模到属性检验的过程.
MARTE is utilized for embedded software modeling. However,it could not provide powerful methods for rigor- ously analyzing the correctness of software systems. This paper introduces the PTA-OZ, which combines the specification language Object-Z with the probabilistic processes PTA. It can provide accurate descriptions for both static and dynamic semantics of embed- ded software models. Additionally, we propose the model transformation rules for converting MARTE models to FFA-OZ models. We verify the semantics preservation in model transformation, proving that the model transformation rules can keep both the struc- tural and behavioral consistency of software. A practical case is demonstrated throughout the processes of software modeling and property verification.
出处
《电子学报》
EI
CAS
CSCD
北大核心
2014年第8期1515-1521,共7页
Acta Electronica Sinica
基金
国家自然科学基金青年科学基金(No.61202351)
国家博士后基金(No.2011M500124)
江苏省普通高校研究生科研创新计划(No.CXLX12-0161)
南京航空航天大学基本科研业务费(No.NS2012133)
关键词
集成模型
模型转换
概率时间自动机
语义一致性
integrating model
model transformation
probabilisfic timed automation
semantic consistency
