计算机科学 ›› 2017, Vol. 44 ›› Issue (11): 240-245.doi: 10.11896/j.issn.1002-137X.2017.11.036

• 第六届全国软件分析测试与演化学术会议 • 上一篇    下一篇

软件模型代数性质的程序化验证

赵会群,黄榆涵   

  1. 北方工业大学计算机学院 北京100144,北方工业大学计算机学院 北京100144
  • 出版日期:2018-12-01 发布日期:2018-12-01
  • 基金资助:
    本文受国家自然科学基金(61370051)资助

Program Verification of Software Model’s Algebraic Properties

ZHAO Hui-qun and HUANG Yu-han   

  • Online:2018-12-01 Published:2018-12-01

摘要: 软件模型代数的思想是通过引入进程代数来对软件体系结构进行建模。它将构件解释为变量,将连接子抽象为代数运算,并针对软件的特性建立了软件体系结构代数模型。在代数模型的基础上,讨论分析获得一系列能指导软件演化的代数性质。但是,上述研究都只对模型的代数性质进行了理论证明,实际上并无程序能够证明这些代数性质的正确性,同时也未给出这些性质的应用方法,使其缺乏可操作性。采用程序化验证的方法对代数性质进行了验证,并对这些性质的应用算法进行了研究,进一步丰富了软件的建模理论,也使得软件演化从理论研究转化为实际应用成为可能。

关键词: 代数模型,代数性质,程序化验证,软件演化

Abstract: Software model algebra is introduced to model software architecture by process algebra.It explains components as variables,abstracts connector as algebra operation,and builds the algebraic model of software architecture according to software features.Based on the discussion about algebraic model,we got a series of algebraic properties to guide software evolution.However,these studies have only theoretically proved the algebraic properties of the mode,no program can actually prove the correctness of these algebraic properties,and they did not give the property applications,making them lack maneuverability.This paper researched the algebraic properties of algorithms,did program verification,further enriched the software model,and also made it possible to change software evolution from theory into practical applications.

Key words: Algebraic model,Algebraic property,Program verification,Software evolution

[1] GAO H,ZHANG L,FAN Z Q.Software architecture description technique based on template[J].Jounal of Beijing University of Aeronautics and Astronautics,2008,4(1):122-126.(in Chinese) 高晖,张莉,樊志强.基于模板的软件体系结构描述技术[J].北京航空航天大学学报,2008,4(1):122-126.
[2] ZHU X Y.Study on Formal Deseription of Sotfware Architecture[D].Beijing:Graduate University of Chinese Academy of Sciences,2005.(in Chinese) 朱雪阳.软件体系结构形式描述研究[D].北京:中国科学院研究生院(软件研究所),2005.
[3] HUANG Z B,ZHANG G Q.A New Method about the Description of Software Architecture[J].Microelectronics & Computer,2006,23(12):82-84,88.(in Chinese) 黄正宝,张广泉.一种新型的软件体系结构描述方法研究[J].微电子学与计算机,2006,23(12):82-84,88.
[4] YUAN B,WANG B Q.Algebraic Model of Reconfigurable System Based on Component Operation[J].Journal of Software,2012,23(10):2735-2745.(in Chinese) 袁博,汪斌强.基于构件运算的可重构系统代数模型[J].软件学报,2012,3(10):2735-2745.
[5] ZHANG Y S.Study on Methods for Description of Software Architecture and Software Evolution Based on Algebra Theory[D].Changsha:Central South University,2007.(in Chinese) 张友生.基于代数理论的软件体系结构描述及软件演化方法研究[D].长沙:中南大学,2007.
[6] DAI F,LI T,XIE Z W,et al.Towards an Algebraic Semantics of Software Evolution Process Models[J].Journal of Software,2012,23(4):846-863.(in Chinese) 代飞,李彤,谢仲文,等.一种软件演化过程模型的代数语义[J].软件学报,2012,23(4):846-863.
[7] ZHAO H Q,SUN J.An algebraic model of Internetware software architecture[J].Chinese Science:Information Science,2013,43(1):161-177.(in Chinese) 赵会群,孙晶.网构软件体系结构代数模型[J].中国科学:信息科学,2013,3(1):161-177.
[8] ZHAO H Q,SUN J.An Algebraic Model of Service Oriented Trust worthy Software Architecture[J].Chinese Journal of Computers,2010,3(5):890-899.(in Chinese) 赵会群,孙晶.面向服务的可信软件体系结构代数模型[J].计算机学报,2010,3(5):890-899.
[9] ALVES A,ARKIN A,ASKARY S,et al.Web services business process execution language version 2.0[EB/OL].(2007-04-11)[2012-08-19].http://docs.oasis-open.org/wsbpel/2.0/OS/ wsbpel-v2.0-OS.html.
[10] SUN J,LI D F.Study of algorithm on evolution for BPEL structure[J].Application Research of Computer,2016,33(9):1-6.(in Chinese) 孙晶,李东方.一种BPEL结构演化算法研究[J].计算机应用研究,2016,33(9):1-6.
[11] ZHAO H Q,YIN C R.Research of model checking method and technology guided by testing purpose[J].Application Research of Computer,2015,2(8):2387-2390,2394.(in Chinese) 赵会群,殷朝冉.测试目的引导的模型检测方法与技术研究[J].计算机应用研究,2015,32(8):2387-2390,4.

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] 雷丽晖,王静. 可能性测度下的LTL模型检测并行化研究[J]. 计算机科学, 2018, 45(4): 71 -75, 88 .
[2] 夏庆勋,庄毅. 一种基于局部性原理的远程验证机制[J]. 计算机科学, 2018, 45(4): 148 -151, 162 .
[3] 厉柏伸,李领治,孙涌,朱艳琴. 基于伪梯度提升决策树的内网防御算法[J]. 计算机科学, 2018, 45(4): 157 -162 .
[4] 王欢,张云峰,张艳. 一种基于CFDs规则的修复序列快速判定方法[J]. 计算机科学, 2018, 45(3): 311 -316 .
[5] 孙启,金燕,何琨,徐凌轩. 用于求解混合车辆路径问题的混合进化算法[J]. 计算机科学, 2018, 45(4): 76 -82 .
[6] 张佳男,肖鸣宇. 带权混合支配问题的近似算法研究[J]. 计算机科学, 2018, 45(4): 83 -88 .
[7] 伍建辉,黄中祥,李武,吴健辉,彭鑫,张生. 城市道路建设时序决策的鲁棒优化[J]. 计算机科学, 2018, 45(4): 89 -93 .
[8] 刘琴. 计算机取证过程中基于约束的数据质量问题研究[J]. 计算机科学, 2018, 45(4): 169 -172 .
[9] 钟菲,杨斌. 基于主成分分析网络的车牌检测方法[J]. 计算机科学, 2018, 45(3): 268 -273 .
[10] 史雯隽,武继刚,罗裕春. 针对移动云计算任务迁移的快速高效调度算法[J]. 计算机科学, 2018, 45(4): 94 -99, 116 .