计算机科学 ›› 2015, Vol. 42 ›› Issue (12): 136-142.

• 第十三届全国软件与应用学术会议 • 上一篇    下一篇

问题框架中问题领域因果行为的形式化验证

朱利鲁,李智   

  1. 广西师范大学广西多源信息挖掘与安全重点实验室 桂林541004 广西师范大学广西区域多源信息集成与智能处理协同创新中心 桂林541004,广西师范大学广西多源信息挖掘与安全重点实验室 桂林541004 广西师范大学广西区域多源信息集成与智能处理协同创新中心 桂林541004
  • 出版日期:2018-11-14 发布日期:2018-11-14
  • 基金资助:
    本文受国家自然科学基金(61262004,61262005),广西自然科学基金(2012GXNSFCA053010),广西科学研究与技术开发计划项目(桂科合1347004-22) ,广西教育厅科研项目(201203YB023),广西多源信息挖掘与安全重点实验室开放基金(14-A-03-01),“八桂学者”工程专项经费资助

Formal Validation of Causal Behaviors of Problem Domains in Problem Frames Approach

ZHU Li-lu and LI Zhi   

  • Online:2018-11-14 Published:2018-11-14

摘要: 为问题框架中问题渐变所依赖的问题领域因果行为的确立提出一种形式化验证方法。为了对问题渐变过程中事件间的因果关系提供可验证的证据支持,简化问题表征的复杂度,进而提高计算机领域软件规约的可靠性,采纳了一种基于NuSMV语言的符号模型检验的形式化验证方法。该验证方法采用UML状态机表示问题领域内部状态变化的有限结构空间,用CTL公式描述问题域内状态之间的可达性性质,通过遍历有限结构状态机来检验CTL公式的正确性,筛选出具有因果关系的外部共享事件,为问题渐变提供有效的技术支持。

关键词: 问题框架,关键问题领域,因果行为,符号模型检验,可达性

Abstract: This paper proposed a method of formally identifying and validating causal behaviors of problem domains,which are the basis of problem progression in the problem frames approach.A symbolic model checking method based on the NuSMV language was adopted in order to provide verifiable evidence of causal relationships between events which are useful in problem progression,reduce the complexity of problem representation,and increase the reliability of specifications of the computing machine.A UML state-chart is used to represent the finite space of internal state transitions of a critical domain.A CTL formula is used to describe the reachability of certain internal states of the domain.A series of causally-related events are identified through traversing all the possible paths of state-transition in the state-chart to validate the correctness of the CTL formula,thus providing effective technical support to problem progression.

Key words: Problem frames,Critical problem domain,Causal behavior,Symbolic model checking,Reachability

[1] Jackson M.Software Requirements and Specifications:A Lexicon of Practice,Principles and Prejudices[M].Reading:Addison-Wesley,1995
[2] Jackson M.Problem Frames:Analyzing and Structuring Software Development Problems[M].Boston:Addison-Wesley,2001
[3] 李智,金芝.从用户需求到软件规约:一种问题变换的方法[J].软件学报,2013,4(5):961-976 Li Z,Jin Z.From user requirements to software specifications:An approach based on problem transformation[J].Journal of Software,2013,4(5):961-976
[4] 杨军,葛海通,郑飞君,等.一种形式化验证方法:模型检验[J].浙江大学学报(理学版),2006,33(4):403-407 Yang J,Ge Hai-tong,Zheng Fei-jun,et al.A formal validation method:model checking[J].Journal of Zhejiang University(Natu-ral Science Edition),2006,33(4):403-407
[5] 文静华,余滨,张梅,等.基于SMV的网络协议形式化分析与验证[J].计算机工程,2006,32(15):135-136,145 Wen Jing-Hua,Yu Bin,Zhang Mei,et al.Formal analysis and validation of network protocol based on SMV[J].Journal of Computer Engineering,2006,32(15):135-136,5
[6] Brayant R E.Graph-Based Algorithm for Boolean Function Manipulation[J].IEEE Trans on Computers,1996,35(8):677-691
[7] Jackson M.Problem Frames Analyzing and Structuring Software Development Problems[J].Soffware Testing,Vertification and Reliability,2002,2(2):124-125
[8] Li Z.Progressing Problems from Requirements to Specifications in Problem Frame[D].Milton Keynes,United Kingdom: Department of Computing,The Open University,2009
[9] Hall J G,Rapanotti L,Jackson M.Problem-oriented software engineering:Solving the package router control problem[J].IEEE Trans.on Software Engineering,2008,4(2):226-241
[10] Schneider S.The B-Method:An Introduction[M].Basingstoke:Palgrave Macmillan,2001
[11] Abrial J R.The B-Book:Assigning Programs to Meanings[M].New York:Cambridge University Press,1996
[12] Hoare C A R.Communicating Sequential Processes[M].NewYork:Prentice-Hall,Inc.,1985
[13] Lai L,Sanders J W.A weakest-environment calculus for communicating processes[C]∥Fritzson P,Finmo L,eds.Proc.of the 4th Nordic Transputer Conf.:Parallel Programming and Applications.Ohmsha:IOS Press,1995:381-395
[14] Allen R,Garlan D.Formalizing architectural connection[C]∥Proc.of the 16th Int’l Conf.on Software Engineering.Los Alamitos:IEEE Computer Society,1994:71-80
[15] Allen R,Garlan D.A formal basis for architectural connection[J].ACM Trans.on Software Engineering and Methodology,1997,6(3):213-249
[16] Hoare C A R.Communicating sequential processes[J].Communications of the ACM,1978,1(8):666-677
[17] Ryan P,Schneider S,Goldsmith M,et al.The Modelling and Analysis of Security Protocols:The CSP Approach[M].Boston:Addison-Wesley,2000
[18] Roman G C.Specifying software/hardware interactions in distributed systems[C]∥Proc.of the 9th Int’l Conf.on Software Engineering.Los Alamitos:IEEE Computer Society,1987:126-139
[19] Hoare C A R,He J.Unifying Theories of Programming[M].New York:Prentice-Hall,1998
[20] Harrison M,Barnard P.On defining requirements for interaction[C]∥Proc.of the IEEE Int’l Symp.on Requirements Enginee-ring(RE’93).Washington:IEEE Computer Society,1993:50-54
[21] FDR.ProBE.http://www.fsel.com
[22] Hall A,Chapman R.Correctness by construction:Developing a commercial secure system[J].IEEE Software,2002,9(1):18-25
[23] Peleska J.Applied formal methods-From CSP to executable hybrid specifications[C]∥Abdallah A E,Jones C B,Sanders J W,eds.Proc.of the 2004 Int’l Conf.on Communicating Sequential Processes:The 1st 25 Years.Heidelberg:Springer-Verlag,2004:293-320
[24] Creese S.Industrial strength CSP:Opportunities and challenges in model-checking[C]∥Abdallah A E,Jones C B,Sanders J W,eds.Proc.of the 2004 Int’l Conf.on Communicating Sequential Processes:The 1st 25 Years.Heidelberg:Springer-Verlag,2004:292
[25] Harel D.Statecharts:A visual formalism for complex systems[J].Science of Computer Programming,1987,8(3):231-274
[26] Li Z.Progressing problems from requirements to specifications in problem frames[C]∥Proc.of the 3rd Int’l Workshop on Applications and Advances of Problem Frames (IWAAPF 2008).New York:ACM Press,2008:53-59
[27] Li Z,Hall J G,Rapanotti L.On the systematic transformation of requirements to specifications[J].Requirements Engineering,2014,9(4):397-419
[28] 李智,庞柳,刘国源,等.一种模型驱动的软件需求分析方法及技术支持[J].广西师范大学学报(自然科学版),2013,31(2):19-26 Li Z,Pang L,Liu G-Y,et al.A Model-Driven Software Requirements Analysis Method and Its Technical Support[J].Journal of Guangxi Normal University(Natural Science Edition),2013,1(2):19-26
[29] http://problemoriented.wikispaces.com/References+and+Links
[30] http://en.wikipedia.org/wiki/Problem-oriented_development
[31] Seater R,Jackson D,Gheyi R.Requirements progression inproblem frames[J].Deriving Specifications From Requirements,2007,2(2):77-102
[32] 朱利鲁.关于问题框架理论中领域间因果行为形式化验证的研究[D].桂林:广西师范大学,2015Zhu L-L.The Study About Formal Validation of Causal Beha-viors of Domains In Problem Frames[D].Guilin:Guangxi Normal University,2015

No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!