Wyniki wyszukiwania - BazTech

1

Wpływ automatycznej kalibracji wizyjnego systemu pozycjonowania na dokładność lokalizacji elementu roboczego

Dziak D. M., Jachimczyk B. S.

Poznan University of Technology Academic Journals. Electrical Engineering

|

2013

|

No. 76

109--116

PL

W artykule przedstawiono strukturę i działanie automatycznego wizyjnego systemu pozycjonowania (PVS), który został zainstalowany na maszynie waterjet (WJ). Ponadto przeprowadzono analizę wpływu kalibracji na działanie PVS. Podstawę systemu stanowią dwie kamery internetowe zamontowane na przemysłowej maszynie WJ. W połączeniu z algorytmem identyfikacji, system przeznaczony jest do pozycjonowania WJ z dużą dokładnością. W tym celu opracowano dwustopniową procedurę kalibracyjną wykorzystującą zestaw znaczników kalibracyjnych w kolorze kontrastującym do tła. Analiza uzyskanych wyników, pokazuje że proponowana metoda pomimo wymagających warunków środowiskowych pozwala na niezawodne pozycjonowanie maszyny WJ z wysoką dokładnością.

EN

This paper presents the structure and principle of operation of the Automatic Waterjet Positioning Vision System (PVS), which was implemented on the waterjet (WJ) machine. Moreover, it presents the impact of calibration method on PVS performance. Two webcams mounted on industrial WJ, form a basis of the system, and constitute its characteristics features. By a combination with the identification algorithm, the PVS was designed for high accuracy positioning of WJ machine. For this purpose, the two-step calibration procedure that uses a set of specific calibration markers in color contrasting to the background, has been developed. The analysis of results shows that, proposed method despite demanding environmental conditions, enables reliable high accuracy positioning of WJ machine.

2

Towards Integrated Verification of Timed Transition Models

Lawford M., Pantelic V., Zhang H.

Fundamenta Informaticae

|

2006

|

Vol. 70, nr 1,2

75-110

EN

This paper describes an attempt to combine theorem proving and model-checking to formally verify real-time systems in a discrete time setting. The Timed Automata Modeling Environment (TAME) has been modified to provide a formal model for Time Transition Models (TTMs) in the PVS proof checker. Strong and weak state-event observation equivalences are formalized in PVS for state-event labeled transition systems (SELTS), the underlying semantic model of TTMs. The state-event equivalences form the basis of truth value preserving abstractions for a real-time temporal logic. When appropriate restrictions are placed upon the TTMs, their PVS models can be easily translated into input for the SAL model-checker. A simple real-time control system is specified and verified using these theories. While these preliminary results indicate that the combination of PVS and SAL could provide a useful environment to perform equivalence verification, model-checking and compositional model reduction of real-time systems, the current implementation in the general purpose SAL model-checker lags well behind state of the art real-time model-checkers.

3

Towards automated consistency checking of module interface specifications

Engel M., Kret A., Mincer-Daszkiewicz J.

Fundamenta Informaticae

|

2000

|

Vol. 42, nr 3,4

251-278

EN

The Trace Assertion Method (TAM) pioneered by Parnas is a formalism used to specify software module interfaces. The main purpose of the research described in this paper is to recognize the possibilities of linking the TAM editor with one of the existing theorem proving systems and to enable thereby the automated consistency checking of trace specifications. Possible approaches to embedding TAM in the Prototype Verification System (PVS) specification language are discussed and the chosen shallow definitional embedding is described in detail. Proof obligations for the consistency checking of trace specifications are obtained as type correctness conditions generated automatically by the PVS type checker. Some of these obligations can be proven automatically by PVS, other proofs need human guidance. Possible ways of increasing automation capabilities of the PVS theorem prover are recognized and presented. We share our experience in defining both specialized and general purpose proof strategies. This research may be viewed as a case study in applying the existing general purpose proof system to consistency checking of some application-specific formalism, which might be of interest for the software designer community