A Formal Modeling Method for Embedded Software Architecture

XU Hai-yang; ZHUANG Yi; GU Jing-jing

doi:10.3969/j.issn.0372-2112.2014.08.009

您当前的位置：

首页 >

文章列表页 >

A Formal Modeling Method for Embedded Software Architecture

更新时间：2025-07-16

- A Formal Modeling Method for Embedded Software Architecture
- Acta Electronica Sinica Vol. 42, Issue 8, Pages: 1515-1521(2014)
- 作者机构：
  
  1. 南京航空航天大学计算机科学与技术学院,江苏,南京,210016
  2. 青岛农业大学理学与信息科学学院,山东,青岛,266109
  3. 南京航空航天大学计算机科学与技术学院,江苏,南京,210016
  4. 青岛农业大学理学与信息科学学院,山东,青岛,266109
- 作者简介：
- 基金信息：
  
  Youth Fund of National Natural Science Foundation of China (No.61202351);Post-doctoral Fund of China (No.2011M500124);Graduate Research Innovation Program of univerities in Jiangsu Province (No.CXLX12_0161);Fundamental Research Funds for Nanjing University of Aeronautics and Astronautics (No.NS2012133)
- DOI：10.3969/j.issn.0372-2112.2014.08.009
  CLC： TP301
- Published：2014
- 稿件说明：
移动端阅览
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：

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

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Transforming HybridUML to Hybrid Program for CPS Property Verification

Related Author

ZHU Min

LI Bi-xin

CHEN Qiao-qiao

JI Shun-hui

LI Jia-kai

Related Institution

School of Computer Science and Engineering, Southeast University

⁰