检索结果-南通市图书馆

Timed-pNets： a communication behavioural semantic model for distributed systems

在线全文

学校读者我要写书评

暂无评论

Frontiers of Computer Science 2015年第1期9卷 87-110页

作者： Yanwen CHEN Yixiang CHEN Eric MADELAINE MoE Engineering Research Center for Software/Hardware Co-design Technology and Application Shanghai Key Laboratory of Trustworthy Computing East China Normal University Shanghai 200062 China INRIA Sophia Antipolis Mediterannee Sophia Antipolis 06902 France University of Nice Sophia Antipolis CNRS Sophia Antipolis 06900 France

This paper presents an approach to build a communication behavioural semantic model for heterogeneous distributed systems that include synchronous and asynchronous communications. Since each node of such system has its own physical clock, it brings the challenges of correctly specifying the system time constraints. Based on the logical clocks proposed by Lamport, and CCSL proposed by Aoste team in INRIA, as well as pNets from Oasis team in INRIA, we develop timed-pNets to model communication behaviours for distributed systems. Timed-pNets are tree style hierarchical structures. Each node is associated with a timed specification which consists of a set of logical clocks and some relations on clocks. The leaves are represented by timed-pLTSs. Non-leaf nodes （called timed-pNets nodes） are synchronisation devices that synchronize the behaviours of subnets （these subnets can be leaves or non-leaf nodes）. Both timed-pLTSs and timed-pNets nodes can be translated to timed specifications. All these notions and methods are illustrated on a simple use-case of car insertion from the area of intelligent transportation systems （ITS）. In the end the TimeSquare tool is used to simulate and check the validity of our model.

关键词： ITS logical time formal method timed specification synchronous and asynchronous communication

Remove Irrelevant Atomic Formulas for Timed Automaton Model Checking

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2006年第1期21卷 41-51页

作者：赵建华李宣东郑滔郑国梁 State Key Laboratory of Novel Software Technology Nanjing University Nanjing 210093 P.R. China Department of Computer Science and Technology Nanjing University Nanjing 210093 P.R. China

Most of the timed automata reachability analysis algorithms in the literature explore the state spaces by enumeration of symbolic states, which use time constraints to represent a set of concrete states. A time constraint is a conjunction of atomic formulas which bound the differences of clock values. In this paper, it is shown that some atomic formulas of symbolic states generated by the algorithms can be removed to improve the model checking time- and spaceefficiency. Such atomic formulas are called as irrelevant atomic formulas. A method is also presented to detect irrelevant formulas based on the test-reset information about clock variables. An optimized model-checking algorithm is designed based on these techniques. The case studies show that the techniques presented in this paper significantly improve the space- and time-efficlency of reachability analysis.

关键词： formal method model checking timed automaton

LTL Formulae to Bchi Automata Translation Using on-the-Fly De-generalization

维普期刊数据库评论

在线全文

维普期刊数据库

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2015年第4期24卷 674-678页

作者： SHAN Laixiang QIN Zheng Department of Computer Science and Technology Tsinghua University School of Software Tsinghua University

In this paper, we present a conversion algorithm to translate a Linear temporal logic(LTL) formula to a Bu¨chi automaton(BA) directly. Acceptance degree(AD) is presented to record acceptance conditions satisfied in each state and transition of the BA. According to AD, on-the-fly de-generalization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is performed in the case of the given LTL formula containing U-subformulae or F-subformulae, that is,it is performed as required during the expansion of the given LTL formula. We compare the conversion algorithm presented in this paper to previous works, and show that it is more efficient for a series of LTL formulae in common use.

关键词： formal method Model checking Linear temporal logic On-the-fly de-generalization

Net-structure-based conditions to decide compatibility and weak compatibility for a class of inter-organizational workflow nets

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Science China(Information Sciences) 2015年第7期58卷 128-143页

作者： LIU GuanJun JIANG ChangJun Department of Computer Science Tongji University Key Laboratory of the Ministry of Education for Embedded System and Service Computing Tongji University

Inter-organizational workflow nets(IWF-nets) can well model the interactions among multiple processes by sending/receiving messages. Compatibility and weak compatibility are crucial properties for *** latter guarantees that a system is deadlock-free and livelock-free while the former also guarantees that it has no dead tasks. Our previous work proved that the(weak) compatibility problem is PSPACE-complete for safe IWF-nets. This paper defines a class of IWF-nets in which some simple circuits are allowed. Necessary and sufficient conditions are presented to decide compatibility and weak compatibility for this class, and they are dependent on the net structures only. Algorithms are developed based on these conditions. In addition, we show that the traditional net structures like siphon cannot be easily used to decide the(weak) compatibility of IWF-nets.

关键词： formal method workflow nets compatibility business process model web services composition

A Semantics-Based Approachfor Achieving Self Fault-Tolerance of Protocols

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2000年第2期15卷 176-183页

作者：李腊元李春林 Department of Computer Science & Technology Wuhan Transportation University Wuhan P.R. China

The cooperation of different processes may be lost by mistake when a protocol is executed. The protocol cannot be normally operated under this condition. In this paper,the self fault-tolerance of protocols is discussed, and a semanticsbased approach for achieving self fault-tolerance of protocols is presented. Some main characteristics of self fault-tolerance of protocols concerning liveness, nontermination and infinity are also presented. Meanwhile, the sufficient and necessary conditions for achieving self fault-tolerance of protocols are given. Finally, a typical protocol that does not satisfy the self fault-tolerance is investigated, and a new redesign version of this existing protocol using the proposed approach is given.

关键词： protocols self fault-tolerance formal method multimedia communications protocol engineering S-T protocol semantics

formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving

在线全文

学校读者我要写书评

暂无评论

Journal of Computer Science & Technology 2010年第6期25卷 1305-1320页

作者： Osman Hasan Sofiène Tahar Department of Electrical and Computer Engineering Concordia University

Probabilistic techniques are widely used in the analysis of algorithms to estimate the computational complexity of algorithms or a computational ***,such analyses are performed using paper-and-pencil proofs and the results are sometimes validated using simulation *** techniques are informal and thus may result in an inaccurate *** this paper,we propose a formal technique for analyzing the expected time complexity of algorithms using higher-order-logic theorem *** approach calls for mathematically modeling the algorithm along with its inputs,using indicator random variables,in higher-order *** model is then used to formally reason about the expected time complexity of the underlying algorithm in a theorem *** paper includes the higher-order-logic formalization of indicator random variables,which are fundamental to the proposed *** order to illustrate the practical effiectiveness and utilization of the proposed infrastructure,the paper also includes the analysis of algorithms for three well-known problems,i.e.,the hat-check problem,the birthday paradox and the hiring problem.

关键词： formal method higher-order logic probability theory theorem proving birthday paradox hat-check problem hiring problem

Proving Mutual Authentication Property of RCIA Protocol in RFID Based on Logic of Events

在线全文

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2022年第1期31卷 79-88页

作者： ZHONG Xiaomei XIAO Meihua ZHANG Tong YANG Ke LUO Yunxian School of Software East China Jiaotong University

The increasing commercialization and massive deployment of radio frequency identification(RFID) systems has raised many security related issues which in return evokes the need of security protocols. Logic of events theory(Lo ET) is a formal method for constructing and reasoning about distributed systems and protocols that involve concepts of security. We propose fresh ciphertext and ciphertext release lemmas to extend Lo ET for analyzing and proving the security of authentication protocols that use symmetric key cryptography more than just digital signature. Based on the extended Lo ET we formally analyze and prove the authentication property of RCIA protocol, which provides mutual authentication between Tag and Reader in RFID *** proof approach based on extended Lo ET could be applied to the design and analysis of such ultralightweight RFID mutual authentication protocols.

关键词： logic of events theory mutual authentication property private key cryptography fresh ciphertext telecommunication security distributed systems ultralightweight RFID mutual authentication protocols radio frequency identification systems LoET radiofrequency identification formal method massive deployment symmetric key cryptography cryptographic protocols RCIA protocol security protocols

Dynamic Scheduling Policy for Patient Flow in a Smart Environment

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

Chinese Journal of Electronics 2017年第3期26卷 530-536页

作者： CHEN Xiao DING Jie Nigel Thomas School of Computer Science and Communication Engineering Jiangsu University State Key Laboratory of Software Development Environment Beihang University School of Information Engineering Yangzhou University School of Computing Science Newcastle University

Given the popularity of smart environment in a hospital involving the participation of a large group of patients,scheduling of patients towards their desired destination is still being a challenging *** the development of Internet of Things(Io T),smart environments are increasingly being deployed in various public scenarios and in particular,hospitals are an important target environment for smart *** paper models a dynamic scheduling policy based on a patient flow scenario in order to solve the queuing issue and facilitate people’s *** dynamic scheduling policy aims to forward incoming patients to dissolve jams especially at the peaks by giving accurate predication of appointment *** main modelling technique is a formal method—Performance evaluation process algebra(PEPA).The findings show that the dynamic scheduling policy is able to efficiently improve the patient flow.

关键词： Dynamic scheduling Patient flow Smart environment formal method Performance evaluation process algebra(PEPA)

A Privilege Separation method for Security Commercial Transactions

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

China Communications 2010年第6期7卷 94-99页

作者： Chen Yasha Hu Jun Sun Yu Gai Xinmao Department of Electrical and Information Engineering Naval University of Engineering Wuhan 430033 P. R China School of Computer Beijing University of Technology Beijing 100124 P. R. China School of Computer National University of Defense Technology Changsha 410073 P. R. China

Privilege user is needed to manage the commercial transactions, but a super-administrator may have monopolize power and cause serious security problem. Relied on trusted computing technology, a privilege separation method is proposed to satisfy the security management requirement for information systems. It authorizes the system privilege to three different managers, and none of it can be interfered by others. Process algebra Communication Sequential Processes is used to model the three powers mechanism, and safety effect is analyzed and compared.

关键词： privilege separation fraud management security commercial transactions formal method