电子学报 ›› 2014, Vol. 42 ›› Issue (8): 1515-1521.DOI: 10.3969/j.issn.0372-2112.2014.08.009

• 学术论文 • 上一篇    下一篇

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

许海洋1,2, 庄毅1, 顾晶晶1   

  1. 1. 南京航空航天大学计算机科学与技术学院, 江苏南京 210016;
    2. 青岛农业大学理学与信息科学学院, 山东青岛 266109
  • 收稿日期:2013-05-17 修回日期:2013-12-12 出版日期:2014-08-25 发布日期:2014-08-25
  • 通讯作者: 庄毅
  • 作者简介:许海洋男,1981年生于山东威海.博士生,讲师,主要从事形式化建模、模型检测等方面的研究工作.E-mail:xhy@nuaa.edu.cn
  • 基金资助:

    国家自然科学基金青年科学基金(No.61202351);国家博士后基金(No.2011M500124);江苏省普通高校研究生科研创新计划(No.CXLX12_0161);南京航空航天大学基本科研业务费(No.NS2012133)

A Formal Modeling Method for Embedded Software Architecture

XU Hai-yang1,2, ZHUANG Yi1, GU Jing-jing1   

  1. 1. College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, Jiangsu 210016, China;
    2. College of Science and Information, Qingdao Agricultural University, Qingdao, Shandong 266109, China
  • Received:2013-05-17 Revised:2013-12-12 Online:2014-08-25 Published:2014-08-25

摘要:

为了解决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.

Key words: integrating model, model transformation, probabilistic timed automation, semantic consistency

中图分类号: