Computer Science ›› 2015, Vol. 42 ›› Issue (12): 136-142.

Previous Articles     Next Articles

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

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!