基于IEC61499标准的组件化模型集成数控系统形式化建模与验证的研究
|
摘要
随着信息技术与机械工业的高速发展与紧密结合,装备制造业作为我国工业发展的排头兵与核心力量,已经成为我国实现工业现代化的关键领域。加快发展装备制造业的核心技术,大力开发先进制造技术,尤其针对高档数控机床的控制中枢——计算机数控系统(Computer Numerical Control Systems, CNC Systems)的设计与开发,正朝着柔性化、智能化和网络化的方向发展。如何保证数控系统的开发在不牺牲大量时间和资源的前提下,能够达到高效、可靠和完备的特点,这需要一种面向数控系统开发方法论的革新。本文摒弃了数控系统的传统开发方法,借鉴组件化模型集成开发方法,采用IEC 61499标准的组件库和形式化方法,建立一套面向嵌入式数控系统建模和验证的形式化开发方法,为数控系统的开发提供安全、快速和有效的解决方案。在对组件化模型集成方法和形式化方法进行深入研究的基础上,针对数控系统的领
域特性和系统需求,提出了面向嵌入式数控系统的形式化框架。整个框架包括两个部分:形式化建模框架和形式化验证框架。形式化建模框架从已构建形成的组件化模型集成数控系统的领域模型出发,通过构造面向数控系统的形式化建模语言(CNC Formal Modeling Language,CNCFML),实现领域模型到形式化模型的模型转换。形式化验证框架通过形式化描述语言,对系统特性进行形式化规约,产生系统相关性质的形式化描述,与形式化模型一起进行模型检验,以检验系统设计模型是否满足功能和性能需求。
针对数控系统的形式化建模框架,结合IEC 61499层次化建模思想和形式化描述方法,将领域模型中文字式或图形化的组件定义为具有精确语法和语义的形式化模型,实现对组件和组件间交互方式清晰、无歧义的描述,以满足系统在执行过程中组件动态行为的确定性和一致性。另外,通过设计领域模型到CNCFML的语法指定、CNCFML的语法语义锚和CNCFML到形式化模型的语义指定,完成领域模型到形式化模型的转换,有利于系统模型层的形式化仿真和验证。
针对数控系统的形式化验证框架,提出一种基于功能验证的输入输出函数和基于性能验证的计算树逻辑(Computation Tree Logic,CTL)集成的数控系统描述语言(CNC Formal Specification Language,CNCFSL),用来描述应用模型的功能需求和系统模型的非功能属性需求,并联系形式化建模框架中应用和系统的形式化模型,完成基于Ptolemy II工具中应用的功能仿真和基于UPPAAL工具中系统的非功能属性验证。
最后,采用所设计研究的数控系统的形式化框架、建模语言和验证方法,给出了两个开发实例:钻孔检测一体机和数控平面切割机控制系统。在基于IEC 61499的模型集成环境CORFU上构造系统的领域模型,通过CNCFML的语义指定生成相应的形式化模型作为领域模型中各层的语义模型,并在Ptolemy II上构造应用的形式化模型,在UPPAAL上构造系统的形式化模型,通过在相应工具上的仿真验证,验证了系统模型在运行过程中满足诸多系统需求,从而论证了本文提出的形式化建模与验证方法论适用于多功能、高性能嵌入式数控系统的开发。
本文提出的嵌入式数控系统的形式化框架、形式化建模语言以及形式化仿真验证方法是将形式化方法和组件化模型集成开发方法应用在数控领域的一个尝试。对该方法的深入研究可能为嵌入式控制系统的需求描述、模型设计以及代码产生和实施等开发过程提供快速、高效和可靠的开发模式和研究途径,并有利于系统中组件的可复用性和可重配置性,对提升我国装备制造业的先进制造技术具有重大意义。
With the rapid development and tight connection of information technology and mechanical industry, equipment manufacture as the leader and core of industry development has been the critical area to realize the modernization of industry in China. To speed up the core techniques of equipment manufacture and develop the advanced manufacturing technology, computer numerical control systems as the pivot of the high-grade NC machine tools is developing at the flexibility, intelligence and networks. How to guarantee the CNC systems development efficient, responsible and complete, while not to waste a lot of time and money needs the innovation for the development approaches of CNC systems. The traditional development methods of CNC systems have been thrown out, while a formal modeling and verification approach for embedded CNC systems is built up with IEC 61499 and formal methods through the component-based model integrated development method to provide the safe, fast and effective development solution for the CNC systems.
The component-based model integrated method and formal methods have been studied in detail. Aiming to the domain specific characteristics and demands, the formal framework for embedded CNC sytems is proposed. The whole framework can be divided into two parts, i.e. the formal modeling framework and the formal verification framework. The formal modeling framework is established by a CNC formal modeling language from the completed CNC domain specific models to attain the formal models of CNC systems. The formal verification framework is to specify the characteristics of systems in a formal way through a formal specification language, to produce the formal specification of the system properties and to combine the formal models into model checking to check whether the formal models are satisfied with the functionality and performance demands of CNC systems.
Aiming to the formal modeling framework of CNC systems, the literal or graphic components of the domain specific models are defined by the formal models with explicit syntax and semantics through the hierarchical modeling thoughts of IEC 61499 and formal specification methods to realize the clear and unambiguous specification for components and the interaction rules between components and even to satisfy the determinacy and consistency of the components dynamic behaviors during the execution process of systems. Besides, the syntax assignment from the domain specific models to CNCFML, the anchor of syntax and semantics in CNCFML and the semantics assignment from CNCFML to the formal models are defined in detail to complete the model transformation from the domain specific models to the formal models to facilitate the simulation and formal verification in the model layer of the CNC systems.
Aiming to the formal verification framework, a CNC formal specification language integrated with the input-output function based on the functionality verification and the computation tree logic based on the performance verification is advanced to describe the functionality requirements of application and the non-functionality requirements of system. The combination of the formal models and formal specifications can be used to simulate the functionality of the application on the Ptolemy II and verify the non-functionality properties of the system on UPPAAL.
Lastly, the two development cases are given by the developed formal framework, CNCFML and the formal verification methods, i.e. drilling test equipment and CNC cutter control systems. The domain specific models are built up on the CORFU which is the model integrated environment based on IEC 61499. Applying with the semantics assignment, the formal models as the semantic models in the each layer of the domain specific models are generated. The formal models of the application are constructed on the Ptolemy II and the formal models of the system are constituted on the UPPAAL. Then the formal models are checked on the responding tools to verify the requirements of systems during the execution process. In the end, the formal modeling and verification approach has been demonstrated to be suitable for the development of the multi functions and high performance CNC systems.
This dissertation attempts to introduce the formal methods and component-based model integrated methods into the CNC systems by proposing the formal framework, CNCFML and the formal verification methods. Further research will probably provide the fast, efficient and responsible development pattern and solutions for the requirements specification, model design, code generation and implementation of the embedded control systems. And it’s helpful for the reusability and reconfiguration of components. This effort is important to enhance the level of the advanced manufacturing technology in equipment manufacture area.
域特性和系统需求,提出了面向嵌入式数控系统的形式化框架。整个框架包括两个部分:形式化建模框架和形式化验证框架。形式化建模框架从已构建形成的组件化模型集成数控系统的领域模型出发,通过构造面向数控系统的形式化建模语言(CNC Formal Modeling Language,CNCFML),实现领域模型到形式化模型的模型转换。形式化验证框架通过形式化描述语言,对系统特性进行形式化规约,产生系统相关性质的形式化描述,与形式化模型一起进行模型检验,以检验系统设计模型是否满足功能和性能需求。
针对数控系统的形式化建模框架,结合IEC 61499层次化建模思想和形式化描述方法,将领域模型中文字式或图形化的组件定义为具有精确语法和语义的形式化模型,实现对组件和组件间交互方式清晰、无歧义的描述,以满足系统在执行过程中组件动态行为的确定性和一致性。另外,通过设计领域模型到CNCFML的语法指定、CNCFML的语法语义锚和CNCFML到形式化模型的语义指定,完成领域模型到形式化模型的转换,有利于系统模型层的形式化仿真和验证。
针对数控系统的形式化验证框架,提出一种基于功能验证的输入输出函数和基于性能验证的计算树逻辑(Computation Tree Logic,CTL)集成的数控系统描述语言(CNC Formal Specification Language,CNCFSL),用来描述应用模型的功能需求和系统模型的非功能属性需求,并联系形式化建模框架中应用和系统的形式化模型,完成基于Ptolemy II工具中应用的功能仿真和基于UPPAAL工具中系统的非功能属性验证。
最后,采用所设计研究的数控系统的形式化框架、建模语言和验证方法,给出了两个开发实例:钻孔检测一体机和数控平面切割机控制系统。在基于IEC 61499的模型集成环境CORFU上构造系统的领域模型,通过CNCFML的语义指定生成相应的形式化模型作为领域模型中各层的语义模型,并在Ptolemy II上构造应用的形式化模型,在UPPAAL上构造系统的形式化模型,通过在相应工具上的仿真验证,验证了系统模型在运行过程中满足诸多系统需求,从而论证了本文提出的形式化建模与验证方法论适用于多功能、高性能嵌入式数控系统的开发。
本文提出的嵌入式数控系统的形式化框架、形式化建模语言以及形式化仿真验证方法是将形式化方法和组件化模型集成开发方法应用在数控领域的一个尝试。对该方法的深入研究可能为嵌入式控制系统的需求描述、模型设计以及代码产生和实施等开发过程提供快速、高效和可靠的开发模式和研究途径,并有利于系统中组件的可复用性和可重配置性,对提升我国装备制造业的先进制造技术具有重大意义。
With the rapid development and tight connection of information technology and mechanical industry, equipment manufacture as the leader and core of industry development has been the critical area to realize the modernization of industry in China. To speed up the core techniques of equipment manufacture and develop the advanced manufacturing technology, computer numerical control systems as the pivot of the high-grade NC machine tools is developing at the flexibility, intelligence and networks. How to guarantee the CNC systems development efficient, responsible and complete, while not to waste a lot of time and money needs the innovation for the development approaches of CNC systems. The traditional development methods of CNC systems have been thrown out, while a formal modeling and verification approach for embedded CNC systems is built up with IEC 61499 and formal methods through the component-based model integrated development method to provide the safe, fast and effective development solution for the CNC systems.
The component-based model integrated method and formal methods have been studied in detail. Aiming to the domain specific characteristics and demands, the formal framework for embedded CNC sytems is proposed. The whole framework can be divided into two parts, i.e. the formal modeling framework and the formal verification framework. The formal modeling framework is established by a CNC formal modeling language from the completed CNC domain specific models to attain the formal models of CNC systems. The formal verification framework is to specify the characteristics of systems in a formal way through a formal specification language, to produce the formal specification of the system properties and to combine the formal models into model checking to check whether the formal models are satisfied with the functionality and performance demands of CNC systems.
Aiming to the formal modeling framework of CNC systems, the literal or graphic components of the domain specific models are defined by the formal models with explicit syntax and semantics through the hierarchical modeling thoughts of IEC 61499 and formal specification methods to realize the clear and unambiguous specification for components and the interaction rules between components and even to satisfy the determinacy and consistency of the components dynamic behaviors during the execution process of systems. Besides, the syntax assignment from the domain specific models to CNCFML, the anchor of syntax and semantics in CNCFML and the semantics assignment from CNCFML to the formal models are defined in detail to complete the model transformation from the domain specific models to the formal models to facilitate the simulation and formal verification in the model layer of the CNC systems.
Aiming to the formal verification framework, a CNC formal specification language integrated with the input-output function based on the functionality verification and the computation tree logic based on the performance verification is advanced to describe the functionality requirements of application and the non-functionality requirements of system. The combination of the formal models and formal specifications can be used to simulate the functionality of the application on the Ptolemy II and verify the non-functionality properties of the system on UPPAAL.
Lastly, the two development cases are given by the developed formal framework, CNCFML and the formal verification methods, i.e. drilling test equipment and CNC cutter control systems. The domain specific models are built up on the CORFU which is the model integrated environment based on IEC 61499. Applying with the semantics assignment, the formal models as the semantic models in the each layer of the domain specific models are generated. The formal models of the application are constructed on the Ptolemy II and the formal models of the system are constituted on the UPPAAL. Then the formal models are checked on the responding tools to verify the requirements of systems during the execution process. In the end, the formal modeling and verification approach has been demonstrated to be suitable for the development of the multi functions and high performance CNC systems.
This dissertation attempts to introduce the formal methods and component-based model integrated methods into the CNC systems by proposing the formal framework, CNCFML and the formal verification methods. Further research will probably provide the fast, efficient and responsible development pattern and solutions for the requirements specification, model design, code generation and implementation of the embedded control systems. And it’s helpful for the reusability and reconfiguration of components. This effort is important to enhance the level of the advanced manufacturing technology in equipment manufacture area.
引文
[1]张相木.“十二五”期间我国装备制造业发展重点及面临机遇[EB/OL]. http://chinaneast.xinhuanet.com/jszb/2009-02/10/content_15648497.htm
[2]国务院关于加快振兴装备制造业的若干意见[EB/OL]. 2006. http://www.gov.cn/jrzg/2006-06/29/content_322286.htm.
[3]李宏伟.开放式数控系统分布式体系结构及其实现策略的研究[D].天津:天津大学, 2005.
[4]吕伯平.机床数控技术及应用[M].北京:北京大学, 2005.
[5]张吉堂,刘永姜,王爱玲等.现代数控原理及控制系统[M].北京:国防工业出版社, 2009.
[6]冷洪滨.高性能数控系统若干关键技术的研究[D].浙江:浙江大学, 2008.
[7]李方.基于模型集成的嵌入式数控系统设计关键技术研究[D].广州:华南理工大学, 2010.
[8] Rastofer, U., Bellosa, F. Component-based software engineering for distributed embedded real-time systems Software [C]. IEEE Proceedings Software Engineering, 2001, 148(3), pp: 99 -103.
[9]陈友东,陈五一,王田苗.基于组件的开放结构数控系统[J].机械工程学报. 2006, 42(6), pp: 188-192.
[10] Wang S. G, Shin K. Reconfigurable Software for Open Architecture Controllers [C]. Proceedings of the 2001 IEEE International Conference on Robotics & Automation, 2001 Seoul, Korea, pp: 4090-4095.
[11] Wang S.G., Kang. S. Modeling Manufacturing Control Software. Proceedings of the 2001 IEEE International Conference on Robotics & Automation, 2001, Seoul, Korea, pp: 4072-4077.
[12] Wang S. G., Shin. K. An Architecture for Embedded Software Integration Using Reusable Components [J]. Synthesis for Embedded Systems, ACM Press, 2000, pp: 110-118.
[13] Thramboulidis K, Doukas G, Frantzis A. Towards an Implementation Model for FB-based Reconfigurahle Distributed Control Applications [C]. 7th International Symposium on Object-oriented Real-time Distributed Computing, Viena, Austria, 2004.
[14] Thramboulidis K, Perdikis D, Kantas S. Model Driven Development of Function Block Based Distributed Control Applications [C]. 16 th IFAC World Conference, Prague, 2005.
[15] Thramboulidis K. Challenges in the Development of Mechatronic Systems: The Mechatronic Component [C]. 13th IEEE International Conference on Emerging Technologies and Factory Automation, 2008, Germany, pp: 624-631.
[16] Angelov C, Xu K, Sierszecki K. A Component-Based Framework for Distributed Control Systems [C]. Proceeding of the 32nd Euromicro Conference on Software Engineering and Advanced Applications, Cavtat-Dubrovnik, Croatia, 2006.
[17] Angelov C, Sierszecki K, Guo Y. Formal Design Models for Distributed Embedded Control Systems [C]. 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems. Denver, Colorado, USA, 2009.
[18] Angelov C, Sierszecki K, Marian N. Component-Based Design of Embedded Software: An Analysis of Design Issues [J]. Proceedings of FIDJI, 2004, pp: 1~11.
[19] COMDES Project. University of South Denmark [EB/OL]. http://seg.mci.sdu.dk/.
[20]李斌.基于构架/构件复用的开放式数控系统研究[D].武汉:华中科技大学, 2004.
[21]王恒,陈恳,刘顺涛.基于软件模式的开放结构控制器平台的研究[J].计算机集成制造系统, 2006, 12(3), pp: 46-50.
[22] International Electro-technical Commission(IEC). International Standard IEC 61499, Function Blocks, Part 1-Part 4[S]. IEC Jan. 2005.http://www.iec.ch/.
[23]Kleppe A., Warmer J., Bast W.解析MDA[M].鲍志云译.北京:人民邮电出版社, 2004.
[24] MARIN B., PASTOR O., ABRAN A. Towards an accurate functional size measurement procedure for conceptual models in an MDA environment [J]. Data & Knowledge Engineering, 2010, pp: 472-490.
[25] Function Blocks Development Kit. Holobloc Inc [EB/OL]. http://www.holobloc.com. July 2005.
[26] CORFU Project. University of Patras [EB/OL].http://seg.ee.upatras.gr/corfu/dev/ index.htm.
[27] Archimedes Project. University of Patras [EB/OL]. http://seg.ee.upatras.gr/mim/ ArchimedesESS.htm.
[28] 4DIAC Project. O3 Neida [EB/OL]. http://www.fordiac.org/10.0.html.
[29] Visser, P.M., Broenink, J.F. and Amerongen, J. van. Design trajectory and controller-plant interaction [J]. Embedded Systems Institute, 2006.
[30] Jovanovic, D. Designing Dependable Process-oriented Software– a CSP based approach [D]. PhD thesis, University of Twente, 2006.
[31] Matthijs H. ten Berge, Bojan Orlic etc. Co-Simulation of Networked Embedded Control Systems, a CSP-like process-oriented approach [C]. Proceedings of the 2006 IEEE Conference on Compunter Aided Control Systems Design, Germany, 2006.
[32] Edward A. Lee and Alberto S.V. A framework for comparing models of computation [J]. IEEE Trans. on Computer-Aided design of integrated circuit and systems , 1998, vol.17, pp.1217-1229.
[33] A. Jantsch and I. Sander. Models of computation and languages for embedded system design [C]. IEEE Proceedings-Computation Digit Technology, 2005, 152(2).
[34] Jie Liu. Responsible frameworks for heterogeneous modeling and design of embedded systems [D]. University of California, Berkeley, CA 94720, Dec. 20th, 2001.
[35] Ptolemy Project. University of California Berkeley [EB/OL]. http://ptolemy.eecs. berkeley.edu.
[36] Ledeczi A. The Generic Modeling Environment [C]. Workshop on Intelligent Signal Processing, Budapest, Hungary, 2001.
[37] DSM Project. http://www.dsmforum.org[EB/OL].
[38] ISIS Project. http://www.isis.vanderbilt.edu/projects/amt/default.asp[EB/OL].
[39] MIC Project. http://www.isis.vanderbilt.edu/research/mic.html[EB/OL].
[40] ESML. http://www.isis.vanderbilt.edu/projects/mobies [EB/OL].
[41]宋柱梅.基于模型集成运算的嵌入式装备控制系统开发方法的研究[D].广州:华南理工大学, 2007.
[42]李迪,李方,肖苏华等.面向计算机数控系统的领域建模设计和应用[J].计算机集成制造系统, 2010, 16(9), pp: 1820-1826.
[43] Li Di, Li Fang, and Huang Xin. A model based integration framework for computer numerical control system development [J]. Robotics and Computer-Integrated Manufacturing. 2010, 26 (4), pp: 333-343.
[44] Li Fang, Li Di, Huang Xin. Component-based model integration approach for computer numerical control system development [J]. Journal of Shanghai Jiao Tong University. 2010, 15(1), pp: 36-42.
[45] J Wan, D Li, H Yan, and P Zhang. Fuzzy feedback scheduling algorithm based on central processing unit utilization for a software-based computer numerical control system [J]. Journal of Engineering Manufacture, 2010, 224(7), pp: 1131-1143.
[46] Jiafu Wan, Di Li, and Ping Zhang. Key technology of embedded system implementation for software-based CNC system [J]. Chinese Journal of Mechanical Engineering, 2010,23(2), pp: 241-248.
[47] Vyatkin, V. The IEC 61499 standard and its semantics [J]. IEEE Ind. Electronics Magazine, 2009, 4(3), pp: 40-48.
[48]古天龙.软件开发的形式化方法[M].高等教育出版社, 2005.
[49] Ian Sommerville. Software Engineering (9th Edition) [M]. Addison Wesley, 2010.
[50] R. Johnson. Framework=(components+patterns) [M]. Communications of the ACM, 1997, 40(10), pp:39-42.
[51] R. Alur, C. Courcoubetis, and D. L. Dill. Model-checking for real-time systems [J]. Logic in Computer Science, 1990, pp: 414-425.
[52] R. Alur, and D. L. Dill. A Theory of Timed Automata [J]. Theoretical Computer Sciecne, 1994, 126(2), pp: 183-235.
[53] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking [M]. MIT Press, 1999.
[54] F. Wang. Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems [J]. Tools and Algorithms for the Construction and Analysis of Systems, 2000, 1785, pp: 142-156.
[55] F. Wang. Formal verification of timed systems: a survey and perspective [J]. Proceedings of the IEEE, 2004, 92(8), pp: 1283-1305.
[56] Jan Tretmans. Conformance Testing with Labelled Transition Systems: Implementation Relations and Test Generation [J]. Computer Networks and ISDN Systems, 1996, 29(1), pp: 49-79.
[57] Lien Y. E. Study of theoretical and practical aspects of transition systems [D]. University of California, Berkeley, 1972.
[58] Keller R. M. Formal verification of parallel programs [J]. Communications of the ACM, 1976, 19(7), pp: 371-383.
[59] Plotkin G. A structural approach to operational semantics [J]. Department of Computer Science Research Report DAIMI FN-19, Aarhus University: Technical Report DAIMI FN-19, 1981.
[60] J Tretmans. Model based testing with labeled transition systems [J]. Formal methods and testing, 2008, pp: 1-38.
[61] Hierons, R. M., Bogdanov and K., Bowen, J. P. etc. Using formal Specifications to support testing [J]. ACM computing surveys, 2009, 41(2), 1-76.
[62] Hall, A. Using formal methods to develop an ATC information system [J]. IEEE Software, 1996, 13(2), 66-76.
[63] Dehbonei, B. and Mejia, F. Formal development of safety-critical software systems inrailway signaling [J]. Applications of formal methods. Prentice-Hall, 1995.
[64] Easterbrook, S., Lutz, R. and Covington, R. etc. Experience using lightweight formal methods for requirements modeling [J]. IEEE Trans. on Software Eng. 1998, 24(1), 4-14.
[65] International Electro-technical Commission(IEC). International standard IEC 61131-3: programming controllers, 2nd edition [S]. Geneva, 2003.
[66] Thramboulidis, K. and Doukas, G. IEC 61499 execution model semantics [J]. Innovative Algorithms and Techniques in Automation, Ind. Electronics and Telecommunications, 2007, pp: 223–228.
[67]沈兵,黄健. Windows下的CNC实时多任务调度策略研究[J].机床与液压, 2002, 6, pp: 126-128.
[68]万加富.面向软数控系统的混合任务调度理论研究[D].广州:华南理工大学, 2008.
[69] F. Wang. Formal Verification of Timed Systems: A Survey and Perspective [J]. Proceedings of the IEEE, 2004, 92(8), pp: 1283-1305.
[70] D. D. Gajski, S. Abdi, A. Gerstlauer, and G. Schirner. Embedded System Design: Modeling, Synthesis, Verification [M]. Springer, ISBN 978-1-4419-0503-1, July 2009.
[71] T. Ball, B. Cook, V. Levin, and S. K. Rajamani. SLAM and static driver verifier: technology transfer of formal methods inside Microsoft [C]. In Proceedings of the Integrated Formal Methods, 2004, Canterbury, U.K, pp: 1-20.
[72] C. Heitmeyer and D. Mandrioli. Formal Methods for Real-Time Computing [M]. New York: Wiley, 1996.
[73] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking [M]. Cambridge, MA: MIT Press, 2001.
[74] Jonathan S. Ostroff. Formal methods for the specification and design of real-time safety critical systems [J]. Journal of Software System, 1992, 18(1), pp. 33–60.
[75] J. v. Benthem and A. T. Meulen. Handbook of Logic and Language [M]. Eds., North-Holland, 1997.
[76] E. M. Clarke, A. Fehnker, Z. Han, B. Krogh, O. Stursberg, and M. Theobald,. Verification of hybrid systems based on counter example guided abstraction refinement [J]. Lecture Notes in Computer Science, Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg, Germany, Springer-Verlag, 2003, vol. 2619, pp:192–207.
[77]林立.基于高阶逻辑系统HOL的数字硬件形式化验证[D].西安电子科技大学, 2005,(02).
[78]朱学仕.形式验证技术的应用研究[D].哈尔滨工程大学, 2005, vol. 1.
[79]李梦君,李舟军,陈火旺. SPVT:一个有效的安全协议验证工具[J],软件学报, 2006, vol. 4.
[80]董护斌.面向实时系统的实时区域时态逻辑: RRTL [D].西北大学, 2002.
[81] M. Archer. TAME: using PVS strategies for special-purpose theorem proving [J]. Annual of Mathematical Artificial Intelligence, 2001, 29(1/4), pp: 201–232.
[82]Mohamed H. Zaki, Sofiene Tahar, Guy Bois. Formal verification of analog and mixed signal designs: A survey. Microelectronics Journal [J], 2008, Vol.39, pp: 1395-1404.
[83] T. Kropf. Introduction to Formal Hardware Verification [M]. Springer, Berlin, 2000.
[84] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray. A Survey of Functional Verification through Hybrid Techniques [J]. Journal of IEEE Design & Test of Computers, March-April 2007.
[85] E. Allen Emerson. Temporal and Modal Logic [J]. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics 1990, J. van Leeuwen, ed., North-Holland Pub. Co./MIT Press, Pages 995-1072.
[86] M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic [M]. Cambridge University Press, 1993.
[87] M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: An Approach [J]. Kluwer Academic Publishers, June 2000.
[88]M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: ACL2 Case Studies [J]. Kluwer Academic Publishers, June 2000.
[89] D. Dill and S. Tasiran. Simulation meets Formal Verification [C]. Slides from a presentation at ICCAD 1999.
[90] D. Dill. What's Between Simulation and Formal Verification? [C]. Slides from a presentation by Prof. Dill, Stanford University at DAC'98.
[91] D. Dill. Formal Verification: Experiences and Future Prospects [C]. Slides from a presentation at POPL 1999.
[92] C.-J. H. Seger. An Introduction to Formal Verification [J]. Technical Report 92-13, UBC, Department of Computer Science, Vancouver, B.C., Canada, June 1992.
[93] E. M. Clarke and R. Kurshan. Computer-aided verification [J]. IEEE Spectrum, 1996, 33(6), pp: 61-67.
[94] E. M. Clarke and H. Schlingloff. Model checking [J]. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning (Volume II), chapter 24, Elsevier Publishers B.V., 2000, pp: 1635–1790.
[95] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic [J]. In Logic of Programs, volume 131 of Lecture Notes in Computer Science, Springer-Verlag, 1981, page, pp: 52-71.
[96] E. M. Clarke, E. A. Emerson and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications [J]. ACM Transactions on Programming Languages and Systems, 1986, 8(2), pp: 244–263.
[97] E. M. Clarke, O. Grumberg and K. Hamaguchi. Another look at LTL model checking [C]. 6th International Conference on Computer Aided Verification (CAV), 1994, volume 818 of Lecture Notes in Computer Science, pp: 415–427.
[98] E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan and L. A. Ness. Verification of the Future bus cache coherence protocol [C]. In 11th International Symposium on Computer Hardware Description Languages and their Applications, Kluwer Academic Publishers, 1993, pp: 5–20.
[99] E. M. Clarke, O. Grumberg and D. E. Long. Model checking and abstraction [J]. ACM Transactions on Programming Languages and Systems.1994, 16(5), pp:1512–1542.
[100] E. M. Clarke, O. Grumberg, K. L. McMillan and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking [C]. In 32nd ACM/IEEE Conference on Design Automation (DAC), 1995, pp: 427–432.
[101]杨军,葛海通,郑飞君,严晓浪.一种形式化验证方法:模型检验[J].浙江大学学报(理学版), 2006, 33(4), pp: 403-407.
[102] MCMILLAN K L. Symbolic Model Checking: An Approach to the State Explosion Problem [D]. Pittsburgh: Carnegie Mellon University, 1993.
[103] J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL—a tool suite for automatic verification of real-time systems [J]. In Lecture Notes in Computer Science & Hybrid Control Systems, Springer-Verlag, Heidelberg, Germany, 1996, vol. 1066, pp. 232–243.
[104] UPPAAL Project. Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark [EB/OL]. http://www.uppaal.org/.
[105] K. L. McMillan. Getting started with SMV [EB/OL]. Cadence Berkeley Labs, 1998.http://www.cs.indiana.edu/classes/p515/readings/smv/McMillan-tutorial.pdf.
[106] Holzmann GJ. The spin model checker [J]. IEEE Transaction on Software Engineering, 1997, 23(5), pp: 279~295.
[107] Spin Project. Bell Labs [EB/OL]. http://spinroot.com/spin/whatispin.html.
[108] T. A. Henzinger, P. H. Ho, and H. Wong Toi. HyTech: A Model Checker for Hybrid Systems [J]. Software Tools for Technology Transfer, 1997, Vol. 1, pp: 110-122.
[109] HyTech Project. The Donald O. Pederson Center for Electronic Systems Design [EB/OL]. http://embedded.eecs.berkeley.edu/research/hytech/.
[110] Sergio Yovine. Kronos: a verification tool for real-time systems [J]. International Journal on Software Tools for Technology Transfer, 1997, Vol. 1, pp: 15-27.
[111] Murphi Project. Prof. Ganesh Gopalakrishnan's research group [EB/OL]. http://verify.stanford.edu/dill/murphi.html.
[112] Yusuke Matsunaga, An efficient equivalence checker for combinational circuits, Proceedings of the 33rd annual conference on Design automation [C], Las Vegas, Nevada, United States, 1996, pp: 629-634.
[113] Paruthi, V., Kuehlmann, A. Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation [C]. Proceedings of the 2000 IEEE International Conference on Computer Design: VLSI in Computers & Processors, 2000, pp: 459-468.
[114] S. Reda, A. Salem. Combinational equivalence checking using Boolean satisfiability and binary decision diagrams [C]. Proceedings of the conference on Design, automation and test in Europe, Munich, Germany, 2001, pp: 122-126.
[115] E. W. Smith, D. L. Dill. Automatic formal verification of block cipher implementations [C]. Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, Portland, Oregon, 2008, pp: 1-7.
[116] Andreas Kuehlmann, Florian Krohm. Equivalence checking using cuts and heaps [C]. Proceedings of the 34th annual conference on Design automation, Anaheim, California, United States, 1997, pp: 263-268.
[117] Shi-Yu Huang, Kwant-Ting Cheng. Formal Equivaence Checking and Design DeBugging [J]. Kluwer Academic Publishers, Norwell, MA, 1998.
[118]周慧.计算树逻辑特性模式研究.计算机工程, 2009, 35(23), pp: 68-70.
[119] Huth M., Ryan M. Logic in Computer Science: Modeling and Reasoning about Systems [M]. New York, USA: MIT Press, 2004.
[120] Clarke E. M., Grumberg O., Peled D. A. Model Checking [M]. London, UK: Cambridge University Press, 1999.
[121] Havelund K., Mike L. J. Formal analysis of a space-craft controller using SPIN [J]. IEEE Transactions on Software Engineering, 2001, 27(8), pp: 749-765.
[122] Perrig A., Szewczyk R., Tygar J. D. SPINs: security protocols for sensor networks [J].Wireless Network, 2002, 8(5), pp: 521-534.
[123]黎升洪,缪淮扣,张新林.线性时态逻辑中的特性模式[J].计算机应用, 2006, 26(8), pp: 1912-1915.
[124]周从华,刘志锋.具有过去时态算子的计算树逻辑模型检测[J].计算机工程, 2007, 33(22), pp: 98-100.
[125] Ben-Ari M., Manna Z., Pnueli A. The temporal logic of branching time [J]. Acta Informatica, 1983, 20(1), pp: 207-226.
[126] McMilan K. L. Symbolic modeling checking [M]. Kluwer Academic Publishers, 1993.
[127] J. Eker, J. Janneck, Edward A. Lee and Jie Liu etc. Taming heterogeneity - the Ptolemy approach[C]. Proceedings of the IEEE, 2003, 91(1), pp:127-144.
[128] E. A. Lee and H. Zheng. Operational Semantics of Hybrid Systems[C]. Proceedings of Hybrid Systems: Computation and Control (HSCC) LNCS 3414, Zurich, Switzerland, March 9-11, 2005, pp: 25-53.
[129] E. A. Lee, H. Zheng. Leveraging Synchronous Language Principles for Heterogeneous Modeling and Design of Embedded Systems [C]. EMSOFT '07, 2007, Salzburg, Austria.
[130] M.-K. Leung, T. Mandl, E. A. Lee, E. Latronico, C. Shelton, S. Tripakis, and B. Lickly[C]. Scalable Semantic Annotation using Lattice-based Ontologies. ACM/IEEE 12th International Conference on Model Driven Engineering Languages and Systems (MODELS), Denver, CO, USA, 4-9 October, 2009.
[131] Christopher Brooks, Edward A. Lee. Ptolemy II - Heterogeneous Concurrent Modeling and Design in Java[C]. 11 February, 2010; Poster presented at the 2010 Berkeley EECS Annual Research Symposium (BEARS).
[132] Edward A. Lee and Stavros Tripakis. Modal Models in Ptolemy [C]. Proceedings of 3rd International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools (EOOLT 2010), October, 2010.
[133] John C. Eidson, Edward A. Lee, Slobodan Matic, Sanjit A. Seshia and Jia Zou. A Time-Centric Model for Cyber-Physical Applications [C]. Proceedings of 3rd International Workshop on Model Based Architecting and Construction of Embedded System (ACESMB 2010), pp. 21-35, October, 2010.
[134] E. A. Lee. Computing Needs Time [J]. Communications of the ACM, 2009, 52(5).
[135] X. Liu, E. A. Lee. CPO semantics of timed interactive actor networks [J]. Theoretical Computer Science, 2008, 409 (1), pp: 110-25.
[136] E. A. Lee, H. Zheng. Leveraging Synchronous Language Principles for HeterogeneousModeling and Design of Embedded Systems [C]. EMSOFT 2007, September 30-October 3, 2007, Salzburg, Austria.
[137] E. A. Lee. The Problem with Threads [J]. IEEE Computer, 2006, 39(5), pp: 33-42.
[138] Kyungmin Bae, Peter Csaba ?lveczky, Thomas Huining Feng, Stavros Tripakis. Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude [C]. ICFEM '09: Proceedings of the 11th International Conference on Formal Engineering Methods, 717-736, 9-12, December, 2009.
[139] Edward A. Lee, Xiaojun Liu, and Stephen Neuendorffer. Classes and inheritance in actor-oriented design [J]. ACM Transactions on Embedded Computing Systems (TECS), 2009, 8(4).
[140] Edward A. Lee. Heterogeneous Actor Modeling [C]. International Conference on Embedded Software (EMSOFT), Taipei, Taiwan, October, 2011.
[141] Christopher Brooks, Chihhong Cheng, Thomas Huining Feng, Edward A. Lee and Reinhard von Hanxleden. Model Engineering using Multimodeling [C]. 1st International Workshop on Model Co-Evolution and Consistency Management (MCCM '08), September 30, 2008.
[142]李琳,江志斌.基于UPPAAL的虚拟生产系统仿真[J].上海交通大学学报, 2006, 40(7), pp: 1140-1147.
[143]徐刚,吴智铭. FMS建模和形式化验证[J].系统仿真学报, 2004, 16(9), pp: 1914-1917.
[144] Behrmann, G., Larsen K. G., Moller O., David A., Pettersson P., Wang Yi. UPPAAL: present and future [C]. Proceedings of the 40th IEEE Conference on Decision and Control, 2001, Vol. 3, pp: 2881-2886.
[145] Havelund K., Skou A., Larsen K. G., Lund K. Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL [C]. Proceedings of the 18th IEEE Real-time Systems Symposium, 1997, pp: 2-13.
[146] Kim G. Larsen, Paul Pettersson and Wang Yi. UPPAAL in a Nutshell [J]. International Journal of Software Tools for Technology Transfer, 1997, 1(2).
[147] Holsapple C.W., Jacob V.S., Pakath, R., Zaveri, J.S. A genetics-based hybrid scheduler for generating static schedules in flexible manufacturing contexts [J]. IEEE Transactions on Systems, Man and Cybernetics, 1993, Vol. 23, pp: 953 -97.
[148] Cavalieri S., Mirabella O. A PN-based scheduler for a flexible semiconductor manufacturing system [C]. Proceedings of IEEE Conference on Emerging Technologiesand Factory Automation, 1996, Vol. 2, pp: 724 -729.
[149] Burns,A. How to verify a Safe Real-Time System: The Application of Model Checking and Timed Automata to the Production Cell Case Study [J]. Real-Time Systems, 2003, 24(2), pp: 135-151.
[150] R. Alur and D. L. Dill. A theory of timed automata [J]. Theoretical Computer Sciences, 1994, Vol. 126, pp: 183-235.
[151] Chen D. J, Torngren M. A Metrics System for Quantifying Operational Coupling in Embedded Computer Control Systems [C]. In Proceeding of EMSOFT’04, Pisa, Italy, 2004.
[152] Chen D. J, Torngren M. A systematic Approach for identifying Operational Relationships in Embedded Computer Control systems [C]. 30th Euromicro Conf. on component–based software engineering track, 2004.
[153] Cengic, G. and Akesson, K. On formal analysis of IEC 61499 applications, part A: Modeling. IEEE Trans. on Ind. Inf., 2010, 6(2), 136-144.
[154] Cengic, G. and Akesson, K. On formal analysis of IEC 61499 applications, part B: Execution Semantics. IEEE Trans. on Ind. Inf., 2010, 6(2), 145-154.
[2]国务院关于加快振兴装备制造业的若干意见[EB/OL]. 2006. http://www.gov.cn/jrzg/2006-06/29/content_322286.htm.
[3]李宏伟.开放式数控系统分布式体系结构及其实现策略的研究[D].天津:天津大学, 2005.
[4]吕伯平.机床数控技术及应用[M].北京:北京大学, 2005.
[5]张吉堂,刘永姜,王爱玲等.现代数控原理及控制系统[M].北京:国防工业出版社, 2009.
[6]冷洪滨.高性能数控系统若干关键技术的研究[D].浙江:浙江大学, 2008.
[7]李方.基于模型集成的嵌入式数控系统设计关键技术研究[D].广州:华南理工大学, 2010.
[8] Rastofer, U., Bellosa, F. Component-based software engineering for distributed embedded real-time systems Software [C]. IEEE Proceedings Software Engineering, 2001, 148(3), pp: 99 -103.
[9]陈友东,陈五一,王田苗.基于组件的开放结构数控系统[J].机械工程学报. 2006, 42(6), pp: 188-192.
[10] Wang S. G, Shin K. Reconfigurable Software for Open Architecture Controllers [C]. Proceedings of the 2001 IEEE International Conference on Robotics & Automation, 2001 Seoul, Korea, pp: 4090-4095.
[11] Wang S.G., Kang. S. Modeling Manufacturing Control Software. Proceedings of the 2001 IEEE International Conference on Robotics & Automation, 2001, Seoul, Korea, pp: 4072-4077.
[12] Wang S. G., Shin. K. An Architecture for Embedded Software Integration Using Reusable Components [J]. Synthesis for Embedded Systems, ACM Press, 2000, pp: 110-118.
[13] Thramboulidis K, Doukas G, Frantzis A. Towards an Implementation Model for FB-based Reconfigurahle Distributed Control Applications [C]. 7th International Symposium on Object-oriented Real-time Distributed Computing, Viena, Austria, 2004.
[14] Thramboulidis K, Perdikis D, Kantas S. Model Driven Development of Function Block Based Distributed Control Applications [C]. 16 th IFAC World Conference, Prague, 2005.
[15] Thramboulidis K. Challenges in the Development of Mechatronic Systems: The Mechatronic Component [C]. 13th IEEE International Conference on Emerging Technologies and Factory Automation, 2008, Germany, pp: 624-631.
[16] Angelov C, Xu K, Sierszecki K. A Component-Based Framework for Distributed Control Systems [C]. Proceeding of the 32nd Euromicro Conference on Software Engineering and Advanced Applications, Cavtat-Dubrovnik, Croatia, 2006.
[17] Angelov C, Sierszecki K, Guo Y. Formal Design Models for Distributed Embedded Control Systems [C]. 2nd International Workshop on Model Based Architecting and Construction of Embedded Systems. Denver, Colorado, USA, 2009.
[18] Angelov C, Sierszecki K, Marian N. Component-Based Design of Embedded Software: An Analysis of Design Issues [J]. Proceedings of FIDJI, 2004, pp: 1~11.
[19] COMDES Project. University of South Denmark [EB/OL]. http://seg.mci.sdu.dk/.
[20]李斌.基于构架/构件复用的开放式数控系统研究[D].武汉:华中科技大学, 2004.
[21]王恒,陈恳,刘顺涛.基于软件模式的开放结构控制器平台的研究[J].计算机集成制造系统, 2006, 12(3), pp: 46-50.
[22] International Electro-technical Commission(IEC). International Standard IEC 61499, Function Blocks, Part 1-Part 4[S]. IEC Jan. 2005.http://www.iec.ch/.
[23]Kleppe A., Warmer J., Bast W.解析MDA[M].鲍志云译.北京:人民邮电出版社, 2004.
[24] MARIN B., PASTOR O., ABRAN A. Towards an accurate functional size measurement procedure for conceptual models in an MDA environment [J]. Data & Knowledge Engineering, 2010, pp: 472-490.
[25] Function Blocks Development Kit. Holobloc Inc [EB/OL]. http://www.holobloc.com. July 2005.
[26] CORFU Project. University of Patras [EB/OL].http://seg.ee.upatras.gr/corfu/dev/ index.htm.
[27] Archimedes Project. University of Patras [EB/OL]. http://seg.ee.upatras.gr/mim/ ArchimedesESS.htm.
[28] 4DIAC Project. O3 Neida [EB/OL]. http://www.fordiac.org/10.0.html.
[29] Visser, P.M., Broenink, J.F. and Amerongen, J. van. Design trajectory and controller-plant interaction [J]. Embedded Systems Institute, 2006.
[30] Jovanovic, D. Designing Dependable Process-oriented Software– a CSP based approach [D]. PhD thesis, University of Twente, 2006.
[31] Matthijs H. ten Berge, Bojan Orlic etc. Co-Simulation of Networked Embedded Control Systems, a CSP-like process-oriented approach [C]. Proceedings of the 2006 IEEE Conference on Compunter Aided Control Systems Design, Germany, 2006.
[32] Edward A. Lee and Alberto S.V. A framework for comparing models of computation [J]. IEEE Trans. on Computer-Aided design of integrated circuit and systems , 1998, vol.17, pp.1217-1229.
[33] A. Jantsch and I. Sander. Models of computation and languages for embedded system design [C]. IEEE Proceedings-Computation Digit Technology, 2005, 152(2).
[34] Jie Liu. Responsible frameworks for heterogeneous modeling and design of embedded systems [D]. University of California, Berkeley, CA 94720, Dec. 20th, 2001.
[35] Ptolemy Project. University of California Berkeley [EB/OL]. http://ptolemy.eecs. berkeley.edu.
[36] Ledeczi A. The Generic Modeling Environment [C]. Workshop on Intelligent Signal Processing, Budapest, Hungary, 2001.
[37] DSM Project. http://www.dsmforum.org[EB/OL].
[38] ISIS Project. http://www.isis.vanderbilt.edu/projects/amt/default.asp[EB/OL].
[39] MIC Project. http://www.isis.vanderbilt.edu/research/mic.html[EB/OL].
[40] ESML. http://www.isis.vanderbilt.edu/projects/mobies [EB/OL].
[41]宋柱梅.基于模型集成运算的嵌入式装备控制系统开发方法的研究[D].广州:华南理工大学, 2007.
[42]李迪,李方,肖苏华等.面向计算机数控系统的领域建模设计和应用[J].计算机集成制造系统, 2010, 16(9), pp: 1820-1826.
[43] Li Di, Li Fang, and Huang Xin. A model based integration framework for computer numerical control system development [J]. Robotics and Computer-Integrated Manufacturing. 2010, 26 (4), pp: 333-343.
[44] Li Fang, Li Di, Huang Xin. Component-based model integration approach for computer numerical control system development [J]. Journal of Shanghai Jiao Tong University. 2010, 15(1), pp: 36-42.
[45] J Wan, D Li, H Yan, and P Zhang. Fuzzy feedback scheduling algorithm based on central processing unit utilization for a software-based computer numerical control system [J]. Journal of Engineering Manufacture, 2010, 224(7), pp: 1131-1143.
[46] Jiafu Wan, Di Li, and Ping Zhang. Key technology of embedded system implementation for software-based CNC system [J]. Chinese Journal of Mechanical Engineering, 2010,23(2), pp: 241-248.
[47] Vyatkin, V. The IEC 61499 standard and its semantics [J]. IEEE Ind. Electronics Magazine, 2009, 4(3), pp: 40-48.
[48]古天龙.软件开发的形式化方法[M].高等教育出版社, 2005.
[49] Ian Sommerville. Software Engineering (9th Edition) [M]. Addison Wesley, 2010.
[50] R. Johnson. Framework=(components+patterns) [M]. Communications of the ACM, 1997, 40(10), pp:39-42.
[51] R. Alur, C. Courcoubetis, and D. L. Dill. Model-checking for real-time systems [J]. Logic in Computer Science, 1990, pp: 414-425.
[52] R. Alur, and D. L. Dill. A Theory of Timed Automata [J]. Theoretical Computer Sciecne, 1994, 126(2), pp: 183-235.
[53] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking [M]. MIT Press, 1999.
[54] F. Wang. Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems [J]. Tools and Algorithms for the Construction and Analysis of Systems, 2000, 1785, pp: 142-156.
[55] F. Wang. Formal verification of timed systems: a survey and perspective [J]. Proceedings of the IEEE, 2004, 92(8), pp: 1283-1305.
[56] Jan Tretmans. Conformance Testing with Labelled Transition Systems: Implementation Relations and Test Generation [J]. Computer Networks and ISDN Systems, 1996, 29(1), pp: 49-79.
[57] Lien Y. E. Study of theoretical and practical aspects of transition systems [D]. University of California, Berkeley, 1972.
[58] Keller R. M. Formal verification of parallel programs [J]. Communications of the ACM, 1976, 19(7), pp: 371-383.
[59] Plotkin G. A structural approach to operational semantics [J]. Department of Computer Science Research Report DAIMI FN-19, Aarhus University: Technical Report DAIMI FN-19, 1981.
[60] J Tretmans. Model based testing with labeled transition systems [J]. Formal methods and testing, 2008, pp: 1-38.
[61] Hierons, R. M., Bogdanov and K., Bowen, J. P. etc. Using formal Specifications to support testing [J]. ACM computing surveys, 2009, 41(2), 1-76.
[62] Hall, A. Using formal methods to develop an ATC information system [J]. IEEE Software, 1996, 13(2), 66-76.
[63] Dehbonei, B. and Mejia, F. Formal development of safety-critical software systems inrailway signaling [J]. Applications of formal methods. Prentice-Hall, 1995.
[64] Easterbrook, S., Lutz, R. and Covington, R. etc. Experience using lightweight formal methods for requirements modeling [J]. IEEE Trans. on Software Eng. 1998, 24(1), 4-14.
[65] International Electro-technical Commission(IEC). International standard IEC 61131-3: programming controllers, 2nd edition [S]. Geneva, 2003.
[66] Thramboulidis, K. and Doukas, G. IEC 61499 execution model semantics [J]. Innovative Algorithms and Techniques in Automation, Ind. Electronics and Telecommunications, 2007, pp: 223–228.
[67]沈兵,黄健. Windows下的CNC实时多任务调度策略研究[J].机床与液压, 2002, 6, pp: 126-128.
[68]万加富.面向软数控系统的混合任务调度理论研究[D].广州:华南理工大学, 2008.
[69] F. Wang. Formal Verification of Timed Systems: A Survey and Perspective [J]. Proceedings of the IEEE, 2004, 92(8), pp: 1283-1305.
[70] D. D. Gajski, S. Abdi, A. Gerstlauer, and G. Schirner. Embedded System Design: Modeling, Synthesis, Verification [M]. Springer, ISBN 978-1-4419-0503-1, July 2009.
[71] T. Ball, B. Cook, V. Levin, and S. K. Rajamani. SLAM and static driver verifier: technology transfer of formal methods inside Microsoft [C]. In Proceedings of the Integrated Formal Methods, 2004, Canterbury, U.K, pp: 1-20.
[72] C. Heitmeyer and D. Mandrioli. Formal Methods for Real-Time Computing [M]. New York: Wiley, 1996.
[73] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking [M]. Cambridge, MA: MIT Press, 2001.
[74] Jonathan S. Ostroff. Formal methods for the specification and design of real-time safety critical systems [J]. Journal of Software System, 1992, 18(1), pp. 33–60.
[75] J. v. Benthem and A. T. Meulen. Handbook of Logic and Language [M]. Eds., North-Holland, 1997.
[76] E. M. Clarke, A. Fehnker, Z. Han, B. Krogh, O. Stursberg, and M. Theobald,. Verification of hybrid systems based on counter example guided abstraction refinement [J]. Lecture Notes in Computer Science, Tools and Algorithms for the Construction and Analysis of Systems. Heidelberg, Germany, Springer-Verlag, 2003, vol. 2619, pp:192–207.
[77]林立.基于高阶逻辑系统HOL的数字硬件形式化验证[D].西安电子科技大学, 2005,(02).
[78]朱学仕.形式验证技术的应用研究[D].哈尔滨工程大学, 2005, vol. 1.
[79]李梦君,李舟军,陈火旺. SPVT:一个有效的安全协议验证工具[J],软件学报, 2006, vol. 4.
[80]董护斌.面向实时系统的实时区域时态逻辑: RRTL [D].西北大学, 2002.
[81] M. Archer. TAME: using PVS strategies for special-purpose theorem proving [J]. Annual of Mathematical Artificial Intelligence, 2001, 29(1/4), pp: 201–232.
[82]Mohamed H. Zaki, Sofiene Tahar, Guy Bois. Formal verification of analog and mixed signal designs: A survey. Microelectronics Journal [J], 2008, Vol.39, pp: 1395-1404.
[83] T. Kropf. Introduction to Formal Hardware Verification [M]. Springer, Berlin, 2000.
[84] J. Bhadra, M. S. Abadir, L.-C. Wang, S. Ray. A Survey of Functional Verification through Hybrid Techniques [J]. Journal of IEEE Design & Test of Computers, March-April 2007.
[85] E. Allen Emerson. Temporal and Modal Logic [J]. Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics 1990, J. van Leeuwen, ed., North-Holland Pub. Co./MIT Press, Pages 995-1072.
[86] M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem-Proving Environment for Higher-Order Logic [M]. Cambridge University Press, 1993.
[87] M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: An Approach [J]. Kluwer Academic Publishers, June 2000.
[88]M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: ACL2 Case Studies [J]. Kluwer Academic Publishers, June 2000.
[89] D. Dill and S. Tasiran. Simulation meets Formal Verification [C]. Slides from a presentation at ICCAD 1999.
[90] D. Dill. What's Between Simulation and Formal Verification? [C]. Slides from a presentation by Prof. Dill, Stanford University at DAC'98.
[91] D. Dill. Formal Verification: Experiences and Future Prospects [C]. Slides from a presentation at POPL 1999.
[92] C.-J. H. Seger. An Introduction to Formal Verification [J]. Technical Report 92-13, UBC, Department of Computer Science, Vancouver, B.C., Canada, June 1992.
[93] E. M. Clarke and R. Kurshan. Computer-aided verification [J]. IEEE Spectrum, 1996, 33(6), pp: 61-67.
[94] E. M. Clarke and H. Schlingloff. Model checking [J]. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning (Volume II), chapter 24, Elsevier Publishers B.V., 2000, pp: 1635–1790.
[95] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic [J]. In Logic of Programs, volume 131 of Lecture Notes in Computer Science, Springer-Verlag, 1981, page, pp: 52-71.
[96] E. M. Clarke, E. A. Emerson and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications [J]. ACM Transactions on Programming Languages and Systems, 1986, 8(2), pp: 244–263.
[97] E. M. Clarke, O. Grumberg and K. Hamaguchi. Another look at LTL model checking [C]. 6th International Conference on Computer Aided Verification (CAV), 1994, volume 818 of Lecture Notes in Computer Science, pp: 415–427.
[98] E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan and L. A. Ness. Verification of the Future bus cache coherence protocol [C]. In 11th International Symposium on Computer Hardware Description Languages and their Applications, Kluwer Academic Publishers, 1993, pp: 5–20.
[99] E. M. Clarke, O. Grumberg and D. E. Long. Model checking and abstraction [J]. ACM Transactions on Programming Languages and Systems.1994, 16(5), pp:1512–1542.
[100] E. M. Clarke, O. Grumberg, K. L. McMillan and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking [C]. In 32nd ACM/IEEE Conference on Design Automation (DAC), 1995, pp: 427–432.
[101]杨军,葛海通,郑飞君,严晓浪.一种形式化验证方法:模型检验[J].浙江大学学报(理学版), 2006, 33(4), pp: 403-407.
[102] MCMILLAN K L. Symbolic Model Checking: An Approach to the State Explosion Problem [D]. Pittsburgh: Carnegie Mellon University, 1993.
[103] J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL—a tool suite for automatic verification of real-time systems [J]. In Lecture Notes in Computer Science & Hybrid Control Systems, Springer-Verlag, Heidelberg, Germany, 1996, vol. 1066, pp. 232–243.
[104] UPPAAL Project. Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark [EB/OL]. http://www.uppaal.org/.
[105] K. L. McMillan. Getting started with SMV [EB/OL]. Cadence Berkeley Labs, 1998.http://www.cs.indiana.edu/classes/p515/readings/smv/McMillan-tutorial.pdf.
[106] Holzmann GJ. The spin model checker [J]. IEEE Transaction on Software Engineering, 1997, 23(5), pp: 279~295.
[107] Spin Project. Bell Labs [EB/OL]. http://spinroot.com/spin/whatispin.html.
[108] T. A. Henzinger, P. H. Ho, and H. Wong Toi. HyTech: A Model Checker for Hybrid Systems [J]. Software Tools for Technology Transfer, 1997, Vol. 1, pp: 110-122.
[109] HyTech Project. The Donald O. Pederson Center for Electronic Systems Design [EB/OL]. http://embedded.eecs.berkeley.edu/research/hytech/.
[110] Sergio Yovine. Kronos: a verification tool for real-time systems [J]. International Journal on Software Tools for Technology Transfer, 1997, Vol. 1, pp: 15-27.
[111] Murphi Project. Prof. Ganesh Gopalakrishnan's research group [EB/OL]. http://verify.stanford.edu/dill/murphi.html.
[112] Yusuke Matsunaga, An efficient equivalence checker for combinational circuits, Proceedings of the 33rd annual conference on Design automation [C], Las Vegas, Nevada, United States, 1996, pp: 629-634.
[113] Paruthi, V., Kuehlmann, A. Equivalence Checking Combining a Structural SAT-Solver, BDDs, and Simulation [C]. Proceedings of the 2000 IEEE International Conference on Computer Design: VLSI in Computers & Processors, 2000, pp: 459-468.
[114] S. Reda, A. Salem. Combinational equivalence checking using Boolean satisfiability and binary decision diagrams [C]. Proceedings of the conference on Design, automation and test in Europe, Munich, Germany, 2001, pp: 122-126.
[115] E. W. Smith, D. L. Dill. Automatic formal verification of block cipher implementations [C]. Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, Portland, Oregon, 2008, pp: 1-7.
[116] Andreas Kuehlmann, Florian Krohm. Equivalence checking using cuts and heaps [C]. Proceedings of the 34th annual conference on Design automation, Anaheim, California, United States, 1997, pp: 263-268.
[117] Shi-Yu Huang, Kwant-Ting Cheng. Formal Equivaence Checking and Design DeBugging [J]. Kluwer Academic Publishers, Norwell, MA, 1998.
[118]周慧.计算树逻辑特性模式研究.计算机工程, 2009, 35(23), pp: 68-70.
[119] Huth M., Ryan M. Logic in Computer Science: Modeling and Reasoning about Systems [M]. New York, USA: MIT Press, 2004.
[120] Clarke E. M., Grumberg O., Peled D. A. Model Checking [M]. London, UK: Cambridge University Press, 1999.
[121] Havelund K., Mike L. J. Formal analysis of a space-craft controller using SPIN [J]. IEEE Transactions on Software Engineering, 2001, 27(8), pp: 749-765.
[122] Perrig A., Szewczyk R., Tygar J. D. SPINs: security protocols for sensor networks [J].Wireless Network, 2002, 8(5), pp: 521-534.
[123]黎升洪,缪淮扣,张新林.线性时态逻辑中的特性模式[J].计算机应用, 2006, 26(8), pp: 1912-1915.
[124]周从华,刘志锋.具有过去时态算子的计算树逻辑模型检测[J].计算机工程, 2007, 33(22), pp: 98-100.
[125] Ben-Ari M., Manna Z., Pnueli A. The temporal logic of branching time [J]. Acta Informatica, 1983, 20(1), pp: 207-226.
[126] McMilan K. L. Symbolic modeling checking [M]. Kluwer Academic Publishers, 1993.
[127] J. Eker, J. Janneck, Edward A. Lee and Jie Liu etc. Taming heterogeneity - the Ptolemy approach[C]. Proceedings of the IEEE, 2003, 91(1), pp:127-144.
[128] E. A. Lee and H. Zheng. Operational Semantics of Hybrid Systems[C]. Proceedings of Hybrid Systems: Computation and Control (HSCC) LNCS 3414, Zurich, Switzerland, March 9-11, 2005, pp: 25-53.
[129] E. A. Lee, H. Zheng. Leveraging Synchronous Language Principles for Heterogeneous Modeling and Design of Embedded Systems [C]. EMSOFT '07, 2007, Salzburg, Austria.
[130] M.-K. Leung, T. Mandl, E. A. Lee, E. Latronico, C. Shelton, S. Tripakis, and B. Lickly[C]. Scalable Semantic Annotation using Lattice-based Ontologies. ACM/IEEE 12th International Conference on Model Driven Engineering Languages and Systems (MODELS), Denver, CO, USA, 4-9 October, 2009.
[131] Christopher Brooks, Edward A. Lee. Ptolemy II - Heterogeneous Concurrent Modeling and Design in Java[C]. 11 February, 2010; Poster presented at the 2010 Berkeley EECS Annual Research Symposium (BEARS).
[132] Edward A. Lee and Stavros Tripakis. Modal Models in Ptolemy [C]. Proceedings of 3rd International Workshop on Equation-Based Object-Oriented Modeling Languages and Tools (EOOLT 2010), October, 2010.
[133] John C. Eidson, Edward A. Lee, Slobodan Matic, Sanjit A. Seshia and Jia Zou. A Time-Centric Model for Cyber-Physical Applications [C]. Proceedings of 3rd International Workshop on Model Based Architecting and Construction of Embedded System (ACESMB 2010), pp. 21-35, October, 2010.
[134] E. A. Lee. Computing Needs Time [J]. Communications of the ACM, 2009, 52(5).
[135] X. Liu, E. A. Lee. CPO semantics of timed interactive actor networks [J]. Theoretical Computer Science, 2008, 409 (1), pp: 110-25.
[136] E. A. Lee, H. Zheng. Leveraging Synchronous Language Principles for HeterogeneousModeling and Design of Embedded Systems [C]. EMSOFT 2007, September 30-October 3, 2007, Salzburg, Austria.
[137] E. A. Lee. The Problem with Threads [J]. IEEE Computer, 2006, 39(5), pp: 33-42.
[138] Kyungmin Bae, Peter Csaba ?lveczky, Thomas Huining Feng, Stavros Tripakis. Verifying Ptolemy II Discrete-Event Models Using Real-Time Maude [C]. ICFEM '09: Proceedings of the 11th International Conference on Formal Engineering Methods, 717-736, 9-12, December, 2009.
[139] Edward A. Lee, Xiaojun Liu, and Stephen Neuendorffer. Classes and inheritance in actor-oriented design [J]. ACM Transactions on Embedded Computing Systems (TECS), 2009, 8(4).
[140] Edward A. Lee. Heterogeneous Actor Modeling [C]. International Conference on Embedded Software (EMSOFT), Taipei, Taiwan, October, 2011.
[141] Christopher Brooks, Chihhong Cheng, Thomas Huining Feng, Edward A. Lee and Reinhard von Hanxleden. Model Engineering using Multimodeling [C]. 1st International Workshop on Model Co-Evolution and Consistency Management (MCCM '08), September 30, 2008.
[142]李琳,江志斌.基于UPPAAL的虚拟生产系统仿真[J].上海交通大学学报, 2006, 40(7), pp: 1140-1147.
[143]徐刚,吴智铭. FMS建模和形式化验证[J].系统仿真学报, 2004, 16(9), pp: 1914-1917.
[144] Behrmann, G., Larsen K. G., Moller O., David A., Pettersson P., Wang Yi. UPPAAL: present and future [C]. Proceedings of the 40th IEEE Conference on Decision and Control, 2001, Vol. 3, pp: 2881-2886.
[145] Havelund K., Skou A., Larsen K. G., Lund K. Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL [C]. Proceedings of the 18th IEEE Real-time Systems Symposium, 1997, pp: 2-13.
[146] Kim G. Larsen, Paul Pettersson and Wang Yi. UPPAAL in a Nutshell [J]. International Journal of Software Tools for Technology Transfer, 1997, 1(2).
[147] Holsapple C.W., Jacob V.S., Pakath, R., Zaveri, J.S. A genetics-based hybrid scheduler for generating static schedules in flexible manufacturing contexts [J]. IEEE Transactions on Systems, Man and Cybernetics, 1993, Vol. 23, pp: 953 -97.
[148] Cavalieri S., Mirabella O. A PN-based scheduler for a flexible semiconductor manufacturing system [C]. Proceedings of IEEE Conference on Emerging Technologiesand Factory Automation, 1996, Vol. 2, pp: 724 -729.
[149] Burns,A. How to verify a Safe Real-Time System: The Application of Model Checking and Timed Automata to the Production Cell Case Study [J]. Real-Time Systems, 2003, 24(2), pp: 135-151.
[150] R. Alur and D. L. Dill. A theory of timed automata [J]. Theoretical Computer Sciences, 1994, Vol. 126, pp: 183-235.
[151] Chen D. J, Torngren M. A Metrics System for Quantifying Operational Coupling in Embedded Computer Control Systems [C]. In Proceeding of EMSOFT’04, Pisa, Italy, 2004.
[152] Chen D. J, Torngren M. A systematic Approach for identifying Operational Relationships in Embedded Computer Control systems [C]. 30th Euromicro Conf. on component–based software engineering track, 2004.
[153] Cengic, G. and Akesson, K. On formal analysis of IEC 61499 applications, part A: Modeling. IEEE Trans. on Ind. Inf., 2010, 6(2), 136-144.
[154] Cengic, G. and Akesson, K. On formal analysis of IEC 61499 applications, part B: Execution Semantics. IEEE Trans. on Ind. Inf., 2010, 6(2), 145-154.