-
Chapter and Conference Paper
Influence of Liquid Film Thickness on Dynamic Property of Magnetic-Liquid Double Suspension Bearing
Due to the low viscosity of seawater, it is difficult to form the seawater-lubricated film, and the bearing capacity and stiffness of the seawater-lubricated film is very small. It is easily to cause the “over...
-
Chapter and Conference Paper
Influence of Liquid Film Thickness on Static Property of Magnetic-Liquid Double Suspension Bearing
Due to the low viscosity of seawater, it is difficult to form the seawater-lubricated film, and the bearing capacity and stiffness of the seawater-lubricated film is very small. It is easily to cause the “over...
-
Chapter and Conference Paper
Characteristics Analysis on Open-Type Liquid Hydrostatic Guideway with Unequal Area Oil Pocket
Design of unequal-area oil pocket can decrease required pressure and flow of primary oil-supply oil pocket in open-type self-adaption oil-supply liquid hydrostatic slide. But anti-vertical-loads and anti-overt...
-
Chapter and Conference Paper
Effect of Film Thickness on Load-Carrying Property of Seawater Dynamic-Hydrostatic Hybrid Thrust Bearing
Since the viscosity of sea water is low, it is difficult to form the lubrication film, the overload and the “liner burn” phenomenon of the seawater. Lubricated hydrostatic-dynamic hybrid thrust bearing are hap...
-
Chapter and Conference Paper
Research on Static Performance of Water-Lubricated Hybrid Bearing with Constant Flow Supply
The article focuses on the thrust bearing with freshwater and marine surface tecter of Water-lubricated Hybrid and established a three dimensional mathematical model. Based on one of opposing ladder-cavity sup...
-
Chapter and Conference Paper
Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures
This paper presents an extension to Hoare Logic for pointer program verification. The main observation leading to this logic is that the value of an expression e depends only on the contents stored in a finite se...
-
Chapter and Conference Paper
Optimize Context-Sensitive Andersen-Style Points-To Analysis by Method Summarization and Cycle-Elimination
This paper presents an efficient context-sensitive, field-based Andersen-style points-to analysis algorithm for Java programs. This algorithm first summarizes methods of the program under analysis using direct...
-
Chapter and Conference Paper
A Partial Order Reduction Technique for Parallel Timed Automaton Model Checking
We propose a partial order reduction technique for timed automaton model checking in this paper. We first show that the symbolic successors w.r.t. partial order paths can be computed using DBMs. An algorithm i...
-
Chapter and Conference Paper
Runtime Verification of Java Programs for Scenario-Based Specifications
In this paper, we use UML sequence diagrams as scenario-based specifications, and give the solution to runtime verification of Java programs for the safety consistency and the mandatory consistency. The safety...
-
Chapter and Conference Paper
Scenario-Based Timing Consistency Checking for Time Petri Nets
In this paper, we solve the consistency checking problems of concurrent and real-time system designs modelled by time Petri nets for the scenario-based specifications expressed by message sequence charts (MSCs...
-
Article
Duration-constrained regular expressions
This paper investigates the logic-automata-connection for Duration Calculus. It has been frequently observed that Duration Calculus with linear duration terms comes close to being a logic of linear hybrid auto...
-
Chapter and Conference Paper
Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming
In this paper, we show that for a class of linear hybrid automata called zero loop-closed automata, the satisfaction problem for linear duration properties can be solved efficiently by linear programming. We give...
-
Chapter and Conference Paper
Timing Analysis of UML Activity Diagrams
UML activity diagrams can be used for modeling the dynamic aspects of systems and for constructing executable systems through forward and reverse engineering. They are very suitable for describing the model of...
-
Chapter and Conference Paper
On checking parallel real-time systems for linear duration properties
The major problem of checking a parallel composition of real-time systems for a real-time property is the explosion of untimed states and time regions. To attack this problem, one can use bisimulation equivale...
-
Chapter and Conference Paper
Hybrid regular expressions
In this paper, we consider the problem verifying hybrid systems modelled by linear hybrid automata. We extend the traditional regular expressions with time constraints and use them as a language to describe th...
