一种软件演化过程建模、性质验证及性能分析方法
|
摘要
本文在EPMM的基础上,建立了以CCS为主要形式工具的软件演化过程的元模型CEPMM,它以任务不可分割为前提,支持软件演化过程全局层、过程层和活动层的形式建模与验证。本文致力于基于CEPMM建立的软件演化过程的建模,性质验证及性能评价,论文的主要工作如下。
(1)在全局层和过程层,提出了EPMM白盒方法建模与CEPMM建模的转化准则,在活动层,本文定义一种AML(Activity Modelling Language)非形式化规约语言,对活动建立非形式描述,同时给出了根据AML非形式规约借助于进程二叉树为活动的建模方法。
(2)本文提出对模型的进行局部范围内的性质验证,为此定义了待验证的对象和DFA子活动概念,通过模型分解来挖掘模型中性质分析验证的对象。
(3)对基于CEPMM建立的软件演化过程模型的结构合理性进行验证,即对模型的安全性与可达性进行验证。本文引入正则表达式来描述验证的性质,并分别针对模型的安全性和可达性的提出了正则表达式描述的方法,最后使用标号迁移系统LTS方法结合有限自动机提出有效的安全性与可达性验证方法。在模型验证中,借鉴CRA组合可达性分析的思想,为模型挑选安全性验证对象和可达性验证对象,对该模型安全性验证对象的集合下的划分中每个划分块的哈斯图,从哈斯图的极小元开始验证,对模型中安全性验证对象逐层进行验证,该方法在大大缩减状态空间的前提下,可以及时准确得定位模型中的问题使建模者能及时对模型进行改进,对可达性验证对象的集合下的划分中每个划分块的哈斯图每个划分块的最大元进行验证。
(4)资源与软件演化过程性能密切相关,为此本文对软件演化过程涉及到资源进行分析,为资源进行分类,并根据每类资源的特点对其属性进行分析。
(5)本文对软件演化过程的性能分析,为了支持软件演化过程进行性能评价,将进程代数CCS扩展了时间概率成本进程代数TCPCCS, TCPCCS支持软件演化过程时间、概率以及成本的分析,分析的结果可以作为决策的参考依据。
In this dissertation, on the basis of EPMM, software evolution process Meta-Mode CEPMM is proposed with CCS as fomal tool. Tasks are inseparable, EPMM supports modeling problem of software evolution process with formulation in global level and process level and activity level.This dissertation aims to the research on software evolution process modeling, verification and performance evaluation of software evolution process, for this purpose, there main progresses have been made in this dissertation.
Firstly, in global level and process level, the rule of transferring modeling based on EPMM by white box modeling approach into on CEPMM is proposed, and in activity level, according the informal specification of activity by AML(Activity Modelling Language), the approach modeling activity with the fomal tool CCS is proposed by means of process of binary tree.
Secondly, for verification the local structure, the concurrent structure and DFA sub-activity are introduced, an model decomposition approach to digging the local structure of it is put forward, with the local structure model as the properties analysis and verification object.
Thirdly, in order to verify the structure rationality of software evolution process, the dynamic properties safety and reachability of software evolution process model must be verified. The method for regular expression to describe safety and accessibility is introduced, and combining the Labeled Transition System (LTS) with the finite automaton, an efficient model verification method is proposed. Reference the idea of commositional reachability analysis, all safety verification objects in the model can be divided. For each Hasse diagram of patrtion, with minimal element of it beginning, properties analysis and verification objects in this model are safety verified step by step. Under the premise of this method, state space can be greatly reduced, and problems in the model can be timely and accurate positioning so that the modeler can timely improve the model.
Fourthly, resources is closely related to performance of the software evolution process, therefore in this dissertation, the software evolution process involves resources are analyzed and classified, and its properties are analyzed according to the characteristics of each type of resources.
At last, the performance of software evolution process is analyzed, in order to support modeling performance of software evolution process, process algebra CCS is extended to be process; algebra TCPCCS, TCPCCS support analyzing time, probability and cost of software evolution process, and the analysis of the results can be a reference for decision.
(1)在全局层和过程层,提出了EPMM白盒方法建模与CEPMM建模的转化准则,在活动层,本文定义一种AML(Activity Modelling Language)非形式化规约语言,对活动建立非形式描述,同时给出了根据AML非形式规约借助于进程二叉树为活动的建模方法。
(2)本文提出对模型的进行局部范围内的性质验证,为此定义了待验证的对象和DFA子活动概念,通过模型分解来挖掘模型中性质分析验证的对象。
(3)对基于CEPMM建立的软件演化过程模型的结构合理性进行验证,即对模型的安全性与可达性进行验证。本文引入正则表达式来描述验证的性质,并分别针对模型的安全性和可达性的提出了正则表达式描述的方法,最后使用标号迁移系统LTS方法结合有限自动机提出有效的安全性与可达性验证方法。在模型验证中,借鉴CRA组合可达性分析的思想,为模型挑选安全性验证对象和可达性验证对象,对该模型安全性验证对象的集合下的划分中每个划分块的哈斯图,从哈斯图的极小元开始验证,对模型中安全性验证对象逐层进行验证,该方法在大大缩减状态空间的前提下,可以及时准确得定位模型中的问题使建模者能及时对模型进行改进,对可达性验证对象的集合下的划分中每个划分块的哈斯图每个划分块的最大元进行验证。
(4)资源与软件演化过程性能密切相关,为此本文对软件演化过程涉及到资源进行分析,为资源进行分类,并根据每类资源的特点对其属性进行分析。
(5)本文对软件演化过程的性能分析,为了支持软件演化过程进行性能评价,将进程代数CCS扩展了时间概率成本进程代数TCPCCS, TCPCCS支持软件演化过程时间、概率以及成本的分析,分析的结果可以作为决策的参考依据。
In this dissertation, on the basis of EPMM, software evolution process Meta-Mode CEPMM is proposed with CCS as fomal tool. Tasks are inseparable, EPMM supports modeling problem of software evolution process with formulation in global level and process level and activity level.This dissertation aims to the research on software evolution process modeling, verification and performance evaluation of software evolution process, for this purpose, there main progresses have been made in this dissertation.
Firstly, in global level and process level, the rule of transferring modeling based on EPMM by white box modeling approach into on CEPMM is proposed, and in activity level, according the informal specification of activity by AML(Activity Modelling Language), the approach modeling activity with the fomal tool CCS is proposed by means of process of binary tree.
Secondly, for verification the local structure, the concurrent structure and DFA sub-activity are introduced, an model decomposition approach to digging the local structure of it is put forward, with the local structure model as the properties analysis and verification object.
Thirdly, in order to verify the structure rationality of software evolution process, the dynamic properties safety and reachability of software evolution process model must be verified. The method for regular expression to describe safety and accessibility is introduced, and combining the Labeled Transition System (LTS) with the finite automaton, an efficient model verification method is proposed. Reference the idea of commositional reachability analysis, all safety verification objects in the model can be divided. For each Hasse diagram of patrtion, with minimal element of it beginning, properties analysis and verification objects in this model are safety verified step by step. Under the premise of this method, state space can be greatly reduced, and problems in the model can be timely and accurate positioning so that the modeler can timely improve the model.
Fourthly, resources is closely related to performance of the software evolution process, therefore in this dissertation, the software evolution process involves resources are analyzed and classified, and its properties are analyzed according to the characteristics of each type of resources.
At last, the performance of software evolution process is analyzed, in order to support modeling performance of software evolution process, process algebra CCS is extended to be process; algebra TCPCCS, TCPCCS support analyzing time, probability and cost of software evolution process, and the analysis of the results can be a reference for decision.
引文
[1]杨芙清.软件工程技术发展思索.软件学报,2005,16(1)：1-7.
[2]Tong Li. An Approach to Modelling Software Evolution Processes [M]. Springer-Verlag,Berlin,2008.
[3]柳军飞,唐稚松.软件过程建模语言研究.软件学报,1996,7(8)：449-457.
[4]Arbaoui S, Derniame JC, Oquendo F, Verjus H. A Comparative Review of Process-centered Software Engineering Environments. Annal of Software Engineering, 2002,14(1-4):311-340.
[5]Bendraou R, Jezequel JM, Gervais MP and Blanc X. A Comparison of Six UML-Based Languages for Software Process Modeling. IEEE Transactions on Software Engineering,2010,36(5):662-675.
[6]李明树,杨秋松,翟健.软件过程建模方法研究.软件学报,2009,20(3)：524-545.
[7]Yoon C, Min SY and Bae DH. Tailoring and Verifying Software Process. Software Engineering Conference,2001, APSEC 2001, Eighth Asia-Pacific,2001:202-209.
[8]Liu XH, Wang WD and Liu WJ. An Intelligent Methodology for Business Process Model Verification. Proceedings of the 6th IEEE International Conference on Control and Automation (ICCA 2007), IEEE CS,2007:2381-2385.
[9]胡旷,董广智,田勇,柳军飞.一种弹性的软件过程模型验证工具.计算机工程与设计,2007,28(07)：1497-1500.
[10]Lee S, Shim J and Wu C. A meta model approach using UML for task assignment policy in software process. Proceedings of the 9th Asia-Pacific Software Engineering Conference on APSEC 2002. IEEE Computer Society,2002:376-382.
[11]费立蜀,顾庆,陈道蓄.一种过程定义模型及其验证性分析,计算机科学,2004,31(1)：145-151.
[12]Guo LH, Lu Z and Gu JZ. A Semantic Modeling and Verification Approach of Workflow Process Based on CSP. Proceedings of 2nd International ICST Conference on Communications and Networking (CHINACOM 2007), IEEE CS,2007:165-169
[13]National Institute of Standards and Technology. Integration Definition For Function Modeling (IDEF0).1993. Federal Information Processing Standards 183.
[14]Fernstrom C. PROCESS WEAVER:Adding Process Support to UNIX.Proceedings of 2nd conference on the Software Process,1993:12-26.
[15]Harel D, Lachover H, Naamad A, Pnueli A, Politi M, Sherman R, Shtul-Trauring A,and Trakhtenbrot M. STATEMATE:A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering,1990, 16(4):403-414.
[16]Cobleigh AM, Clark LA and Osterweil LJ. Verifying Properties of Process Definitions. ACM SIGSOFT Software Engineering Notes,2000,25(5):96-101.
[17]Lerner BS. Model Checking of Software Processes. Proceedings of FSE 2003,2003, 16(4):403-414.
[18JMin SY, Lee HD and Bae DH. SoftPM:A Software Process Management System Reconciling Formalism with Easiness. Information and Software Technology, 2000,42(1):1-16.
[19]Wang DL, Zhang DZ, Gao LX, Liu JM, Zhang HS. Process Knowledge Verification Method Based on Petri Net. Proceedings of 1 st International Workshop on Knowledge Discovery and Data Mining (WKDD 2008), IEEE CS,2008:173-178.
[20]Yang Q, Li M, Wang Q, Yang G, Zhai J, Li L, Hou L and Yang Y. An Algebraic Approach for Managing Inconsistencies in Software Processes. Proceedings of the Int'l Conf.on Software Processes (ICSP 2007). LNCS 4470, Springer-Verlag,2007:121-133.
[21][Wallace 03]Wallace C. Using Alloy in Process Modeling. Information and Software Technology,2003,45(15):1031-1043.
[22]Brockers A and Gruhn V. Computer-Aided Verification of Software Process Model Properties. Proceedings of Advanced Information Systems Engineering,1993:521-546.
[23]Basili VR and Rombach HD. Tailoring the Software Process to Project Goals and Environments. Proceedings of the 9th International Conference on Software Engineering,1987:345-357.
[24]C. A. RHoare,Communicating Sequennal Processes, Communications of the ACM, VO1.21 No.81978:666-677
[25]R..Milner. Communication and Concurrency. New York:Prentice Hall,1989
[26]S. C Cheung,J. Kramer. Checking Safety Properties Using Compositional Reachability Analysis.AcM Transactions on software Engineering Methodology(TOSEM), New York, NY:ACM Press, Vol.8 No.l 1999:49-78.
[27]S. C Cheung, D. Giannakopoulou, J Kramer. Verification of Liveness Properties Using compositional Reachability Analysis. ESEC/SIGSOFT FSE,New York, NY:Springer-Verlag New York, Inc,1997:227-243.
[28]D. Giannakopoulou,The Tracta Approach for Behaviour Analysis of Concurrent Systems. Imperial College Research Report, London:Imperial College, Department of Computing, No.95/161995:16.
[29]J. cobleighjD.Giannakopoulou, C.S.Pasareanu. Learning assumptions fo compositional verification.Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes In Computer Science, Warsaw Poland:Springer, Vol.2619 April 2003:331-346.
[30]Pnueli A. The temporal semantics of concurrent programs.18th Annual Symposium on Foundations of Computer Science,1977.
[31]Owicki S and Lamport L. Proving liveness properties of concurrent programs.ACM Transaction Program. Lang. Syst,1982,4(3):455-495.
[32]Clarke EM and Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. Kozen, D. (ed.) Logic of Programs 1981. LNCS,Springer,1981,131:52-71.
[33]Pnueli A. The temporal semantics of concurrent programs. Theoretical Computer Science,1981,13:45-60。
[34]Clarke EM, Emerson EA and Sistla J. Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specification. ACM Transactions on Programming Languages and Systems,1986,8(2):244-163.
[35]Lamport L. "Sometimes" is sometimes "not never". Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages,1980:174-185.
[36]Emerson EA and Halpern JY. "Sometimes" and "not never" revisited:On branching versus linear time. Journal of the ACM,1986,33(1):151-178.
[37]段振华,张曼.Petri网模型检测概述.中国计算机学会通讯,2009,5(10)：21-28.
[38]Howell RR and Rosier LE. Problems concerning fairness and temporal logic for conflict-free Petri nets. Theoretical Computer Science 64,1989:305-329.
[39]Esparza J. Decidability and Complexity of Petri Net Problems-An Introduction.Lectures on Petri Nets I:Basic Models, Advances in Petri Nets.1996: 374-428.
[40]Berthelot G. Transformations and Decompositions of Nets. In Advances in Petri Nets, Springer LNCS,1987,254:359-376.
[41]Silva M. Sur le concept de macroplace et son utilisation pour lanalyse des reseaux de Petri. R.A.I.R.O. Automatique/Systems Analysis and Control,1981,15(4):335-345.
[42]Silva M. Las redes de Petri en la Automaticia. y la Informatica. Editorial AC,Madrid,1985.
-[43] Suzuki I. Fundamental Properties and Applications of Temporal Petri nets. In Proc. 9th Annu. Conf. Information Sciences and Systems, Johns Hopkins Univ., Baltimore,MD,1985:641-646.
[44]Suzuki I and Lu H. Temporal Petri Nets and Their Application to Modeling and Analysis of a Handshake Daisy Chain Arbiter. IEEE Transaction on Computers,1989, 38(5):696-704.
[45]Suziki I. Formal Analysis of Alternating Bit Protocol by Temporal Petri nets. IEEET ransactions on Software Engineering,1990,16(11):1273-1281.
[46]Feder M, Mandrilli D and Morzenti A. Proving Properties of Real-time Systems through Logical Specifications and Petri Net Models. IEEE Transactions on Software Engineering,1994,20(2):127-141.
[47]Petri CA. Kommunikation mit automaten. Institut fur Instrumentelle Mathematik,Schriften des ⅡM 2, Bonn,1962.
[48]ISO/IEC 15909-1 standard for software and system engineering-high level Petri Nets-partl:concepts, definitions and graphical notation.
[49]Reisig W. Petri Nets:An introduction. Springer-Verlag, Berlin,1985.
[50]袁崇义.Petri网原理与应用.2005年,电子工业出版社.
[51]Harel D and Pnueli A. On the Development of Reactive Systems, in Logics and models of concurrent systems. (La Colle-sur-Loup,1984), vol.13 of NATO Adv. Sci. Inst. Ser.F Computer. Systems Sci., Springer-Verlag, Berlin,1985:477-498.
[52]Bekic H. Towards a Mathematical Theory of Processes. Programming Languages and Their Definition, LNCS, Springer,1984,177:168-206.
[53]Milner R. A Calculus of Communicating Systems. Lecture Notes in Computer Science, Springer-Verlag, vol 92,1980.
[54]Hoare CAR. Communicating Sequential Processes. Communications of the ACM,1978,21(8):666-677.
[55]Hoare CAR. Communicating Sequential Process. Prentice-Hall,1985.
[56]Bergstra JA and Klop JW. The Algebra of Recursively Defined Processes and the Algebra of Regular Processes. Proceedings of ICALP'84, LNCS 172, Springer-Verlag,1984:82-95.
[57]Milner R. An Algebraic Definition of Simulation between Programs. Proceedings of 2nd Int. Joint. Conference on Artifical Intelligence,1971:481-489.
[58]Milner R. Communicating and Mobile Systems the pi-calculus. Cambridge University Press,1999.
[59]J.Magee,J.Kramer. Concurrency:State Models & Java Programs,New York:John Wiley & Sons,1999.
[60]E.M Clarke,O.Grumberg,D.A Peled.Model Checking.Cambridge,MA:MIT Press,1999.
[61]PJancar,A.Kucera:Bisimilarity of processes with finite-state systems,Electronic Notes in Theoratical Computer Science,91997.
[62]J.Stribma.Approximating Weak Bisimulation on Basic Process Algebras,Leccture Notes In Computer Science.Springer-Verlag,Vol.1672 London,UK 1999:366-375.
[63]U.Frendrup,J.N Jensen.A Complete Axiomatization of Simulation for Regular CCS Expressions,Basic Research in Computer Science Rs-01-26,2001. http://www.brics.dk/RS/01/26/BRICS-RS-01-26.pdf
[64]R.Mimer. Communication and Concurrency.NewYork:Prentice Hall,1989.
[65]左孝凌等.离散数学,上海科学技术文献出版社,1982.
[66]Cheung S C, Kramer J.Checking safety properties using compositional reachability analysis[J]. ACM Transactionson Software Engineering and Methodology (TOSEM). New York,NY:ACM Press,1999, 8(1):49-78.
[67]许强,基于确定有限状态自动机的正则表达式引擎的设计与实现[D].西安,西安电子科技大学,2012.
[68]李铁男,基于自动机的正则表达式匹配算法[D].沈阳,东北大学,2011.
[69]Kumar S,Dharmapurikar S, Yu F,et al. Algorithms to accelerate multiple regular expressions matching for deep packet inspection [A]. In Proceedings of the 2006 ACM SIGCOMM Conference,2006:339-350.
[70]Becchi M,Cadambi, S. Memory-Efficient Regular Expression Search Using State Merging [A]. In Proceedings ofINFOCOM 200T[C],2007:1064-1072.
[71]Zhang J,Zhang D,Huang K. A regular expression matching algorithm using Transition Merging [A], In Proceedings of the 15th IEEE Pacific Rim International Symposium on Dependable Computing [C],2009:242-246.
[72]李彤.软件演化过程研究结题报告[M],2007.
[73]代飞.基于EPMM的软件演化过程模型验证[D].昆明,云南大学,2011.
[74]代飞,李彤,谢仲文,于倩,卢萍,郁涌,赵娜.一种软件演化过程模型的代数语义[J].软件学报,2012.
[75]吴帅.UML模型图到B方法形式规约的转换研究与应用[D].江西：江西师范大学,2007
[76]李杨李杨,程建华,房鼎益,陈晓江,冯健.并发系统的安全性与活性的验证方法[J]计算机工程与应用,2008,44(4)
[77]丁志军,蒋昌俊.并发程序验证的时序petri网方法[J].计算机学报,2002,25(5).
[78]Clarke E M.Automatic verification of finite state concurrent system using temporal logical specification[J]. ACM Transaction on Programming Language and Systems,1986,8(2):244-263.
[79]Robin Milner.通信与移动系统π[演算[M].清华大学出版社,2009,6.
[80]梁爱南,李长云,黄贤明.基于π演算的工作流模型分析方法[J].计算机工程,2010,36(6)：70-72.
[81]刘峰,陈笑蓉.基于π演算的工作流模型检验[J].计算机工程,2011,37(23)：
[82]耿素云,屈婉玲,王捍贫.离散数学教程[M].北京大学出版社,1999年9月
[83]杨琛.基于进程代数并发系统的建模与验证研究[D].2006,西安,西北大学.
[84]李杨,程建华,房鼎益,陈晓江,冯健.并发系统的安全性与活性的验证方法[J]计算机工程与应用,2008,44(4)
[85]Fernandez J C, Mounier L, Jard C, et al.On-the-fly verification of finite transition systems[M].Formal Methods in System Design 1(2/3)Hingham, MA:Kluwer Academic Publishers,1992:251-273.
[86]易锦,张文辉.从基于迁移的扩展Buchi自动机到Buchi自动机[J].软件学报,2006,17(4)：720-728.
[87]鲍震宁,张洵,范玉顺.企业资源建模方法研究[J].航空制造技术,2002,(12)：41-44.
[88]万静.基于约束规划的软件过程控制方法研究[D].北京：北京化工大学,2011.
[89]祖旭,黄洪钟,周峰,古莹奎.产品开发过程资源管理及其仿真[J].系统仿真学报,Vol.17 No.6 Jun.2005
[90]Behrmann G, Fehnker A, Hune T, et al. Minimum-cost reachability for priced timed automata[J]. Lecture Notes in Computer Science,2001,2034:147-161.
[91]肖芳雄,黄志球,曹子宁,张君华,覃志东.一种扩展了价格信息的进程代数[J].南京航空大学学报,Vol.41 No. 1 Feb.2009
[92]肖芳雄,李燕,黄志球,曹子宁,陈哲,范大娟,基于时间概率代价进程代数的Web服务组合建模和分析
[93]Baeten J. A brief history of process algebra. Theoretical Computer Science,2005, 335(2-3),131-146
[2]Tong Li. An Approach to Modelling Software Evolution Processes [M]. Springer-Verlag,Berlin,2008.
[3]柳军飞,唐稚松.软件过程建模语言研究.软件学报,1996,7(8)：449-457.
[4]Arbaoui S, Derniame JC, Oquendo F, Verjus H. A Comparative Review of Process-centered Software Engineering Environments. Annal of Software Engineering, 2002,14(1-4):311-340.
[5]Bendraou R, Jezequel JM, Gervais MP and Blanc X. A Comparison of Six UML-Based Languages for Software Process Modeling. IEEE Transactions on Software Engineering,2010,36(5):662-675.
[6]李明树,杨秋松,翟健.软件过程建模方法研究.软件学报,2009,20(3)：524-545.
[7]Yoon C, Min SY and Bae DH. Tailoring and Verifying Software Process. Software Engineering Conference,2001, APSEC 2001, Eighth Asia-Pacific,2001:202-209.
[8]Liu XH, Wang WD and Liu WJ. An Intelligent Methodology for Business Process Model Verification. Proceedings of the 6th IEEE International Conference on Control and Automation (ICCA 2007), IEEE CS,2007:2381-2385.
[9]胡旷,董广智,田勇,柳军飞.一种弹性的软件过程模型验证工具.计算机工程与设计,2007,28(07)：1497-1500.
[10]Lee S, Shim J and Wu C. A meta model approach using UML for task assignment policy in software process. Proceedings of the 9th Asia-Pacific Software Engineering Conference on APSEC 2002. IEEE Computer Society,2002:376-382.
[11]费立蜀,顾庆,陈道蓄.一种过程定义模型及其验证性分析,计算机科学,2004,31(1)：145-151.
[12]Guo LH, Lu Z and Gu JZ. A Semantic Modeling and Verification Approach of Workflow Process Based on CSP. Proceedings of 2nd International ICST Conference on Communications and Networking (CHINACOM 2007), IEEE CS,2007:165-169
[13]National Institute of Standards and Technology. Integration Definition For Function Modeling (IDEF0).1993. Federal Information Processing Standards 183.
[14]Fernstrom C. PROCESS WEAVER:Adding Process Support to UNIX.Proceedings of 2nd conference on the Software Process,1993:12-26.
[15]Harel D, Lachover H, Naamad A, Pnueli A, Politi M, Sherman R, Shtul-Trauring A,and Trakhtenbrot M. STATEMATE:A working environment for the development of complex reactive systems. IEEE Transactions on Software Engineering,1990, 16(4):403-414.
[16]Cobleigh AM, Clark LA and Osterweil LJ. Verifying Properties of Process Definitions. ACM SIGSOFT Software Engineering Notes,2000,25(5):96-101.
[17]Lerner BS. Model Checking of Software Processes. Proceedings of FSE 2003,2003, 16(4):403-414.
[18JMin SY, Lee HD and Bae DH. SoftPM:A Software Process Management System Reconciling Formalism with Easiness. Information and Software Technology, 2000,42(1):1-16.
[19]Wang DL, Zhang DZ, Gao LX, Liu JM, Zhang HS. Process Knowledge Verification Method Based on Petri Net. Proceedings of 1 st International Workshop on Knowledge Discovery and Data Mining (WKDD 2008), IEEE CS,2008:173-178.
[20]Yang Q, Li M, Wang Q, Yang G, Zhai J, Li L, Hou L and Yang Y. An Algebraic Approach for Managing Inconsistencies in Software Processes. Proceedings of the Int'l Conf.on Software Processes (ICSP 2007). LNCS 4470, Springer-Verlag,2007:121-133.
[21][Wallace 03]Wallace C. Using Alloy in Process Modeling. Information and Software Technology,2003,45(15):1031-1043.
[22]Brockers A and Gruhn V. Computer-Aided Verification of Software Process Model Properties. Proceedings of Advanced Information Systems Engineering,1993:521-546.
[23]Basili VR and Rombach HD. Tailoring the Software Process to Project Goals and Environments. Proceedings of the 9th International Conference on Software Engineering,1987:345-357.
[24]C. A. RHoare,Communicating Sequennal Processes, Communications of the ACM, VO1.21 No.81978:666-677
[25]R..Milner. Communication and Concurrency. New York:Prentice Hall,1989
[26]S. C Cheung,J. Kramer. Checking Safety Properties Using Compositional Reachability Analysis.AcM Transactions on software Engineering Methodology(TOSEM), New York, NY:ACM Press, Vol.8 No.l 1999:49-78.
[27]S. C Cheung, D. Giannakopoulou, J Kramer. Verification of Liveness Properties Using compositional Reachability Analysis. ESEC/SIGSOFT FSE,New York, NY:Springer-Verlag New York, Inc,1997:227-243.
[28]D. Giannakopoulou,The Tracta Approach for Behaviour Analysis of Concurrent Systems. Imperial College Research Report, London:Imperial College, Department of Computing, No.95/161995:16.
[29]J. cobleighjD.Giannakopoulou, C.S.Pasareanu. Learning assumptions fo compositional verification.Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes In Computer Science, Warsaw Poland:Springer, Vol.2619 April 2003:331-346.
[30]Pnueli A. The temporal semantics of concurrent programs.18th Annual Symposium on Foundations of Computer Science,1977.
[31]Owicki S and Lamport L. Proving liveness properties of concurrent programs.ACM Transaction Program. Lang. Syst,1982,4(3):455-495.
[32]Clarke EM and Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. Kozen, D. (ed.) Logic of Programs 1981. LNCS,Springer,1981,131:52-71.
[33]Pnueli A. The temporal semantics of concurrent programs. Theoretical Computer Science,1981,13:45-60。
[34]Clarke EM, Emerson EA and Sistla J. Automatic Verification of Finite-state Concurrent Systems Using Temporal Logic Specification. ACM Transactions on Programming Languages and Systems,1986,8(2):244-163.
[35]Lamport L. "Sometimes" is sometimes "not never". Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages,1980:174-185.
[36]Emerson EA and Halpern JY. "Sometimes" and "not never" revisited:On branching versus linear time. Journal of the ACM,1986,33(1):151-178.
[37]段振华,张曼.Petri网模型检测概述.中国计算机学会通讯,2009,5(10)：21-28.
[38]Howell RR and Rosier LE. Problems concerning fairness and temporal logic for conflict-free Petri nets. Theoretical Computer Science 64,1989:305-329.
[39]Esparza J. Decidability and Complexity of Petri Net Problems-An Introduction.Lectures on Petri Nets I:Basic Models, Advances in Petri Nets.1996: 374-428.
[40]Berthelot G. Transformations and Decompositions of Nets. In Advances in Petri Nets, Springer LNCS,1987,254:359-376.
[41]Silva M. Sur le concept de macroplace et son utilisation pour lanalyse des reseaux de Petri. R.A.I.R.O. Automatique/Systems Analysis and Control,1981,15(4):335-345.
[42]Silva M. Las redes de Petri en la Automaticia. y la Informatica. Editorial AC,Madrid,1985.
-[43] Suzuki I. Fundamental Properties and Applications of Temporal Petri nets. In Proc. 9th Annu. Conf. Information Sciences and Systems, Johns Hopkins Univ., Baltimore,MD,1985:641-646.
[44]Suzuki I and Lu H. Temporal Petri Nets and Their Application to Modeling and Analysis of a Handshake Daisy Chain Arbiter. IEEE Transaction on Computers,1989, 38(5):696-704.
[45]Suziki I. Formal Analysis of Alternating Bit Protocol by Temporal Petri nets. IEEET ransactions on Software Engineering,1990,16(11):1273-1281.
[46]Feder M, Mandrilli D and Morzenti A. Proving Properties of Real-time Systems through Logical Specifications and Petri Net Models. IEEE Transactions on Software Engineering,1994,20(2):127-141.
[47]Petri CA. Kommunikation mit automaten. Institut fur Instrumentelle Mathematik,Schriften des ⅡM 2, Bonn,1962.
[48]ISO/IEC 15909-1 standard for software and system engineering-high level Petri Nets-partl:concepts, definitions and graphical notation.
[49]Reisig W. Petri Nets:An introduction. Springer-Verlag, Berlin,1985.
[50]袁崇义.Petri网原理与应用.2005年,电子工业出版社.
[51]Harel D and Pnueli A. On the Development of Reactive Systems, in Logics and models of concurrent systems. (La Colle-sur-Loup,1984), vol.13 of NATO Adv. Sci. Inst. Ser.F Computer. Systems Sci., Springer-Verlag, Berlin,1985:477-498.
[52]Bekic H. Towards a Mathematical Theory of Processes. Programming Languages and Their Definition, LNCS, Springer,1984,177:168-206.
[53]Milner R. A Calculus of Communicating Systems. Lecture Notes in Computer Science, Springer-Verlag, vol 92,1980.
[54]Hoare CAR. Communicating Sequential Processes. Communications of the ACM,1978,21(8):666-677.
[55]Hoare CAR. Communicating Sequential Process. Prentice-Hall,1985.
[56]Bergstra JA and Klop JW. The Algebra of Recursively Defined Processes and the Algebra of Regular Processes. Proceedings of ICALP'84, LNCS 172, Springer-Verlag,1984:82-95.
[57]Milner R. An Algebraic Definition of Simulation between Programs. Proceedings of 2nd Int. Joint. Conference on Artifical Intelligence,1971:481-489.
[58]Milner R. Communicating and Mobile Systems the pi-calculus. Cambridge University Press,1999.
[59]J.Magee,J.Kramer. Concurrency:State Models & Java Programs,New York:John Wiley & Sons,1999.
[60]E.M Clarke,O.Grumberg,D.A Peled.Model Checking.Cambridge,MA:MIT Press,1999.
[61]PJancar,A.Kucera:Bisimilarity of processes with finite-state systems,Electronic Notes in Theoratical Computer Science,91997.
[62]J.Stribma.Approximating Weak Bisimulation on Basic Process Algebras,Leccture Notes In Computer Science.Springer-Verlag,Vol.1672 London,UK 1999:366-375.
[63]U.Frendrup,J.N Jensen.A Complete Axiomatization of Simulation for Regular CCS Expressions,Basic Research in Computer Science Rs-01-26,2001. http://www.brics.dk/RS/01/26/BRICS-RS-01-26.pdf
[64]R.Mimer. Communication and Concurrency.NewYork:Prentice Hall,1989.
[65]左孝凌等.离散数学,上海科学技术文献出版社,1982.
[66]Cheung S C, Kramer J.Checking safety properties using compositional reachability analysis[J]. ACM Transactionson Software Engineering and Methodology (TOSEM). New York,NY:ACM Press,1999, 8(1):49-78.
[67]许强,基于确定有限状态自动机的正则表达式引擎的设计与实现[D].西安,西安电子科技大学,2012.
[68]李铁男,基于自动机的正则表达式匹配算法[D].沈阳,东北大学,2011.
[69]Kumar S,Dharmapurikar S, Yu F,et al. Algorithms to accelerate multiple regular expressions matching for deep packet inspection [A]. In Proceedings of the 2006 ACM SIGCOMM Conference,2006:339-350.
[70]Becchi M,Cadambi, S. Memory-Efficient Regular Expression Search Using State Merging [A]. In Proceedings ofINFOCOM 200T[C],2007:1064-1072.
[71]Zhang J,Zhang D,Huang K. A regular expression matching algorithm using Transition Merging [A], In Proceedings of the 15th IEEE Pacific Rim International Symposium on Dependable Computing [C],2009:242-246.
[72]李彤.软件演化过程研究结题报告[M],2007.
[73]代飞.基于EPMM的软件演化过程模型验证[D].昆明,云南大学,2011.
[74]代飞,李彤,谢仲文,于倩,卢萍,郁涌,赵娜.一种软件演化过程模型的代数语义[J].软件学报,2012.
[75]吴帅.UML模型图到B方法形式规约的转换研究与应用[D].江西：江西师范大学,2007
[76]李杨李杨,程建华,房鼎益,陈晓江,冯健.并发系统的安全性与活性的验证方法[J]计算机工程与应用,2008,44(4)
[77]丁志军,蒋昌俊.并发程序验证的时序petri网方法[J].计算机学报,2002,25(5).
[78]Clarke E M.Automatic verification of finite state concurrent system using temporal logical specification[J]. ACM Transaction on Programming Language and Systems,1986,8(2):244-263.
[79]Robin Milner.通信与移动系统π[演算[M].清华大学出版社,2009,6.
[80]梁爱南,李长云,黄贤明.基于π演算的工作流模型分析方法[J].计算机工程,2010,36(6)：70-72.
[81]刘峰,陈笑蓉.基于π演算的工作流模型检验[J].计算机工程,2011,37(23)：
[82]耿素云,屈婉玲,王捍贫.离散数学教程[M].北京大学出版社,1999年9月
[83]杨琛.基于进程代数并发系统的建模与验证研究[D].2006,西安,西北大学.
[84]李杨,程建华,房鼎益,陈晓江,冯健.并发系统的安全性与活性的验证方法[J]计算机工程与应用,2008,44(4)
[85]Fernandez J C, Mounier L, Jard C, et al.On-the-fly verification of finite transition systems[M].Formal Methods in System Design 1(2/3)Hingham, MA:Kluwer Academic Publishers,1992:251-273.
[86]易锦,张文辉.从基于迁移的扩展Buchi自动机到Buchi自动机[J].软件学报,2006,17(4)：720-728.
[87]鲍震宁,张洵,范玉顺.企业资源建模方法研究[J].航空制造技术,2002,(12)：41-44.
[88]万静.基于约束规划的软件过程控制方法研究[D].北京：北京化工大学,2011.
[89]祖旭,黄洪钟,周峰,古莹奎.产品开发过程资源管理及其仿真[J].系统仿真学报,Vol.17 No.6 Jun.2005
[90]Behrmann G, Fehnker A, Hune T, et al. Minimum-cost reachability for priced timed automata[J]. Lecture Notes in Computer Science,2001,2034:147-161.
[91]肖芳雄,黄志球,曹子宁,张君华,覃志东.一种扩展了价格信息的进程代数[J].南京航空大学学报,Vol.41 No. 1 Feb.2009
[92]肖芳雄,李燕,黄志球,曹子宁,陈哲,范大娟,基于时间概率代价进程代数的Web服务组合建模和分析
[93]Baeten J. A brief history of process algebra. Theoretical Computer Science,2005, 335(2-3),131-146