Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a...Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a fair timed automaton （TA） that recognizes its satisfying models with prototype verification system （PVS） in this paper. Both the tabular construction＇s principles and the PVS implementation details are given for the different type of MITL formula according to the corresponding semantics interpretations. After this transformation procedure, specifications expressed with MITL formula can be verified formally in the timed automata framework developed previously.展开更多
A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and ...A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.展开更多
Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP,...Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP, which is based on the timed automata (TA) theory. By devising RFID locating application into complex events, we model the timing diagram of RFID data streams based on the TA. We optimize the constraint of the event streams and propose a novel method to derive the constraint between objects, as well as the constraint between object and location. Experiments prove the proposed method reduces the cost of RFID complex event processing, and improves the efficiency of the RTLS.展开更多
本文论述了作者对建立全球导航卫星系统(GNSS,Gloal Navigation Satellite System)的系统时间GNSST,守时实验室的时间基准TA(k)和UTC(k)(k为实验室代号)的整体构想和一些思考,并论述了时间尺度算法,驾驭算法,钟差预测算法是如何在其中...本文论述了作者对建立全球导航卫星系统(GNSS,Gloal Navigation Satellite System)的系统时间GNSST,守时实验室的时间基准TA(k)和UTC(k)(k为实验室代号)的整体构想和一些思考,并论述了时间尺度算法,驾驭算法,钟差预测算法是如何在其中发挥作用的.以北斗系统为例,提出了使用两级驾驭算法建立北斗系统时间BDT(Beidou System Time)的方法.以国家授时中心(NTSC,National Time Service Center)为例,详细描述了建立TA(NTSC)和UTC(NTSC)的整体构想,方法,原理和理论依据.分析了TA(NTSC)对UTC(NTSC)的性能影响;以及假如用UTC(NTSC)驾驭产生BDT时,UTC(NTSC)对BDT时间同步精度和频率稳定度性能的影响;最后给出了同时使用UTC(NTSC)和UTC(BSNC)来驾驭产生BDT的设想,从理论上分析了采用该方案对BDT性能提升的影响.展开更多
[目的]了解近15年中美护理教育研究热点并预测未来我国护理教育发展趋势。[方法]以"Web of Science^(TM)核心合集"(WOS)作为美国数据来源,中国知网(CNKI)和万方数据库作为国内数据来源,运用文献计量学方法统计2001年—2015年...[目的]了解近15年中美护理教育研究热点并预测未来我国护理教育发展趋势。[方法]以"Web of Science^(TM)核心合集"(WOS)作为美国数据来源,中国知网(CNKI)和万方数据库作为国内数据来源,运用文献计量学方法统计2001年—2015年中美护理教育相关文献,借助CiteSpace信息可视化分析软件,展现近15年中美护理教育关键词共现知识图谱。[结果]通过对高频关键词分析发现美国护理教育研究热点为有关教学内容、教学模式、症状管理、临床护理教育的研究等。我国近15年护理教育研究热点为护理课程、临床护理教育、在职护士、高级护理人才、护理专家等。[结论]我国护理教育在未来将会以明确的高级护理人才培养目标、灵活多样的教育模式、适应社会发展的课程以及注重能力培养的临床护理教学为主要发展趋势。展开更多
基金Project supported by the National Natural Science Foundation of China （Grant Nos.60373072, 60673115）, the National Basic Research Program of China （Grant No.2002CB312001）, and the National High-Technology Research and Development Program of China （Grant No.2007AA012144）
文摘Based on analysis of the syntax structure and semantics model of the metric interval temporal logic （MITL） formulas, it is shown how to transform a formula written in the real-time temporal logic MITL formula into a fair timed automaton （TA） that recognizes its satisfying models with prototype verification system （PVS） in this paper. Both the tabular construction＇s principles and the PVS implementation details are given for the different type of MITL formula according to the corresponding semantics interpretations. After this transformation procedure, specifications expressed with MITL formula can be verified formally in the timed automata framework developed previously.
基金supported by the National Natural Science Foundation of China(11832012)
文摘A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.
文摘Complex event processing (CEP) can extract meaningful events for real-time locating system (RTLS) applications. To identify complex event accurately in RTLS, we propose a new RFID complex event processing method GEEP, which is based on the timed automata (TA) theory. By devising RFID locating application into complex events, we model the timing diagram of RFID data streams based on the TA. We optimize the constraint of the event streams and propose a novel method to derive the constraint between objects, as well as the constraint between object and location. Experiments prove the proposed method reduces the cost of RFID complex event processing, and improves the efficiency of the RTLS.
文摘本文论述了作者对建立全球导航卫星系统(GNSS,Gloal Navigation Satellite System)的系统时间GNSST,守时实验室的时间基准TA(k)和UTC(k)(k为实验室代号)的整体构想和一些思考,并论述了时间尺度算法,驾驭算法,钟差预测算法是如何在其中发挥作用的.以北斗系统为例,提出了使用两级驾驭算法建立北斗系统时间BDT(Beidou System Time)的方法.以国家授时中心(NTSC,National Time Service Center)为例,详细描述了建立TA(NTSC)和UTC(NTSC)的整体构想,方法,原理和理论依据.分析了TA(NTSC)对UTC(NTSC)的性能影响;以及假如用UTC(NTSC)驾驭产生BDT时,UTC(NTSC)对BDT时间同步精度和频率稳定度性能的影响;最后给出了同时使用UTC(NTSC)和UTC(BSNC)来驾驭产生BDT的设想,从理论上分析了采用该方案对BDT性能提升的影响.
文摘[目的]了解近15年中美护理教育研究热点并预测未来我国护理教育发展趋势。[方法]以"Web of Science^(TM)核心合集"(WOS)作为美国数据来源,中国知网(CNKI)和万方数据库作为国内数据来源,运用文献计量学方法统计2001年—2015年中美护理教育相关文献,借助CiteSpace信息可视化分析软件,展现近15年中美护理教育关键词共现知识图谱。[结果]通过对高频关键词分析发现美国护理教育研究热点为有关教学内容、教学模式、症状管理、临床护理教育的研究等。我国近15年护理教育研究热点为护理课程、临床护理教育、在职护士、高级护理人才、护理专家等。[结论]我国护理教育在未来将会以明确的高级护理人才培养目标、灵活多样的教育模式、适应社会发展的课程以及注重能力培养的临床护理教学为主要发展趋势。
