一种面向嵌入式软件体系结构的形式化建模方法

许海洋; 庄毅; 顾晶晶

doi:10.3969/j.issn.0372-2112.2014.08.009

您当前的位置：

首页 >

文章列表页 >

一种面向嵌入式软件体系结构的形式化建模方法

学术论文 | 更新时间：2025-07-16

- 一种面向嵌入式软件体系结构的形式化建模方法
- A Formal Modeling Method for Embedded Software Architecture
- 电子学报 2014年42卷第8期页码：1515-1521
- 作者机构：
  
  1. 南京航空航天大学计算机科学与技术学院,江苏,南京,210016
  2. 青岛农业大学理学与信息科学学院,山东,青岛,266109
  3. 南京航空航天大学计算机科学与技术学院,江苏,南京,210016
  4. 青岛农业大学理学与信息科学学院,山东,青岛,266109
- 作者简介：
- 基金信息：
  
  国家自然科学基金青年科学基金 (No.61202351）;国家博士后基金 (No.2011M500124）;江苏省普通高校研究生科研创新计划 (No.CXLX12_0161）;南京航空航天大学基本科研业务费 (No.NS2012133）
- DOI：10.3969/j.issn.0372-2112.2014.08.009
  中图分类号： TP301
- 纸质出版：2014
- 稿件说明：
移动端阅览
许海洋, 庄毅, 顾晶晶. 一种面向嵌入式软件体系结构的形式化建模方法[J]. 电子学报, 2014,42(8):1515-1521.

XU Hai-yang, ZHUANG Yi, GU Jing-jing. A Formal Modeling Method for Embedded Software Architecture[J]. Acta Electronica Sinica, 2014, 42(8): 1515-1521.
许海洋, 庄毅, 顾晶晶. 一种面向嵌入式软件体系结构的形式化建模方法[J]. 电子学报, 2014,42(8):1515-1521. DOI： 10.3969/j.issn.0372-2112.2014.08.009.

XU Hai-yang, ZHUANG Yi, GU Jing-jing. A Formal Modeling Method for Embedded Software Architecture[J]. Acta Electronica Sinica, 2014, 42(8): 1515-1521. DOI： 10.3969/j.issn.0372-2112.2014.08.009.

摘要

为了解决MARTE（Modeling and Analysis of Real Time and Embedded systems）在建立嵌入式软件模型时不够精确的问题，结合Object-Z和PTA（Probabilistic Timed Automation）的优点，本文提出了一种集成的形式化建模方法PTA-OZ.该方法不仅能够对嵌入式软件模型的静态语义和动态语义进行精确描述，而且通过模型转换规则，能够将MARTE模型转换为PTA-OZ模型.并对模型转换的语义一致性进行了验证，证明本文方法在转换过程能够保持结构语义和行为语义的一致性.最后通过实例模型描述从嵌入式软件建模到属性检验的过程.

Abstract

MARTE is utilized for embedded software modeling.However

it could not provide powerful methods for rigorously 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 embedded software models.Additionally

we propose the model transformation rules for converting MARTE models to PTA-OZ models.We verify the semantics preservation in model transformation

proving that the model transformation rules can keep both the structural and behavioral consistency of software.A practical case is demonstrated throughout the processes of software modeling and property verification.

关键词

Keywords

references

浏览量

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于微分动态逻辑的CPS建模与属性验证