Computer Science ›› 2017, Vol. 44 ›› Issue (11): 240-245.doi: 10.11896/j.issn.1002-137X.2017.11.036

Previous Articles     Next Articles

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   
No Suggested Reading articles found!