问题框架中问题领域因果行为的形式化验证
|
摘要
为问题框架中问题渐变所依赖的问题领域因果行为的确立提出一种形式化验证方法。为了对问题渐变过程中事件间的因果关系提供可验证的证据支持,简化问题表征的复杂度,进而提高计算机领域软件规约的可靠性,采纳了一种基于NuSMV语言的符号模型检验的形式化验证方法。该验证方法采用UML状态机表示问题领域内部状态变化的有限结构空间,用CTL公式描述问题域内状态之间的可达性性质,通过遍历有限结构状态机来检验CTL公式的正确性,筛选出具有因果关系的外部共享事件,为问题渐变提供有效的技术支持。
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 statechart to validate the correctness of the CTL formula,thus providing effective technical support to problem progression.
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 statechart to validate the correctness of the CTL formula,thus providing effective technical support to problem progression.
引文
[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,24(5):961-976Li Z,Jin Z.From user requirements to software specifications:An approach based on problem transformation[J].Journal of Software,2013,24(5):961-976
[4]杨军,葛海通,郑飞君,等.一种形式化验证方法:模型检验[J].浙江大学学报(理学版),2006,33(4):403-407Yang J,Ge Hai-tong,Zheng Fei-jun,et al.A formal validation method:model checking[J].Journal of Zhejiang University(Natural Science Edition),2006,33(4):403-407
[5]文静华,余滨,张梅,等.基于SMV的网络协议形式化分析与验证[J].计算机工程,2006,32(15):135-136,145Wen 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,145
[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,12(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,34(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].New York: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 the4th 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,21(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 Engineering(RE’93).Washington:IEEE Computer Society,1993:50-54
[21]FDR.ProBE[OL].http://www.fsel.com
[22]Hall A,Chapman R.Correctness by construction:Developing a commercial secure system[J].IEEE Software,2002,19(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 2004Int’l Conf.on Communicating Sequential Processes:The 1st 25Years.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 2004Int’l Conf.on Communicating Sequential Processes:The 1st 25Years.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,19(4):397-419
[28]李智,庞柳,刘国源,等.一种模型驱动的软件需求分析方法及技术支持[J].广西师范大学学报(自然科学版),2013,31(2):19-26Li 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,31(2):19-26
[29]http://problemoriented.wikispaces.com/References+and+Li nks
[30]http://en.wikipedia.org/wiki/Problem-oriented_development
[31]Seater R,Jackson D,Gheyi R.Requirements progression in problem frames[J].Deriving Specifications From Requirements,2007,12(2):77-102
[32]朱利鲁.关于问题框架理论中领域间因果行为形式化验证的研究[D].桂林:广西师范大学,2015Zhu L-L.The Study About Formal Validation of Causal Behaviors of Domains In Problem Frames[D].Guilin:Guangxi Normal University,2015
[2]Jackson M.Problem Frames:Analyzing and Structuring Software Development Problems[M].Boston:Addison-Wesley,2001
[3]李智,金芝.从用户需求到软件规约:一种问题变换的方法[J].软件学报,2013,24(5):961-976Li Z,Jin Z.From user requirements to software specifications:An approach based on problem transformation[J].Journal of Software,2013,24(5):961-976
[4]杨军,葛海通,郑飞君,等.一种形式化验证方法:模型检验[J].浙江大学学报(理学版),2006,33(4):403-407Yang J,Ge Hai-tong,Zheng Fei-jun,et al.A formal validation method:model checking[J].Journal of Zhejiang University(Natural Science Edition),2006,33(4):403-407
[5]文静华,余滨,张梅,等.基于SMV的网络协议形式化分析与验证[J].计算机工程,2006,32(15):135-136,145Wen 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,145
[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,12(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,34(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].New York: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 the4th 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,21(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 Engineering(RE’93).Washington:IEEE Computer Society,1993:50-54
[21]FDR.ProBE[OL].http://www.fsel.com
[22]Hall A,Chapman R.Correctness by construction:Developing a commercial secure system[J].IEEE Software,2002,19(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 2004Int’l Conf.on Communicating Sequential Processes:The 1st 25Years.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 2004Int’l Conf.on Communicating Sequential Processes:The 1st 25Years.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,19(4):397-419
[28]李智,庞柳,刘国源,等.一种模型驱动的软件需求分析方法及技术支持[J].广西师范大学学报(自然科学版),2013,31(2):19-26Li 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,31(2):19-26
[29]http://problemoriented.wikispaces.com/References+and+Li nks
[30]http://en.wikipedia.org/wiki/Problem-oriented_development
[31]Seater R,Jackson D,Gheyi R.Requirements progression in problem frames[J].Deriving Specifications From Requirements,2007,12(2):77-102
[32]朱利鲁.关于问题框架理论中领域间因果行为形式化验证的研究[D].桂林:广西师范大学,2015Zhu L-L.The Study About Formal Validation of Causal Behaviors of Domains In Problem Frames[D].Guilin:Guangxi Normal University,2015