The problem of document rewriting is a fundamental problem in active XML（AXML） data exchange and usually has a higher complexity. Prior work was focused on string automaton theory. This paper tries to solve it by us...The problem of document rewriting is a fundamental problem in active XML（AXML） data exchange and usually has a higher complexity. Prior work was focused on string automaton theory. This paper tries to solve it by using tree automaton. More precisely, the paper firstly defines a new tree automaton, active XML tree automaton （AXTA）, which can efficiently represent the set of AXML documents produced by an AXML document or AXML document schema. And then, an algorithm for constructing AXTA automaton is also proposed. Finally, a polynomial time（PTIME） determining algorithm for AXML document rewriting is presented based on AXTA automaton.展开更多
In an asynchronous cooperative editing workflow of a structured document, each of the co-authors receives in the different phases of the editing process, a copy of the document to insert its contribution. For confiden...In an asynchronous cooperative editing workflow of a structured document, each of the co-authors receives in the different phases of the editing process, a copy of the document to insert its contribution. For confidentiality reasons, this copy may be only a partial replica containing only parts of the (global) document which are of demonstrated interest for the considered co-author. Note that some parts may be a demonstrated interest over a co-author;they will therefore be accessible concurrently. When it’s synchronization time (e.g. at the end of an asynchronous editing phase of the process), we want to merge all contributions of all authors in a single document. Due to the asynchronism of edition and to the potential existence of the document parts offering concurrent access, conflicts may arise and make partial replicas unmergeable in their entirety: they are inconsistent, meaning that they contain conflictual parts. The purpose of this paper is to propose a merging approach said by consensus of such partial replicas using tree automata. Specifically, from the partial replicas updates, we build a tree automaton that accepts exactly the consensus documents. These documents are the maximum prefixes containing no conflict of partial replicas merged.展开更多
Proposed by W3C (World Wide Web Consortium), XQuery is a descriptive query language for XML structured data or documents. The specification of XQuery gives functional description of XQuery’s typing system, but doestn...Proposed by W3C (World Wide Web Consortium), XQuery is a descriptive query language for XML structured data or documents. The specification of XQuery gives functional description of XQuery’s typing system, but doestn’t provide methods to judge the Sub-typing and inDOM relations in language compiling. In this paper, both of the two important relations: Sub-typing and inDOM, are described and analyzed. After some definitions of Tree Automaton, the judgment algorithms of these two relations are proposed. Key words XQuery - typing system - tree automata CLC number TP 301. 6 Biography: XIE Rong-chuan (1946-), male, Associate professor, research direction: database, internet information system.展开更多
A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and ...A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.展开更多
A useful life prediction method based on the integration of the stochastic hybrid automata(SHA) model and the frame of the dynamic fault tree(DFT) is proposed. The SHA model can incorporate the orbit environment, work...A useful life prediction method based on the integration of the stochastic hybrid automata(SHA) model and the frame of the dynamic fault tree(DFT) is proposed. The SHA model can incorporate the orbit environment, work modes, system configuration, dynamic probabilities and degeneration of components,as well as spacecraft dynamics and kinematics. By introducing the frame of DFT, the system is classified into several layers, and the problem of state combination explosion is artfully overcome.An improved dynamic reliability model(DRM) based on the Nelson hypothesis is investigated to improve the defect of cumulative failure probability(CFP), which is used to address the failure probability of components in the SHA model. The simulation using the Monte-Carlo method is finally conducted on two satellites, which are deployed with the same multi-gyro subsystem but run on different orbits. The results show that the predicted useful life of the attitude control system(ACS) with consideration of abrupt failure,degradation, and running environment is quite different between the two satellites.展开更多
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.展开更多
基金Supported by the Natural Science Foundation ofHeilongjiang Province(F00-06)
文摘The problem of document rewriting is a fundamental problem in active XML（AXML） data exchange and usually has a higher complexity. Prior work was focused on string automaton theory. This paper tries to solve it by using tree automaton. More precisely, the paper firstly defines a new tree automaton, active XML tree automaton （AXTA）, which can efficiently represent the set of AXML documents produced by an AXML document or AXML document schema. And then, an algorithm for constructing AXTA automaton is also proposed. Finally, a polynomial time（PTIME） determining algorithm for AXML document rewriting is presented based on AXTA automaton.
文摘In an asynchronous cooperative editing workflow of a structured document, each of the co-authors receives in the different phases of the editing process, a copy of the document to insert its contribution. For confidentiality reasons, this copy may be only a partial replica containing only parts of the (global) document which are of demonstrated interest for the considered co-author. Note that some parts may be a demonstrated interest over a co-author;they will therefore be accessible concurrently. When it’s synchronization time (e.g. at the end of an asynchronous editing phase of the process), we want to merge all contributions of all authors in a single document. Due to the asynchronism of edition and to the potential existence of the document parts offering concurrent access, conflicts may arise and make partial replicas unmergeable in their entirety: they are inconsistent, meaning that they contain conflictual parts. The purpose of this paper is to propose a merging approach said by consensus of such partial replicas using tree automata. Specifically, from the partial replicas updates, we build a tree automaton that accepts exactly the consensus documents. These documents are the maximum prefixes containing no conflict of partial replicas merged.
文摘Proposed by W3C (World Wide Web Consortium), XQuery is a descriptive query language for XML structured data or documents. The specification of XQuery gives functional description of XQuery’s typing system, but doestn’t provide methods to judge the Sub-typing and inDOM relations in language compiling. In this paper, both of the two important relations: Sub-typing and inDOM, are described and analyzed. After some definitions of Tree Automaton, the judgment algorithms of these two relations are proposed. Key words XQuery - typing system - tree automata CLC number TP 301. 6 Biography: XIE Rong-chuan (1946-), male, Associate professor, research direction: database, internet information system.
基金supported by the National Natural Science Foundation of China(11832012)
文摘A state/event fault tree(SEFT)is a modeling technique for describing the causal chains of events leading to failure in software-controlled complex systems.Such systems are ubiquitous in all areas of everyday life,and safety and reliability analyses are increasingly required for these systems.SEFTs combine elements from the traditional fault tree with elements from state-based techniques.In the context of the real-time safety-critical systems,SEFTs do not describe the time properties and important timedependent system behaviors that can lead to system failures.Further,SEFTs lack the precise semantics required for formally modeling time behaviors.In this paper,we present a qualitative analysis method for SEFTs based on transformation from SEFT to timed automata(TA),and use the model checker UPPAAL to verify system requirements’properties.The combination of SEFT and TA is an important step towards an integrated design and verification process for real-time safety-critical systems.Finally,we present a case study of a powerboat autopilot system to confirm our method is viable and valid after achieving the verification goal step by step.
基金supported by the Fundamental Research Funds for the Central Universities(2016083)
文摘A useful life prediction method based on the integration of the stochastic hybrid automata(SHA) model and the frame of the dynamic fault tree(DFT) is proposed. The SHA model can incorporate the orbit environment, work modes, system configuration, dynamic probabilities and degeneration of components,as well as spacecraft dynamics and kinematics. By introducing the frame of DFT, the system is classified into several layers, and the problem of state combination explosion is artfully overcome.An improved dynamic reliability model(DRM) based on the Nelson hypothesis is investigated to improve the defect of cumulative failure probability(CFP), which is used to address the failure probability of components in the SHA model. The simulation using the Monte-Carlo method is finally conducted on two satellites, which are deployed with the same multi-gyro subsystem but run on different orbits. The results show that the predicted useful life of the attitude control system(ACS) with consideration of abrupt failure,degradation, and running environment is quite different between the two satellites.
文摘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.
