安全关键实时通信协议研究
|
摘要
在后PC时代,实时计算和通信技术已被广泛应用于航空航天、国防、交通运输、核电能源和医疗卫生等诸多安全关键系统中。随着安全关键系统呈现出分布式和-体化的新特性,通信网络已成为系统中的核心组件,并且对安全关键系统的构建和验证起着决定性的作用。一方面虽然已有大量的现场总线,但其开发过程中并没有融入安全的设计理念,通常都是在实现完成后,再去推导其设计的安全性。作为一种涌现特性(emergent property),安全性不可能在系统部署之后被添加进去,它必须贯穿于系统的整个开发过程中。因此,在安全关键应用中很少看到现场总线的身影。另一方面,尽管在安全关键领域,时间触发模型以及时间触发协议因其可预测性,时域可组合性以及容错能力而被认为广泛接受。但对其灵活性差,平均情况下资源利用率低等问题从未停止过研究,并提出了大量的改进协议,如Byteflight, FlexRay。这些协议虽然在一定程度上提高了协议的灵活性,但不仅削弱了协议的安全性,如容错能力,而且也没有触及时间驱动协议设计复杂,难于彻底进行形式化验证等安全相关问题。
在本文中,以时间触发协议的基础全局时间为出发点,重新审视了协议的设计理念,提出了一个新的安全关键实时协议-NOP (Node Order Protocol)。它以节点顺序的理念构建分布式系统,并以此概念将现有协议划分为节点顺序和非节点顺序两大类。现有的节点顺序协议,如TTP (Time-triggered Protocol),将节点顺序的构建建立在全局时间的基础之上,而NOP协议设计的与现有的节点顺序协议正好背道而驰,它是以节点传输顺序为基础,并能够在其之上实现全局时间。因此,NOP协议消除了通信协议对全局时钟的依赖,建立了不依赖于全局时钟的仲裁过程与传输控制机制,以事件触发模式实现时间触发协议的传输语义。更为重要的是NOP协议在保持时间触发协议的安全性的同时,提高了协议的灵活性和资源利用率。本文在IEC61508框架下,将功能安全的安全管理理念贯穿于NOP协议的设计,实现和验证等开发环节,表现在风险管理与复杂性控制方面。在本文中,详细描述了NOP协议的语义设计,重点介绍了协议在事件触发模型下的差错检测和诊断的机制。不同于时间触发协议(如TTP)NOP协议并没有对节点潜在的故障模式及其应用环境做任何假设,而是完全依赖协议自身的能力进行检错和诊断,这样的设计不仅提高了协议自身的故障覆盖率,而且使得协议具有更好的可组合性。在协议设计的早期就引入了验证过程以保证开发生命周期的每一阶段的质量。在验证过程中,将传统的安全评估方法FMEA (Failure Modes and Effects Analysis)与模型检测形式化方法相结合,形成“动静”结合的验证体系。
协议的性能的改善也是NOP协议设计的一个目标。对于协议性能的评估,从理论分析与原型测试两个方面进行分析。结果表明,协议延迟在网络负载达到峰值时存在确定的上限,且协议在此时表现出最优的性能,体现在确定的协议延迟和较小的延迟抖动。更值得指出的是,协议在网络负载达到峰值时取得最优的吞吐量,在lOMbps的以太网中,网络利用率可到95%。进一步证实了NOP协议,不同于传统的事件触发协议,是面向“最坏情况”而设计的,当节点有足够消息要发送时,能够使得网络达到饱和状态,这是现有的时间触发协议和事件触发协议所不可及的。在文中,分析了并定义了NOP协议在值域和时域上的接口,当节点能够以最坏情况下的时域行为组合时,NOP协议能够如时间触发协议一样实现时域可组合性。同时NOP协议的设计独立于底层的物理网络,其安全性完全由协议自身来实现,这有助于实现协议的可组合性,特别是与COTS (Commercial Off-the-Shelf)网络,如以太网,的可组合性。更为重要的是NOP协议虽然基于事件触发模型,但由于去除了时间相关的不确定因素,并实现协议状态转换的确定性,因此能够保证冗余单元之间的确定性(determinism)。因此,基于NOP协议能够实现主动冗余策略,如三模冗余系统。
NOP协议采用新的设计思路将时间触发协议和事件触发协议的优势相结合,继承了时间触发协议的安全特性,并融合了事件触发协议的灵活性和资源利用的有效性。NOP协议的突出优点使其能够被应用于具有隐式节点顺序需求的安全关键应用中,成为取代灵活性差,带宽利用率低的时间触发协议的潜在选择。
Nowadays, real-time computing and communication technology have been widely deployed in safety-critical systems, such as aerospace, defense, transportation, nu-clear power-stations and health-care. Time-triggered architecture (TTA) as well as time-triggered protocol (TTP) has been widely accepted in safety-critical systems, due to its predictability, temporal composability and replica determinism. However, the research on improvement of flexibility and average resource utilization of TTP is still ongoing, developing several new protocols such as Byteflight and FlexRay, which clearly shows the need for more flexibility as well as improved utilization to reach wider acceptance. Though these protocols improve the flexibility of TTP, they not only jeopardize the safety capabilities of TTP, but also do not address the safety-related issue on complexity of protocol design and formal validation. In addi-tion, TTP can not be independent of TTA deploying on the top of COTS networks, such as Ethernet, because its fault hypothesis depends on the system architecture. Such issue is remained in Byteflight and FlexRay.
In this thesis, a new real-time communication protocol-Node Order Proto-col, is proposed. which is based on node order concept. Further, from the node order perspective, the existing protocols can be classified as two categories:non-node ordered and node ordered. The most important design principle of NOP is the inversion of the correlation between global time and the communication protocol layer. The existing node order protocols are all based on global time to establish the transmission order. While NOP design swaps these two layers, which makes the transmission order the basis of global time. Thus NOP establishes the arbitra-tion and the transmission control mechanism independent of global time, turning time-triggered communication semantics into event-triggered. And what is most important is that NOP can maintain the same safety capability of time-triggered protocols with better flexibility and resource utilization.
In this thesis, the NOP design is described in detail, emphasizing on error detection and diagnosis mechanisms based on event-triggered model. Unlike time-triggered protocols, such as TTP. NOP detects and diagnoses errors by itself without the assumption on failure modes of a faulty node and on system model, which not only enhances its fault coverage but also improves its composability. In the early phase of the protocol design, the safety assessment is integrated to validate the correctness of protocol design and reduce the possibility of design fault. In this procedure, Failure Mode & Effect Analysis (FMEA) is complemental with model checking to form the static and dynamic analysis framework. The core of the pro-cedure is controlling the complexity and reducing it. In the case of performance evaluation, theoretic analysis and prototype testing are done in parallel. The anal-ysis results show that the worst case response time is bounded even at the peak network load when each node has a ready message with maximum size to be trans-mitted in its turn. And more important, in such scenario, protocol latency is with less jitter. Especially, network throughput reaches its maximum, which is about 9.5Mbps in 10Mbps Ethernet. This result further.confirms that NOP, different from the traditional event-triggered protocols, such as CAN, is designed for worst case. At the same time, it outperforms the time-triggered protocol by saturating the net-work if possible. The interface of NOP in the value domain and in the time domain is analyzed and derived from the worst-case latency. When the nodes can be inte-grated based on the worst-case temporal behavior, and then temporal composability can be supported by NOP. Moreover, NOP design is independent of the underlying network, which facilitates the capability of the composability with COTS networks, such as Ethernet. At the same time, NOP can guarantee replica determinism in event-triggered model by eliminating non-deterministic time-related factors. The consistent order of input messages and observed events (e.g. timeout events) guar-antees the consistent protocol status among correct nodes within a given interval. Thus, the active redundant system can be implemented on the top of NOP, such as Triple Redundancy Modular (TMR).
NOP protocol uses a new design principle combining the features of time-triggered protocols and event-triggered protocols, which preserves the safety features with flexibility and effectiveness of resource utilization. The outstanding merits of NOP makes it a potential option to be used in the safety-critical system with node order requirement, which adopts a low flexibility or low network bandwidth time-triggered protocol at present, such as a TMR redundant system.
在本文中,以时间触发协议的基础全局时间为出发点,重新审视了协议的设计理念,提出了一个新的安全关键实时协议-NOP (Node Order Protocol)。它以节点顺序的理念构建分布式系统,并以此概念将现有协议划分为节点顺序和非节点顺序两大类。现有的节点顺序协议,如TTP (Time-triggered Protocol),将节点顺序的构建建立在全局时间的基础之上,而NOP协议设计的与现有的节点顺序协议正好背道而驰,它是以节点传输顺序为基础,并能够在其之上实现全局时间。因此,NOP协议消除了通信协议对全局时钟的依赖,建立了不依赖于全局时钟的仲裁过程与传输控制机制,以事件触发模式实现时间触发协议的传输语义。更为重要的是NOP协议在保持时间触发协议的安全性的同时,提高了协议的灵活性和资源利用率。本文在IEC61508框架下,将功能安全的安全管理理念贯穿于NOP协议的设计,实现和验证等开发环节,表现在风险管理与复杂性控制方面。在本文中,详细描述了NOP协议的语义设计,重点介绍了协议在事件触发模型下的差错检测和诊断的机制。不同于时间触发协议(如TTP)NOP协议并没有对节点潜在的故障模式及其应用环境做任何假设,而是完全依赖协议自身的能力进行检错和诊断,这样的设计不仅提高了协议自身的故障覆盖率,而且使得协议具有更好的可组合性。在协议设计的早期就引入了验证过程以保证开发生命周期的每一阶段的质量。在验证过程中,将传统的安全评估方法FMEA (Failure Modes and Effects Analysis)与模型检测形式化方法相结合,形成“动静”结合的验证体系。
协议的性能的改善也是NOP协议设计的一个目标。对于协议性能的评估,从理论分析与原型测试两个方面进行分析。结果表明,协议延迟在网络负载达到峰值时存在确定的上限,且协议在此时表现出最优的性能,体现在确定的协议延迟和较小的延迟抖动。更值得指出的是,协议在网络负载达到峰值时取得最优的吞吐量,在lOMbps的以太网中,网络利用率可到95%。进一步证实了NOP协议,不同于传统的事件触发协议,是面向“最坏情况”而设计的,当节点有足够消息要发送时,能够使得网络达到饱和状态,这是现有的时间触发协议和事件触发协议所不可及的。在文中,分析了并定义了NOP协议在值域和时域上的接口,当节点能够以最坏情况下的时域行为组合时,NOP协议能够如时间触发协议一样实现时域可组合性。同时NOP协议的设计独立于底层的物理网络,其安全性完全由协议自身来实现,这有助于实现协议的可组合性,特别是与COTS (Commercial Off-the-Shelf)网络,如以太网,的可组合性。更为重要的是NOP协议虽然基于事件触发模型,但由于去除了时间相关的不确定因素,并实现协议状态转换的确定性,因此能够保证冗余单元之间的确定性(determinism)。因此,基于NOP协议能够实现主动冗余策略,如三模冗余系统。
NOP协议采用新的设计思路将时间触发协议和事件触发协议的优势相结合,继承了时间触发协议的安全特性,并融合了事件触发协议的灵活性和资源利用的有效性。NOP协议的突出优点使其能够被应用于具有隐式节点顺序需求的安全关键应用中,成为取代灵活性差,带宽利用率低的时间触发协议的潜在选择。
Nowadays, real-time computing and communication technology have been widely deployed in safety-critical systems, such as aerospace, defense, transportation, nu-clear power-stations and health-care. Time-triggered architecture (TTA) as well as time-triggered protocol (TTP) has been widely accepted in safety-critical systems, due to its predictability, temporal composability and replica determinism. However, the research on improvement of flexibility and average resource utilization of TTP is still ongoing, developing several new protocols such as Byteflight and FlexRay, which clearly shows the need for more flexibility as well as improved utilization to reach wider acceptance. Though these protocols improve the flexibility of TTP, they not only jeopardize the safety capabilities of TTP, but also do not address the safety-related issue on complexity of protocol design and formal validation. In addi-tion, TTP can not be independent of TTA deploying on the top of COTS networks, such as Ethernet, because its fault hypothesis depends on the system architecture. Such issue is remained in Byteflight and FlexRay.
In this thesis, a new real-time communication protocol-Node Order Proto-col, is proposed. which is based on node order concept. Further, from the node order perspective, the existing protocols can be classified as two categories:non-node ordered and node ordered. The most important design principle of NOP is the inversion of the correlation between global time and the communication protocol layer. The existing node order protocols are all based on global time to establish the transmission order. While NOP design swaps these two layers, which makes the transmission order the basis of global time. Thus NOP establishes the arbitra-tion and the transmission control mechanism independent of global time, turning time-triggered communication semantics into event-triggered. And what is most important is that NOP can maintain the same safety capability of time-triggered protocols with better flexibility and resource utilization.
In this thesis, the NOP design is described in detail, emphasizing on error detection and diagnosis mechanisms based on event-triggered model. Unlike time-triggered protocols, such as TTP. NOP detects and diagnoses errors by itself without the assumption on failure modes of a faulty node and on system model, which not only enhances its fault coverage but also improves its composability. In the early phase of the protocol design, the safety assessment is integrated to validate the correctness of protocol design and reduce the possibility of design fault. In this procedure, Failure Mode & Effect Analysis (FMEA) is complemental with model checking to form the static and dynamic analysis framework. The core of the pro-cedure is controlling the complexity and reducing it. In the case of performance evaluation, theoretic analysis and prototype testing are done in parallel. The anal-ysis results show that the worst case response time is bounded even at the peak network load when each node has a ready message with maximum size to be trans-mitted in its turn. And more important, in such scenario, protocol latency is with less jitter. Especially, network throughput reaches its maximum, which is about 9.5Mbps in 10Mbps Ethernet. This result further.confirms that NOP, different from the traditional event-triggered protocols, such as CAN, is designed for worst case. At the same time, it outperforms the time-triggered protocol by saturating the net-work if possible. The interface of NOP in the value domain and in the time domain is analyzed and derived from the worst-case latency. When the nodes can be inte-grated based on the worst-case temporal behavior, and then temporal composability can be supported by NOP. Moreover, NOP design is independent of the underlying network, which facilitates the capability of the composability with COTS networks, such as Ethernet. At the same time, NOP can guarantee replica determinism in event-triggered model by eliminating non-deterministic time-related factors. The consistent order of input messages and observed events (e.g. timeout events) guar-antees the consistent protocol status among correct nodes within a given interval. Thus, the active redundant system can be implemented on the top of NOP, such as Triple Redundancy Modular (TMR).
NOP protocol uses a new design principle combining the features of time-triggered protocols and event-triggered protocols, which preserves the safety features with flexibility and effectiveness of resource utilization. The outstanding merits of NOP makes it a potential option to be used in the safety-critical system with node order requirement, which adopts a low flexibility or low network bandwidth time-triggered protocol at present, such as a TMR redundant system.
引文
[1]Fan Ye, Justifying the Use of COTS Components within Safety Critical Appli-cations. Ph.D thesis of University of York. Sep.2005.
[2]John Rushby. A Comparison of Bus Architectures for Safety-Critical Embedded Systems.
[3]Thomesse, J.P. Fieldbus Technology in Industrial Automation.Proceeding of IEEE.93(6) 1073-1101. June 2005.
[4]Fred Seidel. X-by-Wire.Chemnitz University of Technology, Operating Systems Group February 25,2009.
[5]N. Navet, Y. Song, F. Simonot-Lion, and C.Wilwert. Trends in Automotive Communication Systems. Proceedings of the IEEE,93(6), June 2005.
[6]Thomas Noltey, Hans Hanssony, Lucia Lo Belloz. Automotive Communications-Past, Current and Future.
[7]Joaquim Ferreira, Paulo Pedreiras,LuIAlmcida,JoseAlberto Fonseca. THE FTT-CAN PROTOCOL FOR FLEXIBILITY IN SAFETY-CRITICAL SYS-TEMS. IEEE MICRO.2002。
[8]Echelon Corporation, Palo Alto, CA. Introduction to the LonWorks System, 1999. Available at http://osa.echelon.com/Program/LonWorksIntroPDF.htm.
[9]Bosch(1991) CAN specification 2.0. Robert Bosch GmbH, Postfach 30 02 40, D-70442 Stuttgart
[10]S.Zhang, A.Burns, J.Chen and E.S. Lee. Hard Real-Time Communication with the Timed Token Protocol:Current State and Challenging Problems. Real-Time Systems Journal, Vol 27, No 3, pp 271-295,2004.
[11]N. Malcolm. W. zhao, The timed-token protocol for real-time communications. Computer 27:35-41.1994. doi:10.1109/2.248878.
[12]Eduardo Tovar, Francisco Vasques(1999) Real-Time Fieldbus Communications Using Profibus Networks. IEEE TRANSACTIONS ON INDUSTRIAL ELEC-TRONICS 46:1241-1251. doi:10.1109/41.808018.
[13]ControlNet(1997), ControlNet Specications. Boca Raton. Florida, ControlNet International,1.03 edition.
[14]E. Tovar and F. Vasques, Scheduling real-time communications with p-net, Real-Time Systems Digest No.1998/306, IEEE Colloquium on,1998.
[15]The WorldFIP Protocol Standard and Specifications. http.//www.cs.pitt.edu/ mhanna/Master/ch2.pdf
[16]阳宪慧.现场总线技术及其应用.清华大学出版社.1999.
[17]N. C. Audsley,A. Grigg. TIMING ANALYSIS OF THE ARINC 629 DATABUS FOR REAL-TIME APPLICATIONS. Microprocessors and Microsystems Vol-ume 21, Issue 1, Pages 55-61, July 1997.
[18]Ernesto Wandeler,Lothar Thiele. Optimal TDMA Time Slot and Cycle Length Allocation for Hard Real-Time Systems.
[19]Nuno Pereira, Eduardo Tovar and Bjorn Andersson Exact Analysis of TDMA with Slot Skipping. rtcas, pp.63-72,13th IEEE International Conference on Em-bedded and Real- Time Computing Systems and Applications(RTCSA'07).2007.
[20]J. Lee and S. Park, An error control scheme for Ethernet-based real-time com-munication,in Proc.3rd Int. Workshop Real-Time Computing Systems and Ap-plications (RTCSA),1996, pp.214-219.
[21]K. Tindell, A. Burns, and A. Wellings, Calculating controller area network (can) message response times, Control Engineering Practice, vol.3(8), p.1163-169, 1995.
[22]Robert I. Davis,Alan Burns,Reinder J. Bril, Johan J. Lukkien. Controller Area Network (CAN) schedulability analysis:Refuted, revisited and revised. Real-Time Syst (2007) 35:239-272 DOI 10.1007/s11241-007-9012-7.
[23]Pang LP, Tian YM, Li SL, Han ZF. Communication protocols of hard real systems. Mini-Micro Systems,2000,21(4):393-396 (in Chinese with English ab-stract).
[24]J.-D. Decotignie, Ethernet- based real-time and industrial communications, Pro-ceeds of The IEEE, vol.93 Issue:6. pp.1102-1117. Jun 2005.
[25]Zhao H. Study of real time connections and communications in Fieldbus net-works. Journal of Computer Research and Development,1997.34(5):362-367 (in Chinese with English abstract).
[26]Kweon SK, Shin KG. Achieving real-time communication over Ethernet with adaptive traffic smoothing. In:Proc. of the IEEE Real-Time Technology and Applications Symp. Washington:IEEE Computer Society Press,2000.90-100.
[27]Krommenacker N, Divoux T. Rondeau E. Using genetic algorithms to design switched Ethernet industrial networks. Industrial Electronics,2002,1(1):152-157.
[28]Pedreiras P, Gai P, Almeida L. et.al. FTT-Ethernet:a flexible real-time com-munication.
[29]Safety Critical Real-Time Networks Based on Ethernet Technology YANG Shi-Ping+, SANG Nan, XIONG Guang-Ze,Journal of Software. vol15. No.1.2005. (in Chinese with English abstract)
[30]何凯,基于以太网的硬实时通信协议的设计与实现.大连理工大学硕十论文.2008.Protocol.that supports dynamic QoS management on Ethernet-based sys-tems.IEEE Transactions on Industrial Informaties,2005,1(3):162-172.
[31]叶莘,Ethernet Powerlink—实时的工业以太网.工业以太网与现场总线.2004.
[32]缪学勤.论六种实时以太网的通信协议.自动化仪表,2005,26(4)：1-6.
[33]冯冬芹,申屠久洪,王少勇等.我国第一个拥有自主知识产权的E以标准及其验证应用.可编程控制器与工厂自动化,2004,1(7)：10-1
[34]PROFINET Unplugged-An introduction to PROFINET IO. http://www.rtaautomation.com/profinetio/
[35]Martin Rostan, Joseph E. Stubbs (ETG) and Dmitry Dzilno (Applied Materi-als), EtherCAT-enabled Advanced Control Architecture. ASMC 2010.
[36]H. Kopetz, Real-Time Systems,Design Principles for Distributed Embedded Ap-plications. USA:Kluwer Academic Publishers,1997.
[37]Hermman Koptez. A Comparison of CAN and TTP In Proc. of the IFAC Dis-tributed Computer Systems Workshop
[38]G. Leen, D. Heffernan. TTCAN, a new time-triggered controller area net-work. Microprocessors and Microsystems 26:77-94.2002. doi:10.1016/S0141-9331(01)00148-X
[39]Florian Hartwich, Bernd Miiller, Thomas Fuhrer, Robert Hugel. Timing in the TTCAN Network.8th International CAN Conference.2002.
[40]L. Almeida, P. Pedreiras, J. A. Fonseca. The FTT-CAN Protocol:Why and How. IEEE Tr. Industrial Electronics 49(6),2002.
[41]T. Nolte, M. Nolin, H. Hansson. Real-Time Server-Based Communication for CAN, IEEE Trans. Industrial Informatics 1(3):192-201, IEEE Industrial Elec-tronics Society,2005.
[42]I Broster. Flexibility in Dependable Communication. PhD thesis, University of York, UK,2003.
[43]J. R. Pimentel, J. A. Fonseca. FlexCAN:A Flexible Architecture for Highly Dependable Embedded Applications. RTN 2004.
[44]G. Cena. A. Valenzano Performance analysis of Byteflight networks. Factory Communication Systems,2004. Proceedings.2004 IEEE International Workshop on. doi:10.1109/WFCS.2004.1377701
[45]J. Berwanger, M. Peller, and R. Griessbach. Bytefight-A New High-Performance Data Bus System for Safety-Related Applications. BMW AG, February 2000.
[46]Wang Z, Wang TR, Sun YX. Survey of real time schedule theory and the state-of-the-are of its application in industrial real time communication system (Part 1). Information and Control,2002.31(2):146?163 (in Chinese with English ab-stract).
[47]Gunnter H, Thomas T. Time-Triggered architecture for safety-related dis-tributed real-time systems in transportation systems. Proc.Of the Fault Tolerant Computing Symposium 28. Munich:IEEE Computer Society Press,1998.402 407.
[48]TTA-Group. The Cross-Industry Consortium for Time- Triggered Systems. http://www.ttagroup.org/.
[49]TTTech. Time-Triggered Technology. http://www.tttech.com/.
[50]Ethernet POWERLINK Communication Profile Specification. EPSG DS 301. Std. V1.1.0,2008.
[51]Hermann K, Gunter G. TTP-A protocol for fault-tolerant real-time systems. IEEE Computer,1994,27(1):14-23.
[52]Time-Triggered protocol TTP/C high-level specification document. TTTech Computer Technology AG, Vienna,2002. http://www. tta-group.org/ttp/specification.htm
[53]Holger Pfeifer. Detlef Schwier, and Friedrich W. von Henke. Formal verifica-tion for time-triggered clock synchronization. In Charles B. Weinstock and John Rushby, editors, Dependable Computing for Critical Applications- 7, volume 12 of Dependable Computing and Fault Tolerant Systems, pages 207-226, San Jose, CA, January 1999. IEEE Computer Society.
[54]D. Schwier and F. von Henke. Mechanical verification of clock synchronization algorithms. In Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of Lecture Notes in Computer Science, pages 262杴71, Lyngby, Denmark. September 1998. Springer-Verlag.
[55]Holger Pfeifer. Formal verification of the TTA group membership algorithm. In Tommaso Bolognesi and Diego Latella, editors, Formal Description Techniques and Protocol Specification, Testing and Verification FORTE XIII/PSTV XX 2000, pages 3-18, Pisa, Italy, October 2000. Kluwer Academic Publishers.
[56]Kenneth Hoyme and Kevin Driscoll. SAFEbusTM. In 11th AIAA/IEEE Digital Avionics Systems Conference, pages 68-73, Seattle, WA, October 1992.2,11
[57]Paul S. Miner. Analysis of the SPIDER fault-tolerance protocols. In C. Michael Holloway, editor, LFM 2000:Fifth NASA Langley Formal Methods Workshop, Hampton, VA, June 2000. NASA Langley Research Center. Slides available at http://shemesh.larc.nasa.gov/fm/Lfm2000/Presentations/lfm2000-spider
[58]FlexRay Consortium. FlexRay Communications System-Protocol Specification. Version 2.0, June 2004.
[59]Traian Pop, Paul Pop, Petru Eles, Zebo Peng, Alexandru Andrei(2008) Timing analysis of the FlexRay communication protocol. Real-Time Sytems 39 205-235. doi:10.1007/s11241-007-9040-3.
[60]H. Kopetz, A. Ademaj, P. Grillinger. and K. Steinhainmer, The time-triggered ethernet(tte) design,in 8th IEEE international Symposium on Object-Oriented Real-Time Distributed Computing(ISORC'05),2005, pp.22-33.
[61]L.Lamport, R.Shostak, and M.Pease, The byzantine general problem, ACM Transactions on Programming Languages and Systems,4(3), pp.382-401, Jul 1982.
[62]John Rushby. An Overview of Formal Verification For the Time-Triggered Ar-chitecture. FTRTFT'02, Oldenburg, Germany, September 2002
[63]Natarajan Shankar. Mechanical verification of a generalized protocol for Byzan-tine faulttolerant clock synchronization. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, Volume 571 of Springer-Verlag Lec-ture Notes in Computer Science, pages 217-236, Nijmegen, The Netherlands, January 1992.
[64]Dawid Trawczynski, Januaz Sosnowski, Junusz Zalewski(2007) The Effect of Large Clock Drift on Performance of Event and Time Triggered Network Inter-faces, depcos-relcomex, pp.344-351,2nd International Conference on Depend-ability of Computer Systems (DepCoS-RELCOMEX '07),2007.
[65]Eric Armengaud. Experimental Evaluation of the FlexRay Clock Synchroniza-tion Service.
[66]M. Schwarz(2002) Implementation of A TTP/C Cluster Based On Commercial Gigabit Ethernet Components. Disertation, Vienna University of Technology, Vienna,Austria,
[67]Leslie Lamport. Time,Clock,and the Ordering of Events in a Distributed System. Communication of the ACM. July 1978.
[68]http://www.ntp.org/
[69]IEEE 1588-2002 standard for a clock synchronization protocol for networked measurement and control systems.
[70]GB/T20438.4-2006/IEC61508-4:1998电气/电子/可编程电子安全相关系统的功能安全第4部分：定义和缩略语GB/T20438.4-2006/IEC61508-4:1998. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 4:Definitions and abbrevia-tions.
[71]Tim Kelly and Rob Weaver.The Goal Structuring Notation -A Safety Argument Notation
[72]Tim Kelly, Extending the safety case concept to address dependabil-ity [C]//PROCEEDINGS of the 22nd INTERNATIONAL SYSTEM SAFETY CONFERENCE,2004.
[73]Inge J R.The safety case,its development and use in the united kingdom[C]//25th International System Safety Conference(ISSC 25),2007.
[74]Chanakya H N, AAP de Alwis, Exploring the role and content of the safety case.chemical engineers, Process Safety and Environmental Protection,2004, 82(4):283-290.
[75]Peter Bishop and Robin Bloomfield.A methodology for safety case develop-ment.Sixth Safety-critical Systems Symposium.Birmingham.1998.
[76]J. A. McDermid and D. J. Pumfrey, Software Safety:Why is there no Consensus? in Proceedings of the 19th International System Safety Conference (ISSC 2001), System Safety Society, Huntsville, USA,2001.
[77]R A Weaver, J McDermid, T. P. Kelly. Software Safety Arguments:Towards a Systematic Categorisation of Evidence.in Proceedings of the 20th Interna-tional System Safety Conference (ISSC 2002), System Safety Society, Denver, Colorado, USA,2002.
[78]International Electrotechnical Commission. Functional safety of electri-cal/electronic/programmable electronic safety-related systems. IEC 61508 First edition. Geneva:1998.
[79]Railway applications-Communications, signalling and processing systems-soft-ware for railway control and protection systems. March 2001.
[80]Algirdas Avizienis.Brian Randell, and Carl Landwehr. Basic Concepts and Tax-onomy of Dependable and Secure Computing. IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING, VOL.1, NO.1, JANUARY-MARCH 2004.
[81]Odd Nordland. When is risk acceptable? proceeding of The 19th International System Safety Conference 2001. Huntsville, Alabama.
[82]M. El Koursi et al. Generalised Assessment Method. ESPRIT P 9032 CASCADE Part 2. INRETS Villeneuve (France):1997.
[83]T.P. Kelly, Managing Complex Safety Cases. in Current Issues in Safety-Critical System:Proceedings of the 11th Safety Critical System Symposium (SSS'03), Bristol, UK, pp.99-115, Springer-Verlag,2003.
[84]I J Bate,T P Kelly. Architectural Considerations in the Certification of Modu-lar Systems. in Proceedings of the 21st International Conference on Computer Safety, Reliability and Security (SAFECOMP'02), Springer-Verlag, September 2002.
[85]CENELEC (European Committee for Electrotechnical Standardization). Rail-way applications-The specification and demonstration of Reliability, Availabil-ity, Maintainability and Safety (RAMS). EN 50126. Brussels:1998.
[86]Fan Ye, Tim Kelly. Contract-Based Justification for COTS Component within Safety- Critical Applications.
[87]G. J. Holzmann, Design and Validation of Computer Protocols. USA:Prentice Hall,1990。
[88]Gunther Bauer, Hermann Kopetz, Peter Puschner. Assumption Coverage under Different Failure Modes in the Time-Triggered Architecture. Research report of Real-time system Group,Vienna University of Technology.
[89]EN50159-2:2001. Railway applications-Communication, signalling and process-ing systems-part 2:Safety related communication in open transmission systems
[90]C. Temple,Avoiding the babbling-idiot failure in a time-triggered communica-tion system, in Proceedings of 28rd Annual International Symposium on Fault-Tolerant Computing,1998.
[91]http://www.osadl.org/
[92]C.M.Krishna, Kang G. Shin. Real-time system.清华大学出版社,2001.
[93]Goddard P. L., Validating The Safety Of Real Time Control Systems Using FMEA. Proceedings of the Annual Reliability and Maintainability Symposium, January 1993.
[94]http://sil4linux.dslab.lzu.edu.cn/
[95]Lutz,R.R.,Shaw. H-Y.,1999a, Applying Adaptive Safety Analysis Techniques. Proceedings of the Tenth International Symposium on Software Reliability En-gineering, Boca Raton, FL, Nov 1-4,1999.
[96]Goddard, P.L.,2000, Software FMEA techniques.2000 Proceedings Annual Re-liability and Maintainability Symposium, pp.118-123.
[97]http://en.wikipedia.org/wiki/Linear_temporal_logic
[98]Pries, K.H.,1998, Failure mode & effects analysis in software development. (SAE Technical Paper Series No.982816). Warren-dale, PA:Society of Automotive Engineers
[99]Jonathan Bowen, Victoria Stavridou,"The Industrial Take-up of Formal Meth-ods in Safety-Critical and Other Areas:A perspective"
[100]Guidelines for Failure Mode and Effects Analysis for Automative, Aerospace and General Manufacturing Industries. Dyadem Press, Richmond Hill, Ontario, Canada. March 2004.
[101]Bouti, A., Ait Kadi, D. A state-of-the-art review of FMEA/FMECA. Interna-tional Journal of reliability, quality and safety engineering 1:515-543,1994.
[102]R. W. Butler (2001-08-06). What is Formal Methods?, http://shemesh.larc.nasa.gov/fm/fm-what.html
[103]Edmund M. Clarke, Orna Grumberg and Doron A. Peled. Model Checking.MIT Press,1999.
[104]http://vl.fmnet.info/
[105]http://formalmethods.wikia.com/wiki/Formal_Methods_Wiki
[106]Holzmann G.J. The SPIN Model Checker:Primer and Reference Manual. Addison-Wesley,2004.
[107]Jonathan Bowen, Victoria Stavridou,"Safety-Critical Systems, Formal Methods and Standards"
[108]Haapanen Pentti, Helminen Atte. FAILURE MODE ANDEFFECTS ANALY-SISOF SOFTWARE-BASED AUTOMATION SYSTEMS.STUK-YTO-TR 190 /AUGUST 2002.
[109]http://en.wikipedia.org/wiki/Model_checking.
[110]Phillip A. Laplante. Real-Time Systems Design And Analysis (3th Edi-tion). Wiley.2004.
[111]http://dslab.lzu.edu.cn:8080/members/licj/spin/
[112]K. Tindell, A. Burns, A. Wellings. An Extendible Approach for Analysing Fixed Priority Hard Real-Time Tasks, Real-Time Systems,6(1) (March 1994) 133-151
[113]K. Tindell and J. Clark, Holistic schedulability analysis for distributed hard real-time systems,Microprocessing and Microprogramming, vol.40, pp.117-134, 1994.
[114]Paul Pop, Petru Eles, and Zebo Peng. Schedulability-Driven Communication Synthesis for Time Triggered Embedded Systems.
[115]http://www.linuxfoundation.org/collaborate/workgroups/networking/netem
[116]Stefan Poledna forward by H.Kopetz. Fault-tolerant Real-Time Systems:the problem of replica determinism. Kluwer.1996.
[117]M. Barborak, M. Malek. The Consensus Problem in Fault-Tolerant Computing. ACM Computing Surveys. Vol.25,No.2, pp.171-220,June 1993.
[118]Babaoglu, O.,Drummond, R.,Streets of Byzantium:Network Architectures for Fast Reliable Broadcasts. Software Engineering, IEEE Transactions on.SE-11 Issue:6,546-554.1985. doi:10.1109/TSE.1985.232247.
[119]徐志根,工长林.三模冗余结构微机联锁系统的安全度分析.西南交通大学学报.第34卷第6期.1999.
[2]John Rushby. A Comparison of Bus Architectures for Safety-Critical Embedded Systems.
[3]Thomesse, J.P. Fieldbus Technology in Industrial Automation.Proceeding of IEEE.93(6) 1073-1101. June 2005.
[4]Fred Seidel. X-by-Wire.Chemnitz University of Technology, Operating Systems Group February 25,2009.
[5]N. Navet, Y. Song, F. Simonot-Lion, and C.Wilwert. Trends in Automotive Communication Systems. Proceedings of the IEEE,93(6), June 2005.
[6]Thomas Noltey, Hans Hanssony, Lucia Lo Belloz. Automotive Communications-Past, Current and Future.
[7]Joaquim Ferreira, Paulo Pedreiras,LuIAlmcida,JoseAlberto Fonseca. THE FTT-CAN PROTOCOL FOR FLEXIBILITY IN SAFETY-CRITICAL SYS-TEMS. IEEE MICRO.2002。
[8]Echelon Corporation, Palo Alto, CA. Introduction to the LonWorks System, 1999. Available at http://osa.echelon.com/Program/LonWorksIntroPDF.htm.
[9]Bosch(1991) CAN specification 2.0. Robert Bosch GmbH, Postfach 30 02 40, D-70442 Stuttgart
[10]S.Zhang, A.Burns, J.Chen and E.S. Lee. Hard Real-Time Communication with the Timed Token Protocol:Current State and Challenging Problems. Real-Time Systems Journal, Vol 27, No 3, pp 271-295,2004.
[11]N. Malcolm. W. zhao, The timed-token protocol for real-time communications. Computer 27:35-41.1994. doi:10.1109/2.248878.
[12]Eduardo Tovar, Francisco Vasques(1999) Real-Time Fieldbus Communications Using Profibus Networks. IEEE TRANSACTIONS ON INDUSTRIAL ELEC-TRONICS 46:1241-1251. doi:10.1109/41.808018.
[13]ControlNet(1997), ControlNet Specications. Boca Raton. Florida, ControlNet International,1.03 edition.
[14]E. Tovar and F. Vasques, Scheduling real-time communications with p-net, Real-Time Systems Digest No.1998/306, IEEE Colloquium on,1998.
[15]The WorldFIP Protocol Standard and Specifications. http.//www.cs.pitt.edu/ mhanna/Master/ch2.pdf
[16]阳宪慧.现场总线技术及其应用.清华大学出版社.1999.
[17]N. C. Audsley,A. Grigg. TIMING ANALYSIS OF THE ARINC 629 DATABUS FOR REAL-TIME APPLICATIONS. Microprocessors and Microsystems Vol-ume 21, Issue 1, Pages 55-61, July 1997.
[18]Ernesto Wandeler,Lothar Thiele. Optimal TDMA Time Slot and Cycle Length Allocation for Hard Real-Time Systems.
[19]Nuno Pereira, Eduardo Tovar and Bjorn Andersson Exact Analysis of TDMA with Slot Skipping. rtcas, pp.63-72,13th IEEE International Conference on Em-bedded and Real- Time Computing Systems and Applications(RTCSA'07).2007.
[20]J. Lee and S. Park, An error control scheme for Ethernet-based real-time com-munication,in Proc.3rd Int. Workshop Real-Time Computing Systems and Ap-plications (RTCSA),1996, pp.214-219.
[21]K. Tindell, A. Burns, and A. Wellings, Calculating controller area network (can) message response times, Control Engineering Practice, vol.3(8), p.1163-169, 1995.
[22]Robert I. Davis,Alan Burns,Reinder J. Bril, Johan J. Lukkien. Controller Area Network (CAN) schedulability analysis:Refuted, revisited and revised. Real-Time Syst (2007) 35:239-272 DOI 10.1007/s11241-007-9012-7.
[23]Pang LP, Tian YM, Li SL, Han ZF. Communication protocols of hard real systems. Mini-Micro Systems,2000,21(4):393-396 (in Chinese with English ab-stract).
[24]J.-D. Decotignie, Ethernet- based real-time and industrial communications, Pro-ceeds of The IEEE, vol.93 Issue:6. pp.1102-1117. Jun 2005.
[25]Zhao H. Study of real time connections and communications in Fieldbus net-works. Journal of Computer Research and Development,1997.34(5):362-367 (in Chinese with English abstract).
[26]Kweon SK, Shin KG. Achieving real-time communication over Ethernet with adaptive traffic smoothing. In:Proc. of the IEEE Real-Time Technology and Applications Symp. Washington:IEEE Computer Society Press,2000.90-100.
[27]Krommenacker N, Divoux T. Rondeau E. Using genetic algorithms to design switched Ethernet industrial networks. Industrial Electronics,2002,1(1):152-157.
[28]Pedreiras P, Gai P, Almeida L. et.al. FTT-Ethernet:a flexible real-time com-munication.
[29]Safety Critical Real-Time Networks Based on Ethernet Technology YANG Shi-Ping+, SANG Nan, XIONG Guang-Ze,Journal of Software. vol15. No.1.2005. (in Chinese with English abstract)
[30]何凯,基于以太网的硬实时通信协议的设计与实现.大连理工大学硕十论文.2008.Protocol.that supports dynamic QoS management on Ethernet-based sys-tems.IEEE Transactions on Industrial Informaties,2005,1(3):162-172.
[31]叶莘,Ethernet Powerlink—实时的工业以太网.工业以太网与现场总线.2004.
[32]缪学勤.论六种实时以太网的通信协议.自动化仪表,2005,26(4)：1-6.
[33]冯冬芹,申屠久洪,王少勇等.我国第一个拥有自主知识产权的E以标准及其验证应用.可编程控制器与工厂自动化,2004,1(7)：10-1
[34]PROFINET Unplugged-An introduction to PROFINET IO. http://www.rtaautomation.com/profinetio/
[35]Martin Rostan, Joseph E. Stubbs (ETG) and Dmitry Dzilno (Applied Materi-als), EtherCAT-enabled Advanced Control Architecture. ASMC 2010.
[36]H. Kopetz, Real-Time Systems,Design Principles for Distributed Embedded Ap-plications. USA:Kluwer Academic Publishers,1997.
[37]Hermman Koptez. A Comparison of CAN and TTP In Proc. of the IFAC Dis-tributed Computer Systems Workshop
[38]G. Leen, D. Heffernan. TTCAN, a new time-triggered controller area net-work. Microprocessors and Microsystems 26:77-94.2002. doi:10.1016/S0141-9331(01)00148-X
[39]Florian Hartwich, Bernd Miiller, Thomas Fuhrer, Robert Hugel. Timing in the TTCAN Network.8th International CAN Conference.2002.
[40]L. Almeida, P. Pedreiras, J. A. Fonseca. The FTT-CAN Protocol:Why and How. IEEE Tr. Industrial Electronics 49(6),2002.
[41]T. Nolte, M. Nolin, H. Hansson. Real-Time Server-Based Communication for CAN, IEEE Trans. Industrial Informatics 1(3):192-201, IEEE Industrial Elec-tronics Society,2005.
[42]I Broster. Flexibility in Dependable Communication. PhD thesis, University of York, UK,2003.
[43]J. R. Pimentel, J. A. Fonseca. FlexCAN:A Flexible Architecture for Highly Dependable Embedded Applications. RTN 2004.
[44]G. Cena. A. Valenzano Performance analysis of Byteflight networks. Factory Communication Systems,2004. Proceedings.2004 IEEE International Workshop on. doi:10.1109/WFCS.2004.1377701
[45]J. Berwanger, M. Peller, and R. Griessbach. Bytefight-A New High-Performance Data Bus System for Safety-Related Applications. BMW AG, February 2000.
[46]Wang Z, Wang TR, Sun YX. Survey of real time schedule theory and the state-of-the-are of its application in industrial real time communication system (Part 1). Information and Control,2002.31(2):146?163 (in Chinese with English ab-stract).
[47]Gunnter H, Thomas T. Time-Triggered architecture for safety-related dis-tributed real-time systems in transportation systems. Proc.Of the Fault Tolerant Computing Symposium 28. Munich:IEEE Computer Society Press,1998.402 407.
[48]TTA-Group. The Cross-Industry Consortium for Time- Triggered Systems. http://www.ttagroup.org/.
[49]TTTech. Time-Triggered Technology. http://www.tttech.com/.
[50]Ethernet POWERLINK Communication Profile Specification. EPSG DS 301. Std. V1.1.0,2008.
[51]Hermann K, Gunter G. TTP-A protocol for fault-tolerant real-time systems. IEEE Computer,1994,27(1):14-23.
[52]Time-Triggered protocol TTP/C high-level specification document. TTTech Computer Technology AG, Vienna,2002. http://www. tta-group.org/ttp/specification.htm
[53]Holger Pfeifer. Detlef Schwier, and Friedrich W. von Henke. Formal verifica-tion for time-triggered clock synchronization. In Charles B. Weinstock and John Rushby, editors, Dependable Computing for Critical Applications- 7, volume 12 of Dependable Computing and Fault Tolerant Systems, pages 207-226, San Jose, CA, January 1999. IEEE Computer Society.
[54]D. Schwier and F. von Henke. Mechanical verification of clock synchronization algorithms. In Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1486 of Lecture Notes in Computer Science, pages 262杴71, Lyngby, Denmark. September 1998. Springer-Verlag.
[55]Holger Pfeifer. Formal verification of the TTA group membership algorithm. In Tommaso Bolognesi and Diego Latella, editors, Formal Description Techniques and Protocol Specification, Testing and Verification FORTE XIII/PSTV XX 2000, pages 3-18, Pisa, Italy, October 2000. Kluwer Academic Publishers.
[56]Kenneth Hoyme and Kevin Driscoll. SAFEbusTM. In 11th AIAA/IEEE Digital Avionics Systems Conference, pages 68-73, Seattle, WA, October 1992.2,11
[57]Paul S. Miner. Analysis of the SPIDER fault-tolerance protocols. In C. Michael Holloway, editor, LFM 2000:Fifth NASA Langley Formal Methods Workshop, Hampton, VA, June 2000. NASA Langley Research Center. Slides available at http://shemesh.larc.nasa.gov/fm/Lfm2000/Presentations/lfm2000-spider
[58]FlexRay Consortium. FlexRay Communications System-Protocol Specification. Version 2.0, June 2004.
[59]Traian Pop, Paul Pop, Petru Eles, Zebo Peng, Alexandru Andrei(2008) Timing analysis of the FlexRay communication protocol. Real-Time Sytems 39 205-235. doi:10.1007/s11241-007-9040-3.
[60]H. Kopetz, A. Ademaj, P. Grillinger. and K. Steinhainmer, The time-triggered ethernet(tte) design,in 8th IEEE international Symposium on Object-Oriented Real-Time Distributed Computing(ISORC'05),2005, pp.22-33.
[61]L.Lamport, R.Shostak, and M.Pease, The byzantine general problem, ACM Transactions on Programming Languages and Systems,4(3), pp.382-401, Jul 1982.
[62]John Rushby. An Overview of Formal Verification For the Time-Triggered Ar-chitecture. FTRTFT'02, Oldenburg, Germany, September 2002
[63]Natarajan Shankar. Mechanical verification of a generalized protocol for Byzan-tine faulttolerant clock synchronization. In J. Vytopil, editor, Formal Techniques in Real-Time and Fault-Tolerant Systems, Volume 571 of Springer-Verlag Lec-ture Notes in Computer Science, pages 217-236, Nijmegen, The Netherlands, January 1992.
[64]Dawid Trawczynski, Januaz Sosnowski, Junusz Zalewski(2007) The Effect of Large Clock Drift on Performance of Event and Time Triggered Network Inter-faces, depcos-relcomex, pp.344-351,2nd International Conference on Depend-ability of Computer Systems (DepCoS-RELCOMEX '07),2007.
[65]Eric Armengaud. Experimental Evaluation of the FlexRay Clock Synchroniza-tion Service.
[66]M. Schwarz(2002) Implementation of A TTP/C Cluster Based On Commercial Gigabit Ethernet Components. Disertation, Vienna University of Technology, Vienna,Austria,
[67]Leslie Lamport. Time,Clock,and the Ordering of Events in a Distributed System. Communication of the ACM. July 1978.
[68]http://www.ntp.org/
[69]IEEE 1588-2002 standard for a clock synchronization protocol for networked measurement and control systems.
[70]GB/T20438.4-2006/IEC61508-4:1998电气/电子/可编程电子安全相关系统的功能安全第4部分：定义和缩略语GB/T20438.4-2006/IEC61508-4:1998. Functional safety of electrical/electronic/programmable electronic safety-related systems-Part 4:Definitions and abbrevia-tions.
[71]Tim Kelly and Rob Weaver.The Goal Structuring Notation -A Safety Argument Notation
[72]Tim Kelly, Extending the safety case concept to address dependabil-ity [C]//PROCEEDINGS of the 22nd INTERNATIONAL SYSTEM SAFETY CONFERENCE,2004.
[73]Inge J R.The safety case,its development and use in the united kingdom[C]//25th International System Safety Conference(ISSC 25),2007.
[74]Chanakya H N, AAP de Alwis, Exploring the role and content of the safety case.chemical engineers, Process Safety and Environmental Protection,2004, 82(4):283-290.
[75]Peter Bishop and Robin Bloomfield.A methodology for safety case develop-ment.Sixth Safety-critical Systems Symposium.Birmingham.1998.
[76]J. A. McDermid and D. J. Pumfrey, Software Safety:Why is there no Consensus? in Proceedings of the 19th International System Safety Conference (ISSC 2001), System Safety Society, Huntsville, USA,2001.
[77]R A Weaver, J McDermid, T. P. Kelly. Software Safety Arguments:Towards a Systematic Categorisation of Evidence.in Proceedings of the 20th Interna-tional System Safety Conference (ISSC 2002), System Safety Society, Denver, Colorado, USA,2002.
[78]International Electrotechnical Commission. Functional safety of electri-cal/electronic/programmable electronic safety-related systems. IEC 61508 First edition. Geneva:1998.
[79]Railway applications-Communications, signalling and processing systems-soft-ware for railway control and protection systems. March 2001.
[80]Algirdas Avizienis.Brian Randell, and Carl Landwehr. Basic Concepts and Tax-onomy of Dependable and Secure Computing. IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING, VOL.1, NO.1, JANUARY-MARCH 2004.
[81]Odd Nordland. When is risk acceptable? proceeding of The 19th International System Safety Conference 2001. Huntsville, Alabama.
[82]M. El Koursi et al. Generalised Assessment Method. ESPRIT P 9032 CASCADE Part 2. INRETS Villeneuve (France):1997.
[83]T.P. Kelly, Managing Complex Safety Cases. in Current Issues in Safety-Critical System:Proceedings of the 11th Safety Critical System Symposium (SSS'03), Bristol, UK, pp.99-115, Springer-Verlag,2003.
[84]I J Bate,T P Kelly. Architectural Considerations in the Certification of Modu-lar Systems. in Proceedings of the 21st International Conference on Computer Safety, Reliability and Security (SAFECOMP'02), Springer-Verlag, September 2002.
[85]CENELEC (European Committee for Electrotechnical Standardization). Rail-way applications-The specification and demonstration of Reliability, Availabil-ity, Maintainability and Safety (RAMS). EN 50126. Brussels:1998.
[86]Fan Ye, Tim Kelly. Contract-Based Justification for COTS Component within Safety- Critical Applications.
[87]G. J. Holzmann, Design and Validation of Computer Protocols. USA:Prentice Hall,1990。
[88]Gunther Bauer, Hermann Kopetz, Peter Puschner. Assumption Coverage under Different Failure Modes in the Time-Triggered Architecture. Research report of Real-time system Group,Vienna University of Technology.
[89]EN50159-2:2001. Railway applications-Communication, signalling and process-ing systems-part 2:Safety related communication in open transmission systems
[90]C. Temple,Avoiding the babbling-idiot failure in a time-triggered communica-tion system, in Proceedings of 28rd Annual International Symposium on Fault-Tolerant Computing,1998.
[91]http://www.osadl.org/
[92]C.M.Krishna, Kang G. Shin. Real-time system.清华大学出版社,2001.
[93]Goddard P. L., Validating The Safety Of Real Time Control Systems Using FMEA. Proceedings of the Annual Reliability and Maintainability Symposium, January 1993.
[94]http://sil4linux.dslab.lzu.edu.cn/
[95]Lutz,R.R.,Shaw. H-Y.,1999a, Applying Adaptive Safety Analysis Techniques. Proceedings of the Tenth International Symposium on Software Reliability En-gineering, Boca Raton, FL, Nov 1-4,1999.
[96]Goddard, P.L.,2000, Software FMEA techniques.2000 Proceedings Annual Re-liability and Maintainability Symposium, pp.118-123.
[97]http://en.wikipedia.org/wiki/Linear_temporal_logic
[98]Pries, K.H.,1998, Failure mode & effects analysis in software development. (SAE Technical Paper Series No.982816). Warren-dale, PA:Society of Automotive Engineers
[99]Jonathan Bowen, Victoria Stavridou,"The Industrial Take-up of Formal Meth-ods in Safety-Critical and Other Areas:A perspective"
[100]Guidelines for Failure Mode and Effects Analysis for Automative, Aerospace and General Manufacturing Industries. Dyadem Press, Richmond Hill, Ontario, Canada. March 2004.
[101]Bouti, A., Ait Kadi, D. A state-of-the-art review of FMEA/FMECA. Interna-tional Journal of reliability, quality and safety engineering 1:515-543,1994.
[102]R. W. Butler (2001-08-06). What is Formal Methods?, http://shemesh.larc.nasa.gov/fm/fm-what.html
[103]Edmund M. Clarke, Orna Grumberg and Doron A. Peled. Model Checking.MIT Press,1999.
[104]http://vl.fmnet.info/
[105]http://formalmethods.wikia.com/wiki/Formal_Methods_Wiki
[106]Holzmann G.J. The SPIN Model Checker:Primer and Reference Manual. Addison-Wesley,2004.
[107]Jonathan Bowen, Victoria Stavridou,"Safety-Critical Systems, Formal Methods and Standards"
[108]Haapanen Pentti, Helminen Atte. FAILURE MODE ANDEFFECTS ANALY-SISOF SOFTWARE-BASED AUTOMATION SYSTEMS.STUK-YTO-TR 190 /AUGUST 2002.
[109]http://en.wikipedia.org/wiki/Model_checking.
[110]Phillip A. Laplante. Real-Time Systems Design And Analysis (3th Edi-tion). Wiley.2004.
[111]http://dslab.lzu.edu.cn:8080/members/licj/spin/
[112]K. Tindell, A. Burns, A. Wellings. An Extendible Approach for Analysing Fixed Priority Hard Real-Time Tasks, Real-Time Systems,6(1) (March 1994) 133-151
[113]K. Tindell and J. Clark, Holistic schedulability analysis for distributed hard real-time systems,Microprocessing and Microprogramming, vol.40, pp.117-134, 1994.
[114]Paul Pop, Petru Eles, and Zebo Peng. Schedulability-Driven Communication Synthesis for Time Triggered Embedded Systems.
[115]http://www.linuxfoundation.org/collaborate/workgroups/networking/netem
[116]Stefan Poledna forward by H.Kopetz. Fault-tolerant Real-Time Systems:the problem of replica determinism. Kluwer.1996.
[117]M. Barborak, M. Malek. The Consensus Problem in Fault-Tolerant Computing. ACM Computing Surveys. Vol.25,No.2, pp.171-220,June 1993.
[118]Babaoglu, O.,Drummond, R.,Streets of Byzantium:Network Architectures for Fast Reliable Broadcasts. Software Engineering, IEEE Transactions on.SE-11 Issue:6,546-554.1985. doi:10.1109/TSE.1985.232247.
[119]徐志根,工长林.三模冗余结构微机联锁系统的安全度分析.西南交通大学学报.第34卷第6期.1999.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |