In order to solve the problem of artificial generation and low efficiency of test sequences for zone controller (ZC), a model-based automatic generation method of test sequence is proposed. Firstly, the timed automata...In order to solve the problem of artificial generation and low efficiency of test sequences for zone controller (ZC), a model-based automatic generation method of test sequence is proposed. Firstly, the timed automata model is established based on function analysis of the zone controller, and the correctness of the model is verified by UPPAAL. Then by parsing the timed automata model files, state information and transition conditions can be extracted to generate test case sets. Finally, according to the serialization conditions of test cases, the test cases are serialized into test sequences by using the improved depth first search algorithm. A case, the ZC controls the train running within its jurisdiction, shows that the method is correct and can effectively improve the efficiency of test sequence generation.展开更多
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.展开更多
In this work, we propose an approach for the verification of the AADL architecture. This approach is based on Model Driven Engineering (MDE) and assisted by a toolchain. Indeed, we define a source meta-model for AADL ...In this work, we propose an approach for the verification of the AADL architecture. This approach is based on Model Driven Engineering (MDE) and assisted by a toolchain. Indeed, we define a source meta-model for AADL and a target meta-model for the timed automata formalism;we define a transformation process in two steps: the first is a Model2 Model transformation which takes an AADL Model and produces the corresponding timed automata model. The second transformation is a Model2 Text transformation which takes a timed automata model and generates a text in ta-format code. This code is accepted by the Uppaal toolbox. A case study has been developed to show the feasibility and validity of the proposed approach.展开更多
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.展开更多
Previous studies suggest that there are three different jam phases in the cellular automata automaton model with a slow-to-start rule under open boundaries.In the present paper,the dynamics of each free-flow-jam phase...Previous studies suggest that there are three different jam phases in the cellular automata automaton model with a slow-to-start rule under open boundaries.In the present paper,the dynamics of each free-flow-jam phase transition is studied.By analysing the microscopic behaviour of the traffic flow,we obtain analytical results on the phase transition dynamics.Our results can describe the detailed time evolution of the system during phase transition,while they provide good approximation for the numerical simulation data.These findings can perfectly explain the microscopic mechanism and details of the boundary-triggered phase transition dynamics.展开更多
This paper mainly deals with the effects of transit stops on vehicle speeds and conversion lane numbers in a mixed traffic lane. Based on thorough research of traffic flow and cellular automata theory, it calibrates t...This paper mainly deals with the effects of transit stops on vehicle speeds and conversion lane numbers in a mixed traffic lane. Based on thorough research of traffic flow and cellular automata theory, it calibrates the cellular length and the running speed. Also, a cellular automata model for mixed traffic flow on a two-lane system under a periodic boundary condition is presented herewith, which also takes into consideration the harbour-shaped transit stop as well. By means of computer simulation, the article also studies the effects of bus parking time on the traffic volume, the transit speed and the fast lane speed at the same time. The results demonstrate that, with the increase of the bus parking time, the traffic volume of the transit stop and the transit speed decrease while the fast lane speed increases. This result could help calculate the transit delay correctly and make arrangements for transit routes reasonably and scientifically.展开更多
文摘In order to solve the problem of artificial generation and low efficiency of test sequences for zone controller (ZC), a model-based automatic generation method of test sequence is proposed. Firstly, the timed automata model is established based on function analysis of the zone controller, and the correctness of the model is verified by UPPAAL. Then by parsing the timed automata model files, state information and transition conditions can be extracted to generate test case sets. Finally, according to the serialization conditions of test cases, the test cases are serialized into test sequences by using the improved depth first search algorithm. A case, the ZC controls the train running within its jurisdiction, shows that the method is correct and can effectively improve the efficiency of test sequence generation.
基金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.
文摘In this work, we propose an approach for the verification of the AADL architecture. This approach is based on Model Driven Engineering (MDE) and assisted by a toolchain. Indeed, we define a source meta-model for AADL and a target meta-model for the timed automata formalism;we define a transformation process in two steps: the first is a Model2 Model transformation which takes an AADL Model and produces the corresponding timed automata model. The second transformation is a Model2 Text transformation which takes a timed automata model and generates a text in ta-format code. This code is accepted by the Uppaal toolbox. A case study has been developed to show the feasibility and validity of the proposed approach.
文摘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.
基金Project supported by the National Natural Science Foundation of China (Grant Nos. 70971094 and 50908155)the Program for Changjiang Scholars and Innovative Research Team in University (PCSIRT)
文摘Previous studies suggest that there are three different jam phases in the cellular automata automaton model with a slow-to-start rule under open boundaries.In the present paper,the dynamics of each free-flow-jam phase transition is studied.By analysing the microscopic behaviour of the traffic flow,we obtain analytical results on the phase transition dynamics.Our results can describe the detailed time evolution of the system during phase transition,while they provide good approximation for the numerical simulation data.These findings can perfectly explain the microscopic mechanism and details of the boundary-triggered phase transition dynamics.
基金This work was supported in part by the-National Natural Science Foundation of China （61403342, 61273286, U1509207, 61325019, 113 02195）, and Hubei Key Laboratory of Intelligent Vision Based Monitoring for Hydroelectric Engineering （2014KLA09）.
基金Project supported by the Science and Technology Support Program of Gansu Province,China (Grant No. 0804GKCA038)
文摘This paper mainly deals with the effects of transit stops on vehicle speeds and conversion lane numbers in a mixed traffic lane. Based on thorough research of traffic flow and cellular automata theory, it calibrates the cellular length and the running speed. Also, a cellular automata model for mixed traffic flow on a two-lane system under a periodic boundary condition is presented herewith, which also takes into consideration the harbour-shaped transit stop as well. By means of computer simulation, the article also studies the effects of bus parking time on the traffic volume, the transit speed and the fast lane speed at the same time. The results demonstrate that, with the increase of the bus parking time, the traffic volume of the transit stop and the transit speed decrease while the fast lane speed increases. This result could help calculate the transit delay correctly and make arrangements for transit routes reasonably and scientifically.
