| 一种面向嵌入式软件体系结构的形式化建模方法 |
| |
| 引用本文： | 许海洋,庄毅,顾晶晶.一种面向嵌入式软件体系结构的形式化建模方法[J].电子学报,2014,42(8):1515-1521. |
| |
| 作者姓名： | 许海洋 庄毅 顾晶晶 |
| |
| 作者单位： | 1. 南京航空航天大学计算机科学与技术学院, 江苏南京 210016;
2. 青岛农业大学理学与信息科学学院, 山东青岛 266109 |
| |
| 基金项目： | 国家自然科学基金青年科学基金，国家博士后基金，江苏省普通高校研究生科研创新计划，南京航空航天大学基本科研业务费 |
| |
| 摘 要： | 为了解决MARTE（Modeling and Analysis of Real Time and Embedded systems）在建立嵌入式软件模型时不够精确的问题，结合Object-Z和PTA（Probabilistic Timed Automation）的优点，本文提出了一种集成的形式化建模方法--PTA-OZ.该方法不仅能够对嵌入式软件模型的静态语义和动态语义进行精确描述，而且通过模型转换规则，能够将MARTE模型转换为PTA-OZ模型.并对模型转换的语义一致性进行了验证，证明本文方法在转换过程能够保持结构语义和行为语义的一致性.最后通过实例模型描述从嵌入式软件建模到属性检验的过程.
|
| 关 键 词： | 集成模型 模型转换 概率时间自动机 语义一致性 |
| 收稿时间： | 2013-05-17 |
A Formal Modeling Method for Embedded Software Architecture |
| |
| 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. |
| |
| Authors: | XU Hai-yang ZHUANG Yi GU Jing-jing |
| |
| Affiliation: | 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 |
| |
| Abstract: | |
| |
| Keywords: | integrating model model transformation probabilistic timed automation semantic consistency |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《电子学报》浏览原始摘要信息 |
|
点击此处可从《电子学报》下载全文 |
