基于Petri网的嵌入式系统建模与验证研究
|
摘要
随着嵌入式系统在各个领域的广泛应用,嵌入式系统变得越来越复杂。在嵌入式系统设计中采用模型的方法,有利于确保系统的正确性,缩短开发周期,降低开发费用。本文以Perti网为建模工具,对嵌入式系统的建模和分析验证进行了一些研究。
嵌入式系统具有实时性、并发性等特点,并要求高可靠性和正确性。为了设计具有这样特点的系统,设计过程必须基于一个形式化描述,以捕获嵌入式系统的这些特点。Petri网对这类系统是一个很好的描述方法:可以表示并行和连续活动,并且很容易捕捉不确定性行为。但传统的Petri网缺乏时间概念和数据表达力,不能很好的描述嵌入式系统的实时性要求和数据流。针对传统Petri网的这些缺点,本文提出基于PRES+的嵌入式系统的建模与分析验证研究。
首先,介绍嵌入式系统的一个形式化计算模型PRES+,可以描述嵌入式系统的一些重要特征,其中,托肯携带数据信息,变迁执行数据的转换,时间通过与变迁相连的活动期限来捕获。同时,引入PRES+模型的分层机制和组合修改操作。分层机制使模型能够有条理的构建,由简单的单元组件构成,使得设计师在每个描述级上都可以很容易理解;组合修改操作,通过增加或减少模块来改变其功能或状态,从而以最小的影响,实现了网模型的修改,并有效保存了系统的性质,使系统在修改后不需要再重新验证其性质。
其次,介绍了系统模型的分析与验证,对基于PRES+建模的嵌入式系统,分别提出两种方法,对它进行分析验证。第一种为形式化验证方法,利用模型检测来验证系统的一些性质,将其表示成时序逻辑公式。介绍了一个转换程序,把PRES+模型转换成时间自动机TA,并使用模型验证工具UPPAAL对其进行分析验证;第二种方法,通过程序模拟Petri网中各个库所中托肯的变化情况,模拟Petri网的动态行为,从而达到分析验证的目的。最后,提出一种策略,使用正确性保留等价转换,对PRES+模型进行简化,从而提高其验证效率。
Embedded systems becomes more and more complicated with its widespread use in a variety of domains. Modeling approach could improve the correctness,shorten the period of design,and reduce the cost in embedded system development.Base on Petri Net,we did some research on embedded system modeling and verification.
Embedded sytems are characterized by their dedicated function,real-time and concurrent behavior,and high requirements on reliability and correctness.In order to devise systems with such features,the design process must be based upon a formal representation that captures the characteristics of embedded systems. Petri nets are an good represnetation for this sort of systems: it can represent parallel as well as sequential activities and easily capture non-deterministic behaviors.However,the traditional Petri net model lacks the notion of time and data expression,it can not represent the real-time requirement and data flow.To meet these problems,this paper proposed the research on embedded system modeling and analysis base on PRES+.
First ,we present a formal computation model PRES+ for embedded system .The model can capture some important features of embedded sytems,in which tokens hold information,transitons perform transformation of data,and timing is captured by associating lower and upper limits to the duration of activities related to transitions.Furthermore,introduce the Hierarchy mechanism as well as the compositon and modification operation.Hierarchy is a useful tool that allows the system to be constructed in a structured way by composing a number of fully understandble entities;The composition and modificaion operation can change the functions or statesadd by adding or reducing the module,thus,it changes the net model in a lower effect,and perserves the system properties,so that we need not to verify its properties after changed again.
Sencond ,we presnet the analysis and verification of the system model, propose two methods to analyze and verify the systems represented in PRES+,the first method is the formal verification,in which model checking is used to prove whether the system model satisfies its required properties expressed as temproal logic formulas.Introduce a translation procedure that translate the PRES+ model to time automata,and then analyze and verify the TA model using the Uppaal;the second method,through the program to simulate the changes of the token in every places,simulate the dynamic behavior of Petri net to achieve the analysis and testing purposes. Besides,propose a strategy, simplify the PRES+ model through the correctness-perservation equivalent translation,in order to improve the verification efficiency.
嵌入式系统具有实时性、并发性等特点,并要求高可靠性和正确性。为了设计具有这样特点的系统,设计过程必须基于一个形式化描述,以捕获嵌入式系统的这些特点。Petri网对这类系统是一个很好的描述方法:可以表示并行和连续活动,并且很容易捕捉不确定性行为。但传统的Petri网缺乏时间概念和数据表达力,不能很好的描述嵌入式系统的实时性要求和数据流。针对传统Petri网的这些缺点,本文提出基于PRES+的嵌入式系统的建模与分析验证研究。
首先,介绍嵌入式系统的一个形式化计算模型PRES+,可以描述嵌入式系统的一些重要特征,其中,托肯携带数据信息,变迁执行数据的转换,时间通过与变迁相连的活动期限来捕获。同时,引入PRES+模型的分层机制和组合修改操作。分层机制使模型能够有条理的构建,由简单的单元组件构成,使得设计师在每个描述级上都可以很容易理解;组合修改操作,通过增加或减少模块来改变其功能或状态,从而以最小的影响,实现了网模型的修改,并有效保存了系统的性质,使系统在修改后不需要再重新验证其性质。
其次,介绍了系统模型的分析与验证,对基于PRES+建模的嵌入式系统,分别提出两种方法,对它进行分析验证。第一种为形式化验证方法,利用模型检测来验证系统的一些性质,将其表示成时序逻辑公式。介绍了一个转换程序,把PRES+模型转换成时间自动机TA,并使用模型验证工具UPPAAL对其进行分析验证;第二种方法,通过程序模拟Petri网中各个库所中托肯的变化情况,模拟Petri网的动态行为,从而达到分析验证的目的。最后,提出一种策略,使用正确性保留等价转换,对PRES+模型进行简化,从而提高其验证效率。
Embedded systems becomes more and more complicated with its widespread use in a variety of domains. Modeling approach could improve the correctness,shorten the period of design,and reduce the cost in embedded system development.Base on Petri Net,we did some research on embedded system modeling and verification.
Embedded sytems are characterized by their dedicated function,real-time and concurrent behavior,and high requirements on reliability and correctness.In order to devise systems with such features,the design process must be based upon a formal representation that captures the characteristics of embedded systems. Petri nets are an good represnetation for this sort of systems: it can represent parallel as well as sequential activities and easily capture non-deterministic behaviors.However,the traditional Petri net model lacks the notion of time and data expression,it can not represent the real-time requirement and data flow.To meet these problems,this paper proposed the research on embedded system modeling and analysis base on PRES+.
First ,we present a formal computation model PRES+ for embedded system .The model can capture some important features of embedded sytems,in which tokens hold information,transitons perform transformation of data,and timing is captured by associating lower and upper limits to the duration of activities related to transitions.Furthermore,introduce the Hierarchy mechanism as well as the compositon and modification operation.Hierarchy is a useful tool that allows the system to be constructed in a structured way by composing a number of fully understandble entities;The composition and modificaion operation can change the functions or statesadd by adding or reducing the module,thus,it changes the net model in a lower effect,and perserves the system properties,so that we need not to verify its properties after changed again.
Sencond ,we presnet the analysis and verification of the system model, propose two methods to analyze and verify the systems represented in PRES+,the first method is the formal verification,in which model checking is used to prove whether the system model satisfies its required properties expressed as temproal logic formulas.Introduce a translation procedure that translate the PRES+ model to time automata,and then analyze and verify the TA model using the Uppaal;the second method,through the program to simulate the changes of the token in every places,simulate the dynamic behavior of Petri net to achieve the analysis and testing purposes. Besides,propose a strategy, simplify the PRES+ model through the correctness-perservation equivalent translation,in order to improve the verification efficiency.
引文
1. Wayne Wolf著,孙玉芳等译.嵌入式计算系统设计原理[M].北京:机械工业出版社,2002.4-7
2. Luis AlejandroC. Modeling and formal verifieation of embeddeds on a Petri net representation[J].Systems Architecture,2003,49:571-589.
3. Daniel D ajski,Frank Vahid,Sanjiv Narayan等.边计年,吴为民译.嵌入式系统的描述与设计[M].北京:机械工业出版社,2005
4. Trong-Yen Lee; Pao-Ann Hsiung. Embedded software synthesis and prototyping[C]. Consumer Electronics, IEEE Transactions on Volume 50, Issue 1, Feb 2004 Page(s):386– 392
5. Gomes L,Costa A .Petri nets as supporting formalism within Embedded Systems Co-design[C]. International Symposium on Industrial Embedded Systems ,2006:1– 4
6.郭军.基于Petri网的嵌入式系统高层级设计方法与技术研究[博士论文].西北大学.2007:20-31
7.廖晓文.基于UML与Petri网的嵌入式系统建模方法的研究[硕士论文].广东工业大学.2005:1-3
8. Pettit. R.G., Gomaa. H. Analyzing Behavior of Concurrent Software Designs for Embedded Systems[C]. Object and Component-Oriented Real-Time Distributed Computing, 2007. ISORC '07. 10th IEEE International Symposium on 7-9 May 2007 Page(s):124– 132
9. Pimentel. J.R. Safety-reliability of distributed embedded system fault tolerant units[C]. Industrial Electronics Society, 2003. IECON '03. The 29th Annual Conference of the IEEE Volume 1, 2-6 Nov. 2003 Page(s):945 - 950 vol.1
10. Gomes, L.; Lourenco, J. Petri nets-based automatic generation GUI tools for embedded systems[C].Human System Interactions, 2008 Conference on 25-27 May 2008 Page(s):269– 274
11. Cortes, L.A.; Eles, P.; Peng, Z.Verification of embedded systems using a Petri net based representation[C].System Synthesis, 2000. Proceedings. The 13th International Symposium on 20-22 Sept. 2000 Page(s):149– 155
12. Gomes. L., Barros. J.P., Costa. A., Pais. R., Moutinho. F. Towards usage of formal methods within embedded systems co-design[C].Emerging Technologies and Factory Automation, 2005. ETFA 2005. 10th IEEE Conference on Volume 1, 19-22 Sept. 2005 Page(s):4 pp.– 284
13.王志英.嵌入式系统原理与设计[M].北京:高等教育出版社,2007.4-5
14. Claude Girault,Rudiger Valk .王生原等译.系统工程Petri网—建模、验证与应用指南[M].北京:电子工业出版社,2005
15. Liqiong Chen; Zhiqing Shao; Guisheng Fan; Xiuying Wang. Modeling and Analyzing Distributed Real-time and Embedded Systems with High-Level Petri Nets[C].Mechtronic and Embedded Systems and Applications, 2008. MESA 2008. IEEE/ASME International Conference on 12-15 Oct. 2008 Page(s):476– 481
16. T murata. Petri Nets:Properties,Analysis and Application.[C]. Proceedings of the IEEE,Apr.1989,77(4):541-580.
17. Rammig, F.; Rust, C. Modeling of dynamically modifiable embedded real-time systems[C].Object-Oriented Real-Time Dependable Systems, 2003. WORDS 2003 Fall. Proceedings. Ninth IEEE International Workshop on 1-3 Oct. 2003 Page(s):28– 34
18. Zonghua Gu, Kang G Shin. An Integrated Approach toModeling and Analysis of Embedded Real2time Systems Based on Timed Petri Nets [ C ]. Washington D C: IEEE Computer Society, 2003. 3502359.
19. Costa, A.; Gomes, L. Petri net Splitting Operation within Embedded Systems Co-design[C]. Industrial Informatics, 2007 5th IEEE International Conference on Volume 1, 23-27 June 2007 Page(s):503– 508
20. Z Peng,K Kuchcinski. Automated Transformation of Algorithms into Register-Transfer lever Implementations[C].IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems,Feb. 1994,13(2):150-160
21. Esser, R. An object oriented Petri net language for embedded system design.[C]Software Technology and Engineering Practice, 1997. Proceedings., Eighth IEEE International Workshop on [incorporating Computer Aided Software Engineering] 14-18 July 1997 Page(s):216– 223
22. L A Cortes,P Eles,Z Peng. A Petri Net Based Model for Heterogeneous Embedded Systems[C]. IEEE Norchip Conference,Nov.1999:248-255
23.张海涛.嵌入式系统的设计及应用[M].北京:科学出版社,2007.58-81
24.张海涛.基于Petri网的分布式实时嵌入式系统调度的建模[J].计算机工程,2006,32(18):6-8
25.廖晓文.面向对象的Petri网在嵌入式系统开发中的应用[J].微型机与应用,2005(4)
26. S. Edwards, L. Lavagno, E.A. Lee, A. Sangiovanni-Vicentelli, Design of embedded systems: formal models,validation, and synthesis[C]. Proc. IEEE 85 (1997) 366–390.
27. D. Harel. Statecharts: A visual formalism for complex systems, Science of ComputerProgramming 8 (3) (1987) 231–274.
28. E.A. Lee, T.M. Parks, Dataflow process networks[C]. Proc.IEEE 83 (5) (1995) 773–799.
29.袁崇义. Petri网原理与应用[M].电子工业出版社,1998
30. Leandro Dias da Silva , Angelo Perkusich. A Model-Based Approach to Formal Specification and Verification of Embedded Systems Using Colored Petri Nets[C]. Atkinson et al. (Eds.): Component-Based Software Development, LNCS 3778, pp. 35–58, 2005.
31. Varea M,Hashimi B A. Dual Transitions Petri Net Based Modeling Technique for Embedded Systems Specification[C].In:Proceeding of the 4th Design,Automation and Test in Europe(DATE),Munich,Germany,2001,566- 571.
32. L.A. Cortes, P. Eles, Z. Peng, Definitions of equivalence for transformational synthesis of embedded systems[C] in:Proc. ICECCS, 2000, pp. 134–142.
33. L.A. Cortes, P. Eles, Z. Peng. Hierarchical modeling and verification of embedded systems[J] in: Proc. Euromicro Symposium on Digital System Design, 2001, pp. 63–70.
34. Gomes, L.; Barros, J.P. On structuring mechanisms for Petri nets based system design[C].Emerging Technologies and Factory Automation, 2003. Proceedings. ETFA '03. IEEE Conference Volume 2, 16-19 Sept. 2003 Page(s):431 - 438 vol.2
35. P. Tarr, H. Ossher, W. Harrison, and J. Stanley M. Sutton. N Degrees of Separation: Multi-Dimensional Separation of Concerns[C]. In Proceedings of the 21st international conference on Software engineering, pages 107–119. IEEE Computer Society Press, 1999.
36. E. Smith. Arbiter Behaviour and Petri Nets[J]. Fachberichte Informatik, Universit¨at Koblenz-Landau, 2/93, 1993.
37. L. Gomes and A. Steiger-Garc??ao. Towards the Implementation of Conflict Resolution on a Non Autonomous High-Level Petri Net Model[C]. In Workshop Manufacturing and Petri Nets, Osaka, Japan, jun 1996. Satellite workshop of the 17th International Conference on Application and Theory of Petri Nets (ICATPN’96).
38. Cortes. L.A., Eles. P., Peng. Z. Formal coverification of embedded systems using model checking[C].Euromicro Conference, 2000. Proceedings of the 26th Volume 1, 5-7 Sept. 2000 Page(s):106 - 113 vol.1
39. R. Alur, C. Courcoubetis, D.L. Dill. Model checking for real-time systems[C] in: Proc. Symposium on Logic in Computer Science, 1990, pp. 414–425
40. Johan Bengtsson, Kim G. Larsen, Fredrik Larsson,Paul Pettersson, and Wang Yi. Uppaal– a tool suite for automatic verification of real-time systems[C]. In Proceedings of Workshop on Verification and Control of Hybrid Systems III, pages 232–243, October 1995
41. T. Henzinger, P. Ho, and H. Wong-Toi. Kronos:A verification tool for real-time systems[J]. Software Tools for Technology Transfer, 1, 1997.
42. E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications.[J] ACM Transactions on Programming Languages and Systems 8 (2) (1986) 244–263
43. R. Alur and D. L. Dill. A theory of timed automata[J].Theoretical Computer Science, 126:183–235, 1994.
44. Johan Bengtsson, Fredrik Larsson. Uppaal A Tool for Automatic Verification of Real-time Systems [ D ]. Sweden: Upp sala University,1996. 1269.
45. Johan Bengtsson, Kim GLarsen, Fredrik Larsson, et al. UPPAAL: A Tool Suite for Automatic Verification of Real-time Systems [M ]. New York: Springer-Verlag, 1996. 232-243.
46. WANG YI,PAUL PETTERSSON,MATS DANIELS. Automatic verification of real—time communicating systems by constraint solving:proceedings of the 7th International Conference on Formal Description Techniques,North Holland[C] Sweden:Es.n.J,1994:223-238
47. R. Gerber and I. Lee. A layered approach to automating the verification of real-time systems[C].IEEE Transactions on Software Engineering,18(9):768–784, 1992.
48. E. Filippi, L. Lavagno, L. Licciardi, A. Montanaro, M. Paolini,R. Passerone, M. Sgroi, and A. Sangiovanni-Vincentelli. Intellectual Property Re-use in Embedded System CO-design: an Industrial Case Study.[C] in Proc. ISSS, 1998, pp. 37-42.
2. Luis AlejandroC. Modeling and formal verifieation of embeddeds on a Petri net representation[J].Systems Architecture,2003,49:571-589.
3. Daniel D ajski,Frank Vahid,Sanjiv Narayan等.边计年,吴为民译.嵌入式系统的描述与设计[M].北京:机械工业出版社,2005
4. Trong-Yen Lee; Pao-Ann Hsiung. Embedded software synthesis and prototyping[C]. Consumer Electronics, IEEE Transactions on Volume 50, Issue 1, Feb 2004 Page(s):386– 392
5. Gomes L,Costa A .Petri nets as supporting formalism within Embedded Systems Co-design[C]. International Symposium on Industrial Embedded Systems ,2006:1– 4
6.郭军.基于Petri网的嵌入式系统高层级设计方法与技术研究[博士论文].西北大学.2007:20-31
7.廖晓文.基于UML与Petri网的嵌入式系统建模方法的研究[硕士论文].广东工业大学.2005:1-3
8. Pettit. R.G., Gomaa. H. Analyzing Behavior of Concurrent Software Designs for Embedded Systems[C]. Object and Component-Oriented Real-Time Distributed Computing, 2007. ISORC '07. 10th IEEE International Symposium on 7-9 May 2007 Page(s):124– 132
9. Pimentel. J.R. Safety-reliability of distributed embedded system fault tolerant units[C]. Industrial Electronics Society, 2003. IECON '03. The 29th Annual Conference of the IEEE Volume 1, 2-6 Nov. 2003 Page(s):945 - 950 vol.1
10. Gomes, L.; Lourenco, J. Petri nets-based automatic generation GUI tools for embedded systems[C].Human System Interactions, 2008 Conference on 25-27 May 2008 Page(s):269– 274
11. Cortes, L.A.; Eles, P.; Peng, Z.Verification of embedded systems using a Petri net based representation[C].System Synthesis, 2000. Proceedings. The 13th International Symposium on 20-22 Sept. 2000 Page(s):149– 155
12. Gomes. L., Barros. J.P., Costa. A., Pais. R., Moutinho. F. Towards usage of formal methods within embedded systems co-design[C].Emerging Technologies and Factory Automation, 2005. ETFA 2005. 10th IEEE Conference on Volume 1, 19-22 Sept. 2005 Page(s):4 pp.– 284
13.王志英.嵌入式系统原理与设计[M].北京:高等教育出版社,2007.4-5
14. Claude Girault,Rudiger Valk .王生原等译.系统工程Petri网—建模、验证与应用指南[M].北京:电子工业出版社,2005
15. Liqiong Chen; Zhiqing Shao; Guisheng Fan; Xiuying Wang. Modeling and Analyzing Distributed Real-time and Embedded Systems with High-Level Petri Nets[C].Mechtronic and Embedded Systems and Applications, 2008. MESA 2008. IEEE/ASME International Conference on 12-15 Oct. 2008 Page(s):476– 481
16. T murata. Petri Nets:Properties,Analysis and Application.[C]. Proceedings of the IEEE,Apr.1989,77(4):541-580.
17. Rammig, F.; Rust, C. Modeling of dynamically modifiable embedded real-time systems[C].Object-Oriented Real-Time Dependable Systems, 2003. WORDS 2003 Fall. Proceedings. Ninth IEEE International Workshop on 1-3 Oct. 2003 Page(s):28– 34
18. Zonghua Gu, Kang G Shin. An Integrated Approach toModeling and Analysis of Embedded Real2time Systems Based on Timed Petri Nets [ C ]. Washington D C: IEEE Computer Society, 2003. 3502359.
19. Costa, A.; Gomes, L. Petri net Splitting Operation within Embedded Systems Co-design[C]. Industrial Informatics, 2007 5th IEEE International Conference on Volume 1, 23-27 June 2007 Page(s):503– 508
20. Z Peng,K Kuchcinski. Automated Transformation of Algorithms into Register-Transfer lever Implementations[C].IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems,Feb. 1994,13(2):150-160
21. Esser, R. An object oriented Petri net language for embedded system design.[C]Software Technology and Engineering Practice, 1997. Proceedings., Eighth IEEE International Workshop on [incorporating Computer Aided Software Engineering] 14-18 July 1997 Page(s):216– 223
22. L A Cortes,P Eles,Z Peng. A Petri Net Based Model for Heterogeneous Embedded Systems[C]. IEEE Norchip Conference,Nov.1999:248-255
23.张海涛.嵌入式系统的设计及应用[M].北京:科学出版社,2007.58-81
24.张海涛.基于Petri网的分布式实时嵌入式系统调度的建模[J].计算机工程,2006,32(18):6-8
25.廖晓文.面向对象的Petri网在嵌入式系统开发中的应用[J].微型机与应用,2005(4)
26. S. Edwards, L. Lavagno, E.A. Lee, A. Sangiovanni-Vicentelli, Design of embedded systems: formal models,validation, and synthesis[C]. Proc. IEEE 85 (1997) 366–390.
27. D. Harel. Statecharts: A visual formalism for complex systems, Science of ComputerProgramming 8 (3) (1987) 231–274.
28. E.A. Lee, T.M. Parks, Dataflow process networks[C]. Proc.IEEE 83 (5) (1995) 773–799.
29.袁崇义. Petri网原理与应用[M].电子工业出版社,1998
30. Leandro Dias da Silva , Angelo Perkusich. A Model-Based Approach to Formal Specification and Verification of Embedded Systems Using Colored Petri Nets[C]. Atkinson et al. (Eds.): Component-Based Software Development, LNCS 3778, pp. 35–58, 2005.
31. Varea M,Hashimi B A. Dual Transitions Petri Net Based Modeling Technique for Embedded Systems Specification[C].In:Proceeding of the 4th Design,Automation and Test in Europe(DATE),Munich,Germany,2001,566- 571.
32. L.A. Cortes, P. Eles, Z. Peng, Definitions of equivalence for transformational synthesis of embedded systems[C] in:Proc. ICECCS, 2000, pp. 134–142.
33. L.A. Cortes, P. Eles, Z. Peng. Hierarchical modeling and verification of embedded systems[J] in: Proc. Euromicro Symposium on Digital System Design, 2001, pp. 63–70.
34. Gomes, L.; Barros, J.P. On structuring mechanisms for Petri nets based system design[C].Emerging Technologies and Factory Automation, 2003. Proceedings. ETFA '03. IEEE Conference Volume 2, 16-19 Sept. 2003 Page(s):431 - 438 vol.2
35. P. Tarr, H. Ossher, W. Harrison, and J. Stanley M. Sutton. N Degrees of Separation: Multi-Dimensional Separation of Concerns[C]. In Proceedings of the 21st international conference on Software engineering, pages 107–119. IEEE Computer Society Press, 1999.
36. E. Smith. Arbiter Behaviour and Petri Nets[J]. Fachberichte Informatik, Universit¨at Koblenz-Landau, 2/93, 1993.
37. L. Gomes and A. Steiger-Garc??ao. Towards the Implementation of Conflict Resolution on a Non Autonomous High-Level Petri Net Model[C]. In Workshop Manufacturing and Petri Nets, Osaka, Japan, jun 1996. Satellite workshop of the 17th International Conference on Application and Theory of Petri Nets (ICATPN’96).
38. Cortes. L.A., Eles. P., Peng. Z. Formal coverification of embedded systems using model checking[C].Euromicro Conference, 2000. Proceedings of the 26th Volume 1, 5-7 Sept. 2000 Page(s):106 - 113 vol.1
39. R. Alur, C. Courcoubetis, D.L. Dill. Model checking for real-time systems[C] in: Proc. Symposium on Logic in Computer Science, 1990, pp. 414–425
40. Johan Bengtsson, Kim G. Larsen, Fredrik Larsson,Paul Pettersson, and Wang Yi. Uppaal– a tool suite for automatic verification of real-time systems[C]. In Proceedings of Workshop on Verification and Control of Hybrid Systems III, pages 232–243, October 1995
41. T. Henzinger, P. Ho, and H. Wong-Toi. Kronos:A verification tool for real-time systems[J]. Software Tools for Technology Transfer, 1, 1997.
42. E.M. Clarke, E.A. Emerson, A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications.[J] ACM Transactions on Programming Languages and Systems 8 (2) (1986) 244–263
43. R. Alur and D. L. Dill. A theory of timed automata[J].Theoretical Computer Science, 126:183–235, 1994.
44. Johan Bengtsson, Fredrik Larsson. Uppaal A Tool for Automatic Verification of Real-time Systems [ D ]. Sweden: Upp sala University,1996. 1269.
45. Johan Bengtsson, Kim GLarsen, Fredrik Larsson, et al. UPPAAL: A Tool Suite for Automatic Verification of Real-time Systems [M ]. New York: Springer-Verlag, 1996. 232-243.
46. WANG YI,PAUL PETTERSSON,MATS DANIELS. Automatic verification of real—time communicating systems by constraint solving:proceedings of the 7th International Conference on Formal Description Techniques,North Holland[C] Sweden:Es.n.J,1994:223-238
47. R. Gerber and I. Lee. A layered approach to automating the verification of real-time systems[C].IEEE Transactions on Software Engineering,18(9):768–784, 1992.
48. E. Filippi, L. Lavagno, L. Licciardi, A. Montanaro, M. Paolini,R. Passerone, M. Sgroi, and A. Sangiovanni-Vincentelli. Intellectual Property Re-use in Embedded System CO-design: an Industrial Case Study.[C] in Proc. ISSS, 1998, pp. 37-42.