在CTCS-3(Chinese Train Control System Level 3)级列控系统中,RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节,现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RA...在CTCS-3(Chinese Train Control System Level 3)级列控系统中,RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节,现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RAISE的形式化方法,结合域的模型,在对RBC切换流程分析的基础上,构建状态转移图,得到切换协议的形式化模型,使用等价和推断的推理规则对模型的正确性和实时性进行推理验证,得到的结果表明,RBC切换协议满足规范标准对正确性与实时性的要求,将验证结果与其他文献的结论进行比较分析,说明该方法具有通用性,对于推广其在列控系统场景验证中的应用有一定的实际意义。展开更多
Using the tools of distinct excluded blocks, computational search and symbolic dynamics, the classification problem of all 256 elementary cellular automata is discussed from the point of view of time series generated ...Using the tools of distinct excluded blocks, computational search and symbolic dynamics, the classification problem of all 256 elementary cellular automata is discussed from the point of view of time series generated by them,and examples in each class are provided to explain the methods used.展开更多
Contrary to the “end” and “death” assertions on philosophy, this paper predicts an equilibrium-based and harmony-centered scientific reincarnation of philosophy. Logically, the reincarnation is backed by a formal ...Contrary to the “end” and “death” assertions on philosophy, this paper predicts an equilibrium-based and harmony-centered scientific reincarnation of philosophy. Logically, the reincarnation is backed by a formal system and a background independent geometry that transcends spacetime. Physically, it is supported by definable quantum causality and bipolar logical unifications of matter and antimatter, particle and wave, big bang and black hole, relativity and quantum entanglement. Philosophically, it is distinguished from Western metaphysics and dialectics as well as the Dao of Laozi. It is named a quantum reincarnation for its central claim that YinYang bipolar quantum entanglement is the source of causality for the Being of beings following the 2nd law of thermodynamics. Thus, it presents a modest unification of science and philosophy for their reciprocal interaction (Note: Equilibrium subsumes non-equilibrium and quasi—equilibrium as local non-equilibriums can form global equilibrium or quasi-equilibrium).展开更多
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.展开更多
A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agent...A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.展开更多
Geometrical diagnostic methods were often applied to distinguish the gravitational models. But it is scarce to investigate the differences between the different formalisms of modified gravitational theories (e.g. the ...Geometrical diagnostic methods were often applied to distinguish the gravitational models. But it is scarce to investigate the differences between the different formalisms of modified gravitational theories (e.g. the metric formalism and the Palatini formalism). In this paper, we discriminate the gravitational theory with the different formalisms by using the geometrical diagnostic methods. For a considered modified theory of gravity (e.g. the f(R) theory or GBD theory), we can see that the difference between the two formalisms is remarkable according to the diagnostic results. And relative to the ΛCDM model, there are more deviations in metric formalism than those in Palatini formalism, according to the {r, s} diagnostic. Given that the GBD (generalized Brans-Dicke theory) is a time-variable Newton gravitational constant (VG) theory, the differences between the VG theory and the constant-G theory are studied. It indicates that the variation of Newton’s gravitational constant could induce notable effects on geometrical quantities (e.g. r, s and q) in both metric formalism and Palatini formalism.展开更多
文摘在CTCS-3(Chinese Train Control System Level 3)级列控系统中,RBC(Radio Block Center)切换是影响列车安全高效运行的重要环节,现阶段对RBC切换协议进行验证分析所使用的形式化方法还存在状态爆炸或描述性质单一等问题。基于Timed RAISE的形式化方法,结合域的模型,在对RBC切换流程分析的基础上,构建状态转移图,得到切换协议的形式化模型,使用等价和推断的推理规则对模型的正确性和实时性进行推理验证,得到的结果表明,RBC切换协议满足规范标准对正确性与实时性的要求,将验证结果与其他文献的结论进行比较分析,说明该方法具有通用性,对于推广其在列控系统场景验证中的应用有一定的实际意义。
文摘Using the tools of distinct excluded blocks, computational search and symbolic dynamics, the classification problem of all 256 elementary cellular automata is discussed from the point of view of time series generated by them,and examples in each class are provided to explain the methods used.
文摘Contrary to the “end” and “death” assertions on philosophy, this paper predicts an equilibrium-based and harmony-centered scientific reincarnation of philosophy. Logically, the reincarnation is backed by a formal system and a background independent geometry that transcends spacetime. Physically, it is supported by definable quantum causality and bipolar logical unifications of matter and antimatter, particle and wave, big bang and black hole, relativity and quantum entanglement. Philosophically, it is distinguished from Western metaphysics and dialectics as well as the Dao of Laozi. It is named a quantum reincarnation for its central claim that YinYang bipolar quantum entanglement is the source of causality for the Being of beings following the 2nd law of thermodynamics. Thus, it presents a modest unification of science and philosophy for their reciprocal interaction (Note: Equilibrium subsumes non-equilibrium and quasi—equilibrium as local non-equilibriums can form global equilibrium or quasi-equilibrium).
基金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.
文摘A multi-agent based transport system is modeled by timed automata model extended with clock variables. The correctness properties of safety and liveness of this model are verified by timed automata based UPPAAL. Agents have a degree of control on their own actions, have their own threads of control, and under some circumstances they are also able to take decisions. Therefore they are autonomous. The multi-agent system is modeled as a network of timed automata based agents supported by clock variables. The representation of agent requirements based on mathematics is helpful in precise and unambiguous specifications, thereby ensuring correctness. This formal representation of requirements provides a way for logical reasoning about the artifacts produced. We can be systematic and precise in assessing correctness by rigorously specifying the functional requirements.
文摘Geometrical diagnostic methods were often applied to distinguish the gravitational models. But it is scarce to investigate the differences between the different formalisms of modified gravitational theories (e.g. the metric formalism and the Palatini formalism). In this paper, we discriminate the gravitational theory with the different formalisms by using the geometrical diagnostic methods. For a considered modified theory of gravity (e.g. the f(R) theory or GBD theory), we can see that the difference between the two formalisms is remarkable according to the diagnostic results. And relative to the ΛCDM model, there are more deviations in metric formalism than those in Palatini formalism, according to the {r, s} diagnostic. Given that the GBD (generalized Brans-Dicke theory) is a time-variable Newton gravitational constant (VG) theory, the differences between the VG theory and the constant-G theory are studied. It indicates that the variation of Newton’s gravitational constant could induce notable effects on geometrical quantities (e.g. r, s and q) in both metric formalism and Palatini formalism.
