Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a...Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a formal method with precise syntax and semantics defined. System modeled by PVS specification could be verified by tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time systems. In this approach, we provide 1) a time-extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from a timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexibility and user friendliness in modeling, extendability in formalization and verification content, and better performance. Time constraints are modeled and verified and is a highlight of this paper.展开更多
In order to model the hysteresis behavior of a nano piezoelectric actuator(PA)on nano scale in a real time system,a new hysteresis modeling method based on an improved sub-pixel blocking matching algorithm with an opt...In order to model the hysteresis behavior of a nano piezoelectric actuator(PA)on nano scale in a real time system,a new hysteresis modeling method based on an improved sub-pixel blocking matching algorithm with an optimal block size is proposed in this paper.First,Preisach model is introduced to model the hysteresis behavior of a piezoelectric actuator.Then,a real time block matching algorithm is researched and its block size is optimized with a standard object.Finally,experiments are performed with respect to a nanometer movement platform system,and the results show the feasibility and validity of the sub-pixel estimation based block matching algorithm and its application in modeling the hysteresis behavior of PA.展开更多
文摘Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a formal method with precise syntax and semantics defined. System modeled by PVS specification could be verified by tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time systems. In this approach, we provide 1) a time-extended UML statechart for modeling dynamic behavior of an embedded real-time system; 2) an approach to capture timed automata based semantics from a timed statechart; and 3) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexibility and user friendliness in modeling, extendability in formalization and verification content, and better performance. Time constraints are modeled and verified and is a highlight of this paper.
基金supported by the National Natural Science Foundation of China(Grant No.61305025)
文摘In order to model the hysteresis behavior of a nano piezoelectric actuator(PA)on nano scale in a real time system,a new hysteresis modeling method based on an improved sub-pixel blocking matching algorithm with an optimal block size is proposed in this paper.First,Preisach model is introduced to model the hysteresis behavior of a piezoelectric actuator.Then,a real time block matching algorithm is researched and its block size is optimized with a standard object.Finally,experiments are performed with respect to a nanometer movement platform system,and the results show the feasibility and validity of the sub-pixel estimation based block matching algorithm and its application in modeling the hysteresis behavior of PA.
