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

doi:10.3969/j.issn.0372-2112.2014.08.009

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

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

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

1. 南京航空航天大学计算机科学与技术学院, 江苏南京 210016;
2. 青岛农业大学理学与信息科学学院, 山东青岛 266109

收稿日期:2013-05-17 修回日期:2013-12-12 出版日期: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-yang^1,2, ZHUANG Yi¹, GU Jing-jing¹

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
- Supported by:
- 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)

摘要/Abstract

摘要：

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

中图分类号:

TP301

许海洋, 庄毅, 顾晶晶. 一种面向嵌入式软件体系结构的形式化建模方法[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.

参考文献

[1] Mallet F,André C.On the semantics of UML/MARTE clock constraints[A].IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing[C].Tokyo:IEEE Computer Society,2009.305-312.
[2] André C,Mallet F.Specification and verification of time requirements with CCSL and Esterel[J].ACM SIGPLAN Notices.2009,44(7):167-176.
[3] 于苏东,刘雷波,尹首一,等.嵌入式粗颗粒度可重构处理器的软硬件协同设计流程[J].电子学报，2009,37(5):1136-1140. Yu Sudong,Liu Leibo,Yin Shouyi,et al.Hardware-software Co-Design flow for embedded coarse-grained reconfigurable processer[J].Acta Electronica Sinica,2009,37(5):1136-1140.(in Chinese)
[4] Mallet F.Clock constraint specification language:specifying clock constraints with UML/MARTE[J].Innovations in Systems and Software Engineering.2008,4(3):309-314.
[5] Mallet F,De Simone R.MARTE:A profile for RTE systems modeling,analysis and simulation[A].Proceedings of the 1st International Conference on Simulation Tools and Techniques for Communications,Networks and Systems & Workshops[C].Marseille:ACM Press,2008.1-8.
[6] Woodcock J,Larsen P G,Bicarregui J,et al.Formal methods:Practice and experience[J].ACM Computing Surveys,2009,41(4):1-40.
[7] Quadri I R,Gamatié A,Boulet P,et al.Expressing embedded systems configurations at high abstraction levels with UML MARTE profile:advantages,limitations and alternatives[J].Journal of Systems Architecture.2012,58(5):178-194.
[8] Didier A,Farias A,Mota A.Checking Z data refinements using traces refinement[A].Proceedings of the Eleventh Brazilian Symposium on Formal Methods[C].Amsterdam:Elsevier,2009.129-148.
[9] Derrick J,North S,Simons A J H.Z2SAL-Building a Model Checker for Z[A].Abstract State Machines,B and Z[C].Berlin:Springer-Verlag,2008.280-293.
[10] Rasch H,Wehrheim H.Checking consistency in UML diagrams:classes and state machines[A].Formal Methods for open,Object-based Distributed Systems[C].Berlin:Springer-Verlag,2003.229-243.
[11] Rasch H,Wehrheim H.Checking the validity of scenarios in UML models[A].Formal methods for open,object-based distributed systems[C].Berlin:Springer-Verlag,2005.67-82.
[12] Knapp A,Merz S,Rauh C.Model checking timed UML state machines and collaborations[A].Formal Techniques in Real-Time and Fault-Tolerant Systems[C].Berlin:Springer-Verlag,2002.395-414.
[13] Mller M,Olderog E R,Rasch H,et al.Integrating a formal method into a software engineering process with UML and Java[J].Formal Aspects of Computing,2008,20(2):161-204.
[14] Basin D,Olderog E R,Sevinc P E.Specifying and analyzing security automata using CSP-OZ[A].Proceedings of the 2nd ACM Symposium on Information,Computer and Communications Security[C].New York:ACM Press,2007.70-81.
[15] 朱敏,李必信,陈乔乔,等.基于微分动态逻辑的CPS建模与属性验证[J].电子学报,2012,40(6):1126-1132. Zhu Min,Li Bixin,Chen Qiaoqiao,et al.Transforming hybrid UML to hybrid program for CPS property verification[J].Acta Electronica Sinica,2012,40(6):1126-1132.(in Chinese)
[16] Gotlieb A.TCAS software verification using constraint programming[J].The Knowledge Engineering Review,2012,27(3):343-360.
[17] Kwiatkowska M,Norman G,Segala R,et al.Automatic verification of real-time systems with discrete probability distributions[J].Theoretical Computer Science,2002,282(1):101-150.
[18] Duke R,Rose G,Smith G.Object-Z:A specification language advocated for the description of standards[J].Computer Standards & Interfaces,1995,17(5):511-533.
[19] Kim S K,Carrington D.A formal metamodeling approach to a transformation between the UML state machine and Object-Z[A].Formal Methods and Software Engineering[C].Berlin:Springer-Verlag,2002.548-560.
[20] Kim S K,Burger D,Carrington D.An MDA approach towards integrating formal and informal modeling languages[A].Formal Method[C].Berlin:Springer-Verlag,2005.448-464.
[21] Huzar Z,Kuzniarz L,Reggio G,et al.Consistency problems in UML-based doftware development[A].UML Modeling Languages and Applications[C].Berlin:Springer-Verlag,2005.1-12.
[22] Varró D.Automated formal verification of visual modeling languages by model checking[J].Software and Systems Modeling.2004,3(2):85-113.
[23] 万勇兵,徐中伟,梅萌.一种符号化执行的实时系统一致性测试生成方法[J].电子学报,2013,41(11):2276-2284. Wan Yongbing,Xu Zhongwei,Mei Meng.A symbolic execution method for confromance test generation of real-time system[J].Acta Electronica Sinica,2013,41(11):2276-2284.(in Chinese)
[24] Giese H,Lambers L.Towards automatic verification of behavior preservation for model transformation via invariant checking[A].Graph Transformations[C].Berlin:Springer-Verlag,2012.249-263.

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

A Formal Modeling Method for Embedded Software Architecture

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 2

编辑推荐

Metrics

[1]	吴文李, 范小朋, 周庚申, 黄羿, 曹旸, 林桂婵. 基于集成模型的BOM近似度量方法[J]. 电子学报, 2019, 47(5): 1023-1028.
[2]	朱敏, 李必信, 陈乔乔, 吉顺慧, 李加凯. 基于微分动态逻辑的CPS建模与属性验证[J]. 电子学报, 2012, 40(6): 1126-1132.