In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the sa...In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.展开更多
随着集成电路的发展,电子设备变得越来越复杂,对于通用串行总线(Universal Serial Bus,USB)接口的验证来说,传统的验证方法已经无法满足需求。使用通用验证方法学(Universal Verification Methodology,UVM)验证平台可以提高验证效率,减...随着集成电路的发展,电子设备变得越来越复杂,对于通用串行总线(Universal Serial Bus,USB)接口的验证来说,传统的验证方法已经无法满足需求。使用通用验证方法学(Universal Verification Methodology,UVM)验证平台可以提高验证效率,减少人工操作和误差,保证USB设备的品质和可靠性。本文介绍了一种基于UVM的USB接口验证平台设计,该平台可以对USB接口进行模块化和可重用性设计,支持自动化测试流程,测试数据的收集和分析等功能。通过应用UVM验证平台,针对USB接口传输方式对其单次传输过程进行封装并继承使用,加速USB设备的开发和测试进程,提高产品质量和生产效率。实验结果表明,与传统的验证方法相比,使用UVM验证平台可以显著提高验证效率和精度。此外,该平台还具有高可靠性和高可维护性,可广泛应用于各种USB设备的开发与生产过程中。展开更多
Theoretical foundations of programming systems from modules, objects, components, services are given. Identified relevant theory of programming proposed by the author with the participation of students and postgraduat...Theoretical foundations of programming systems from modules, objects, components, services are given. Identified relevant theory of programming proposed by the author with the participation of students and postgraduates: graph modular programming theory with graph representation as an adjacency matrix for mathematical achievability of graph vertices;theory of generating programming and theory of software factories;theory of graph object and component modeling (OCM) by means of logic and algebra-mathematical theory of determining individual elements of complex systems;theory of system programming based on ontological and service-component models (SOA, SCA) with security and quality systems. The Internet Smart and Nanotechnology are given for perspective transition of computer technology to nanotechnology.展开更多
Interface automata are one of the prominent formalisms for specifying interface behaviors of componentbased systems. However, only one-to-one communication is allowed in the composition of interface automata. This pap...Interface automata are one of the prominent formalisms for specifying interface behaviors of componentbased systems. However, only one-to-one communication is allowed in the composition of interface automata. This paper presents multicast interface automata which generalize the classic interface automata and accommodate multicast communication mechanism. The multicast interface automata endorse both bottom-up and top-down design methodologies. Theoretical results on compatibility and refinement are established for incremental design and independent implementability.展开更多
基金supported by the New Century Excellent Researcher Award Program from Ministry of Education of China (Grant No. NCET-07-0059)the Fundamental Research Funds for the Central Universities (Grant No.2011YJS006)+1 种基金the National High Technology Research and DevelopmentProgram of China ("863" Program) (Grant No. 2011AA010104)the State Key Laboratory of Rail Traffic Control and Safety Research Project(Grant Nos. RCS2008ZZ001, RCS2008ZZ005)
文摘In order to satisfy the safety-critical requirements,the train control system(TCS) often employs a layered safety communication protocol to provide reliable services.However,both description and verification of the safety protocols may be formidable due to the system complexity.In this paper,interface automata(IA) are used to describe the safety service interface behaviors of safety communication protocol.A formal verification method is proposed to describe the safety communication protocols using IA and translate IA model into PROMELA model so that the protocols can be verified by the model checker SPIN.A case study of using this method to describe and verify a safety communication protocol is included.The verification results illustrate that the proposed method is effective to describe the safety protocols and verify deadlocks,livelocks and several mandatory consistency properties.A prototype of safety protocols is also developed based on the presented formally verifying method.
文摘随着集成电路的发展,电子设备变得越来越复杂,对于通用串行总线(Universal Serial Bus,USB)接口的验证来说,传统的验证方法已经无法满足需求。使用通用验证方法学(Universal Verification Methodology,UVM)验证平台可以提高验证效率,减少人工操作和误差,保证USB设备的品质和可靠性。本文介绍了一种基于UVM的USB接口验证平台设计,该平台可以对USB接口进行模块化和可重用性设计,支持自动化测试流程,测试数据的收集和分析等功能。通过应用UVM验证平台,针对USB接口传输方式对其单次传输过程进行封装并继承使用,加速USB设备的开发和测试进程,提高产品质量和生产效率。实验结果表明,与传统的验证方法相比,使用UVM验证平台可以显著提高验证效率和精度。此外,该平台还具有高可靠性和高可维护性,可广泛应用于各种USB设备的开发与生产过程中。
文摘Theoretical foundations of programming systems from modules, objects, components, services are given. Identified relevant theory of programming proposed by the author with the participation of students and postgraduates: graph modular programming theory with graph representation as an adjacency matrix for mathematical achievability of graph vertices;theory of generating programming and theory of software factories;theory of graph object and component modeling (OCM) by means of logic and algebra-mathematical theory of determining individual elements of complex systems;theory of system programming based on ontological and service-component models (SOA, SCA) with security and quality systems. The Internet Smart and Nanotechnology are given for perspective transition of computer technology to nanotechnology.
基金This work was supported by the Chinese National 973 Plan （2010CB328003）, the National Natural Science Foundation of China （Grant Nos. 61272001, 60903030, 91218302）, the Chinese National Key Technology R＆D Program （SQ2012BAJY4052）, the Importation and Development of High-Caliber Talents Project of Beijing Municipal Institutions （YETP0167）, and the Tsinghua University Initiative Scientific Research Program.
文摘Interface automata are one of the prominent formalisms for specifying interface behaviors of componentbased systems. However, only one-to-one communication is allowed in the composition of interface automata. This paper presents multicast interface automata which generalize the classic interface automata and accommodate multicast communication mechanism. The multicast interface automata endorse both bottom-up and top-down design methodologies. Theoretical results on compatibility and refinement are established for incremental design and independent implementability.
