This paper discusses a transport protocol and its formal description techniques for local network. The transport layer function, the transport services and a transport protocol design in a local network architecture m...This paper discusses a transport protocol and its formal description techniques for local network. The transport layer function, the transport services and a transport protocol design in a local network architecture model are presented. A transport protocol specification using the finite state automata (FSA) is given. The correctness of the protocol is verified by using the reachability tree technique with respect to the protocol properties of completeness, deadlock and livelock freeness, termination and reachability.展开更多
The distributed denial of service (DDoS) attack is one of the dangers in intrusion modes. It's difficult to defense and can cause serious damage to the system. Based on a careful study of the attack principles and...The distributed denial of service (DDoS) attack is one of the dangers in intrusion modes. It's difficult to defense and can cause serious damage to the system. Based on a careful study of the attack principles and characteristics, an object-oriented formalized description is presented, which contains a three-level framework and offers full specifications of all kinds of DDoS modes and their features and the relations between one another. Its greatest merit lies in that it contributes to analyzing, checking and judging DDoS. Now this formalized description has been used in a special IDS and it works very effectively.(展开更多
Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description met...Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description methods. This paper presents a new hybrid formal method for communication protocol specification. In this method, finite state machine (FSM), communication sequential process (CSP) and abstract data type (ADT) are mixed and the best features of these approaches are offered. In this paper, the main formal description techniques (FDT) for protocol engineering are brieny introduced and a hybrid formal description method based on the FSM, CSP and ADT for communication protocol is described. Finally, this paper presents the formal specification of an example protocol for LAN by using the proposed hybrid formal method. The results of studies show that the hybrid formal description method for communication protocol is an available and effective approach.展开更多
Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approa...Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approach of choreography model verification based on Description Logic.A meta model of service choreography is built to provide a conceptual framework to capture the formal syntax and semantics of service choreography.Based on the framework,a set of rules and constraints are defined in Description Logic for choreography model verification.To automate model verification,the UML-based service choreography model will be transformed,by the given algorithms,into the DL-based ontology,and thus the model properties can be verified by reasoning through the ontology with the help of a popular DL reasoned.A case study is given to demonstrate applicability of the method.Furthermore,the work will be compared with other related research.展开更多
High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent u...High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent us from developing high quality software. To address the problem, this paper proposes integrating graphical specification technique UML with formal specification technique to construct user requirement specification. We also present a prototype tool to perform the automatic translation from UML specification into Object-Z specification.展开更多
文摘This paper discusses a transport protocol and its formal description techniques for local network. The transport layer function, the transport services and a transport protocol design in a local network architecture model are presented. A transport protocol specification using the finite state automata (FSA) is given. The correctness of the protocol is verified by using the reachability tree technique with respect to the protocol properties of completeness, deadlock and livelock freeness, termination and reachability.
文摘The distributed denial of service (DDoS) attack is one of the dangers in intrusion modes. It's difficult to defense and can cause serious damage to the system. Based on a careful study of the attack principles and characteristics, an object-oriented formalized description is presented, which contains a three-level framework and offers full specifications of all kinds of DDoS modes and their features and the relations between one another. Its greatest merit lies in that it contributes to analyzing, checking and judging DDoS. Now this formalized description has been used in a special IDS and it works very effectively.(
文摘Since communication protocol deals with complex issues related to distribution such as communication, concurrency and synchronization, their development needs to be traced by using sophisticated formal description methods. This paper presents a new hybrid formal method for communication protocol specification. In this method, finite state machine (FSM), communication sequential process (CSP) and abstract data type (ADT) are mixed and the best features of these approaches are offered. In this paper, the main formal description techniques (FDT) for protocol engineering are brieny introduced and a hybrid formal description method based on the FSM, CSP and ADT for communication protocol is described. Finally, this paper presents the formal specification of an example protocol for LAN by using the proposed hybrid formal method. The results of studies show that the hybrid formal description method for communication protocol is an available and effective approach.
基金This work is supported by the National Natural Science Fund number 61802428.
文摘Web Services Choreography Description Language lacks a formal system to accurately express the semantics of service behaviors and verify the correctness of a service choreography model.This paper presents a new approach of choreography model verification based on Description Logic.A meta model of service choreography is built to provide a conceptual framework to capture the formal syntax and semantics of service choreography.Based on the framework,a set of rules and constraints are defined in Description Logic for choreography model verification.To automate model verification,the UML-based service choreography model will be transformed,by the given algorithms,into the DL-based ontology,and thus the model properties can be verified by reasoning through the ontology with the help of a popular DL reasoned.A case study is given to demonstrate applicability of the method.Furthermore,the work will be compared with other related research.
基金This work is supported by the National Natural Science Foundation of China （No. 60073020）, the University Natural Science Foundation of Jiangsu Province of China （No. 05KJB520119） and the Natural Science Foundation Project of Chongqing （No. CSTC2006BB2259）.
文摘High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent us from developing high quality software. To address the problem, this paper proposes integrating graphical specification technique UML with formal specification technique to construct user requirement specification. We also present a prototype tool to perform the automatic translation from UML specification into Object-Z specification.
