Leslie Lamport提出的一种新逻辑:行为时序逻辑TLA(Temporal Logic of Actions),它能在一种语言中同时表达模型程序与逻辑规则。AVISPA是基于行为时序逻辑的用HLPSL语言编程的协议安全检测工具。文中提出对Kerberos协议角色化,然后用AVI...Leslie Lamport提出的一种新逻辑:行为时序逻辑TLA(Temporal Logic of Actions),它能在一种语言中同时表达模型程序与逻辑规则。AVISPA是基于行为时序逻辑的用HLPSL语言编程的协议安全检测工具。文中提出对Kerberos协议角色化,然后用AVISPA工具对HLPSL编码进行检测,结果表明用基于TLA的检测工具是宜于使用且有效的。展开更多
The paper proposes an approach to solving some verification prob- lems of time Petri nets using linear programming. The approach is based on the observation that for loop-closed time Petri nets, it is only necessary t...The paper proposes an approach to solving some verification prob- lems of time Petri nets using linear programming. The approach is based on the observation that for loop-closed time Petri nets, it is only necessary to investigate a finite prefix of an untimed run of the underlying Petri net. Using the technique the paper gives solutions to reachability and bounded delay timing analysis problems. For both problems algorithms are given, that are decision procedures for loop-closed time Petri nets, and semi-decision procedures for general time Petri nets.展开更多
In this paper, we propose a Multi-granularity Spatial Access Control （MSAC） model, in which multi- granularity spatial objects introduce more types of policy rule conflicts than single-granularity objects do. To ana...In this paper, we propose a Multi-granularity Spatial Access Control （MSAC） model, in which multi- granularity spatial objects introduce more types of policy rule conflicts than single-granularity objects do. To analyze and detect these conflicts, we first analyze the conflict types with respect to the relationship among the policy rules, and then formalize the conflicts by template matrices. We designed a model-checking algorithm to detect potential conflicts by establishing formalized matrices of the policy set. Lastly, we conducted experiments to verify the performance of the algorithm using various spatial data sets and rule sets. The results show that the algorithm can detect all the formalized conflicts. Moreover, the algorithm＇s efficiency is more influenced by the spatial object granularity than the size of the rule set.展开更多
In this article a new approach for checking the adequacy of GARCH-type models in time series was proposed. The resulted tests involve weight functions, which provide them with the flexibility in choosing scores to enh...In this article a new approach for checking the adequacy of GARCH-type models in time series was proposed. The resulted tests involve weight functions, which provide them with the flexibility in choosing scores to enhance power performance. The choice of weight functions and the power properties of the tests are studied. For a large number of alternatives, asymptotically distribution-free maximin test is constructed. The tests are asymptotically chi-squared under the null hypothesis and easy to implement. Simulation results indicate that the tests perform well.展开更多
文摘Leslie Lamport提出的一种新逻辑:行为时序逻辑TLA(Temporal Logic of Actions),它能在一种语言中同时表达模型程序与逻辑规则。AVISPA是基于行为时序逻辑的用HLPSL语言编程的协议安全检测工具。文中提出对Kerberos协议角色化,然后用AVISPA工具对HLPSL编码进行检测,结果表明用基于TLA的检测工具是宜于使用且有效的。
基金Keywords:real-time system, time Petri net, linear programming, model-checkingThis work is supported by the National Natural Sc
文摘The paper proposes an approach to solving some verification prob- lems of time Petri nets using linear programming. The approach is based on the observation that for loop-closed time Petri nets, it is only necessary to investigate a finite prefix of an untimed run of the underlying Petri net. Using the technique the paper gives solutions to reachability and bounded delay timing analysis problems. For both problems algorithms are given, that are decision procedures for loop-closed time Petri nets, and semi-decision procedures for general time Petri nets.
基金supported by the National Natural Science Foundation of China(Nos.51204185 and 41674030)Natural Youth Science Foundation of Jiangsu Province,China(No.BK20140185)+1 种基金China Postdoctoral Science Foundation(No.2016M601909)the Fundamental Research Funds for the Central Universities(No.2014QNA44)
文摘In this paper, we propose a Multi-granularity Spatial Access Control （MSAC） model, in which multi- granularity spatial objects introduce more types of policy rule conflicts than single-granularity objects do. To analyze and detect these conflicts, we first analyze the conflict types with respect to the relationship among the policy rules, and then formalize the conflicts by template matrices. We designed a model-checking algorithm to detect potential conflicts by establishing formalized matrices of the policy set. Lastly, we conducted experiments to verify the performance of the algorithm using various spatial data sets and rule sets. The results show that the algorithm can detect all the formalized conflicts. Moreover, the algorithm＇s efficiency is more influenced by the spatial object granularity than the size of the rule set.
基金supported by a grant from the Research Grants Council of Hong Kong.Jianhong Wu was also supported by a grant from Humanities & Social Sciences in Chinese University (07JJD790154)the Youth Talent Foundation of Zhejiang GongShang University (Q09-12)
文摘In this article a new approach for checking the adequacy of GARCH-type models in time series was proposed. The resulted tests involve weight functions, which provide them with the flexibility in choosing scores to enhance power performance. The choice of weight functions and the power properties of the tests are studied. For a large number of alternatives, asymptotically distribution-free maximin test is constructed. The tests are asymptotically chi-squared under the null hypothesis and easy to implement. Simulation results indicate that the tests perform well.
