Railway transportation system is a critical sector where design methods and techniques are defined by international standards in order to reduce possible risks to an acceptable minimum level. CENELEC 50128 strongly re...Railway transportation system is a critical sector where design methods and techniques are defined by international standards in order to reduce possible risks to an acceptable minimum level. CENELEC 50128 strongly recommends the utilization of finite state machines during system modelling stage and formal proof methods during the verifi- cation and testing stages of control algorithms. Due to the high importance of interlocking table at the design state of a sig- nalization system, the modelling and verification of inter- locking tables are examined in this work. For this purpose, abstract state machines are used as a modelling tool. The developed models have been performed in a generalized structure such that the model control can be done automatically for the interlocking systems. In this study, NuSMV is used at the verification state. Also, the consistency of the developed models has been supervised through fault injection. The developed models and software components are applied on a real railway station operated by Metro Istanbul Co.展开更多
The excited-state intramolecular hydrogen abstraction reactions of butanal have been investigated using the CAS-MP2/6-311＋G^＊//CASSCF/6-31G^＊ methods. Calculated results show that the hydrogen transfer induced fluo...The excited-state intramolecular hydrogen abstraction reactions of butanal have been investigated using the CAS-MP2/6-311＋G^＊//CASSCF/6-31G^＊ methods. Calculated results show that the hydrogen transfer induced fluorescence quenching of the n,π^＊-excited state of covalent butanal with three paths： （1） The first path corresponds to direct S0-react reconstitution, which involves the first S1 decay by partial hydrogen atom transfer. （2） The second stepwise mechanism can be viewed as a full hydrogen atom transfer followed by a partial hydrogen atom back transfer, electron transfer （near S1/S0 or S0-TS） and finally a proton transfer to S0-react. （3） On the triplet surface, the surface crossing to the singlet state would be clearly much efficient at the T1/S0 region due to the large SOC value of 8.3 cm^-1. The S0-react decay route from T1/S0 was studied with an intrinsic reaction coordinate （IRC） calculation at the CASSCF level, resulting in the S0-React minimum.展开更多
Hydrogen abstraction reaction, H+C2H4 --H2+C2H2 was studied by using A initio SCF method. Ge-ometries were fully optimized at SCF level and energies were computed at STO-3G basis set for reactants and transition state...Hydrogen abstraction reaction, H+C2H4 --H2+C2H2 was studied by using A initio SCF method. Ge-ometries were fully optimized at SCF level and energies were computed at STO-3G basis set for reactants and transition state. Vibrational analysis was performed thereupon. Finally, the rate constant calculations were carried out at different temperatures for all range of reaction temperature according to Eyring's sbwlute reaction rate theory. The calculated activation energy is 12. 68 kcal/mol, lower than observed value (H. S kcal/mol) by 1. 82 kcal/mol only. The agreement of the calculated rate constants with the experiments is satisfactory.展开更多
The addition and abstraction reactions of OH radical with benzoate anion are investigated by density functional theory calculations that include solvent effects using UB3LYP, UCAM-B3LYP, UmPW1PW91 and UM06-2X function...The addition and abstraction reactions of OH radical with benzoate anion are investigated by density functional theory calculations that include solvent effects using UB3LYP, UCAM-B3LYP, UmPW1PW91 and UM06-2X functionals with the 6-311++G(2d,2p) basis set. Geometry optimizations of the reactants, products and transition state species are performed for the possible reaction paths. For the addition reactions, those targeting the ipso-, ortho-, meta- and para-carbons are predicted to be exoergic. The H-atom abstraction reactions from ortho, meta and para positions are also predicted to be exoergic. On the basis of the rate constants calculated by means of the transition state theory, the H-atom abstraction reaction from the ortho position is determined to be the favored path followed by the ortho OH addition reaction.展开更多
This paper adopts counterexample guided abstraction refinement scheme to alleviate the state explosion problem of deadlock detection. We extend the classical labeled transition system models by qualifying transitions ...This paper adopts counterexample guided abstraction refinement scheme to alleviate the state explosion problem of deadlock detection. We extend the classical labeled transition system models by qualifying transitions as certain and uncertain to make deadlock-freedom conservative, i.e. if the abstraction of a system is deadlock-free, then the system is deadlock-free. An abstraction refinement approach to deadlock detection is proposed, and the correctness of the approach is proved.展开更多
In order to fully realize semantic interoperability among distributed and heterogeneous applications on the web, a set of effective interoperability mechanisms is presented. This mechanism adopts service interactive i...In order to fully realize semantic interoperability among distributed and heterogeneous applications on the web, a set of effective interoperability mechanisms is presented. This mechanism adopts service interactive interfaces （SII） and service aggregative interfaces （SAI） modeled with abstract state machine （ASM） to abstractly describe the behavior of the invoked web service instances, which makes business processing accurately specify tasks and effectively solves the problems of communication and collaboration between service providers and service requesters. The mechanism also uses appropriate mediators to solve the problems of information and coinmunication incompatibility during the course of service interaction, which is convenient for service interoperability, sharing and integration. The mechanism＇ s working principle and interoperability implementation are illustrated by a use case in detail.展开更多
提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础...提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.展开更多
用户如何方便有效地使用网格是网格界面和使用模式研究的一个关键问题,用户3A使用网格,即Anytime,Any place,and on Any device,体现了用户对网格使用的基本需求.本文给出了用户3A使用模式的形式定义,并利用ASM(Abstract State Machine...用户如何方便有效地使用网格是网格界面和使用模式研究的一个关键问题,用户3A使用网格,即Anytime,Any place,and on Any device,体现了用户对网格使用的基本需求.本文给出了用户3A使用模式的形式定义,并利用ASM(Abstract State Machine)对用户和服务网格(USG)进行了形式化建模,最后证明了用户和服务网格系统在满足用户合法性s、ession连通性和服务连续性的情况下,用户可以3A使用服务网格.展开更多
Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activitie...Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.展开更多
文摘Railway transportation system is a critical sector where design methods and techniques are defined by international standards in order to reduce possible risks to an acceptable minimum level. CENELEC 50128 strongly recommends the utilization of finite state machines during system modelling stage and formal proof methods during the verifi- cation and testing stages of control algorithms. Due to the high importance of interlocking table at the design state of a sig- nalization system, the modelling and verification of inter- locking tables are examined in this work. For this purpose, abstract state machines are used as a modelling tool. The developed models have been performed in a generalized structure such that the model control can be done automatically for the interlocking systems. In this study, NuSMV is used at the verification state. Also, the consistency of the developed models has been supervised through fault injection. The developed models and software components are applied on a real railway station operated by Metro Istanbul Co.
基金supported by ‘Qinglan’ Talent Engineering Funds and Key Subject of Inorganic Chemistry by Tianshui Normal University
文摘The excited-state intramolecular hydrogen abstraction reactions of butanal have been investigated using the CAS-MP2/6-311＋G^＊//CASSCF/6-31G^＊ methods. Calculated results show that the hydrogen transfer induced fluorescence quenching of the n,π^＊-excited state of covalent butanal with three paths： （1） The first path corresponds to direct S0-react reconstitution, which involves the first S1 decay by partial hydrogen atom transfer. （2） The second stepwise mechanism can be viewed as a full hydrogen atom transfer followed by a partial hydrogen atom back transfer, electron transfer （near S1/S0 or S0-TS） and finally a proton transfer to S0-react. （3） On the triplet surface, the surface crossing to the singlet state would be clearly much efficient at the T1/S0 region due to the large SOC value of 8.3 cm^-1. The S0-react decay route from T1/S0 was studied with an intrinsic reaction coordinate （IRC） calculation at the CASSCF level, resulting in the S0-React minimum.
文摘Hydrogen abstraction reaction, H+C2H4 --H2+C2H2 was studied by using A initio SCF method. Ge-ometries were fully optimized at SCF level and energies were computed at STO-3G basis set for reactants and transition state. Vibrational analysis was performed thereupon. Finally, the rate constant calculations were carried out at different temperatures for all range of reaction temperature according to Eyring's sbwlute reaction rate theory. The calculated activation energy is 12. 68 kcal/mol, lower than observed value (H. S kcal/mol) by 1. 82 kcal/mol only. The agreement of the calculated rate constants with the experiments is satisfactory.
文摘The addition and abstraction reactions of OH radical with benzoate anion are investigated by density functional theory calculations that include solvent effects using UB3LYP, UCAM-B3LYP, UmPW1PW91 and UM06-2X functionals with the 6-311++G(2d,2p) basis set. Geometry optimizations of the reactants, products and transition state species are performed for the possible reaction paths. For the addition reactions, those targeting the ipso-, ortho-, meta- and para-carbons are predicted to be exoergic. The H-atom abstraction reactions from ortho, meta and para positions are also predicted to be exoergic. On the basis of the rate constants calculated by means of the transition state theory, the H-atom abstraction reaction from the ortho position is determined to be the favored path followed by the ortho OH addition reaction.
基金supported by the Natural Science Foundation of Shanghai (Grant No.09ZR1412100)the National Natural Science Foundation of China (Grant No.60673115)the Shanghai Leading Academic Discipline Project (Grant No.J50103)
文摘This paper adopts counterexample guided abstraction refinement scheme to alleviate the state explosion problem of deadlock detection. We extend the classical labeled transition system models by qualifying transitions as certain and uncertain to make deadlock-freedom conservative, i.e. if the abstraction of a system is deadlock-free, then the system is deadlock-free. An abstraction refinement approach to deadlock detection is proposed, and the correctness of the approach is proved.
基金The Natural Science Foundation of Hunan Province (No.05JJ30122),the Education Department Foundation of Hunan Prov-ince (No.05C519).
文摘In order to fully realize semantic interoperability among distributed and heterogeneous applications on the web, a set of effective interoperability mechanisms is presented. This mechanism adopts service interactive interfaces （SII） and service aggregative interfaces （SAI） modeled with abstract state machine （ASM） to abstractly describe the behavior of the invoked web service instances, which makes business processing accurately specify tasks and effectively solves the problems of communication and collaboration between service providers and service requesters. The mechanism also uses appropriate mediators to solve the problems of information and coinmunication incompatibility during the course of service interaction, which is convenient for service interoperability, sharing and integration. The mechanism＇ s working principle and interoperability implementation are illustrated by a use case in detail.
文摘提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.
文摘用户如何方便有效地使用网格是网格界面和使用模式研究的一个关键问题,用户3A使用网格,即Anytime,Any place,and on Any device,体现了用户对网格使用的基本需求.本文给出了用户3A使用模式的形式定义,并利用ASM(Abstract State Machine)对用户和服务网格(USG)进行了形式化建模,最后证明了用户和服务网格系统在满足用户合法性s、ession连通性和服务连续性的情况下,用户可以3A使用服务网格.
基金National Natural Science Foundations of China(No. 61073013,No. 90818024)Aviation Science Foundation of China( No.2010ZAO4001)
文摘Timed abstract state machine(TASM) is a formal specification language used to specify and simulate the behavior of real-time systems. Formal verification of TASM model can be fulfilled through model checking activities by translating into UPPAAL. Firstly, the translational semantics from TASM to UPPAAL is presented through atlas transformation language(ATL). Secondly, the implementation of the proposed model transformation tool TASM2UPPAAL is provided. Finally, a case study is given to illustrate the automatic transformation from TASM model to UPPAAL model.
