Informacja

Drogi użytkowniku, aplikacja do prawidłowego działania wymaga obsługi JavaScript. Proszę włącz obsługę JavaScript w Twojej przeglądarce.

English (EN)·Polski (PL)·Yкраїнський (UK)
Przejdź do strony domowej biblioteki Centralna Biblioteka Wojskowa Link otwiera się w nowym oknie Logo biblioteki Prolib Integro - strona głównaCentralna Biblioteka Wojskowa

Wyszukujesz frazę "weryfikacja" wg kryterium: Temat

  Lista filtrów
Wyrównaj
    Wyświetlanie 1-6 z 6
    Tytuł:
    Petri nets and activity diagrams in logic controller specification – transformation and verification
    Sieci petriego i diagramy aktywności w specyfikacji sterowników logicznych – transformacja i weryfikacja
    Autorzy:
    Grobelna, I.
    Grobelny, M.
    Adamski, M.
    Powiązania:
    https://bibliotekanauki.pl/articles/389795.pdf
    Data publikacji:
    2010
    Wydawca:
    Politechnika Bydgoska im. Jana i Jędrzeja Śniadeckich. Wydawnictwo PB
    Tematy:
    formal verification
    logic controller
    model checking
    Petri nets
    UML Activity
    Diagrams
    formalna weryfikacja
    sterownik logiczny
    weryfikacja modelowa
    sieci Petriego
    diagramy aktywności UML
    Opis:
    The paper presents formal verification method of logic controller specification taking into account user-specified properties. Logic controller specification may be expressed as Petri net or UML 2.0 Activity Diagram. Activity Diagrams seem to be more user-friendly and easy-understanding that Petri nets. Specification in form of activity diagram may afterwards be transformed into Petri net, which may then be formally verified and used to automatically generate implementation (code). A new transformation method dedicated for event-driven systems is proposed. Verification process is executed automatically by the NuSMV model checker tool. Model description based on specification and properties list is being built. Model description derived from Petri net is presented in RTL-level and easy to synthesize as reconfigurable logic controller or PLC. Properties are defined using temporal logic. In model checking process, verification tool checks whether requirements are satisfied in attached system model. If this is not the case, appropriate counterexamples are generated.
    Praca prezentuje metodę formalnej weryfikacji specyfikacji sterownika logicznego uwzględniającą właściwości podane przez użytkownika. Specyfikacja sterownika logicznego może być przedstawiona m.in. w postaci sieci Petriego lub diagramu aktywności języka UML. Diagramy aktywności wydają się być bardziej przyjazne i zrozumiałe dla użytkownika niż sieci Petriego. Specyfikacja w postaci diagramu aktywności może zostać przekształcona do sieci Petriego, która następnie może być formalnie zweryfikowana i wykorzystana do automatycznej generacji implementacji (kodu). Węzły diagramu aktywności konsekwentnie interpretowane są jako tranzycje sieci Petriego, w odróżnieniu od klasycznego podejścia (w starszych wersjach UML) gdzie odwzorowywało się je jako miejsca sieci Petriego. Proces weryfikacji wykonywany jest automatycznie przez narzędzia weryfikacji modelowej. Tworzony jest opis modelu bazujący na specyfikacji oraz lista wymagań. Nowatorskim podejściem jest przedstawienie sieci Petriego na poziomie RTL w taki sposób, że łatwo jest przeprowadzić syntezę logiczną sieci w postaci współbieżnego rekonfigurowalnego sterownika logicznego lub sterownika PLC bez konieczności przekształcania modelu. Wymagania określone są przy użyciu logiki temporalnej. W procesie weryfikacji modelowej narzędzie weryfikujące NuSMV sprawdza, czy model systemu spełnia stawiane mu wymagania. Jeżeli tak nie jest, generowany jest odpowiedni kontrprzykład.
    Źródło:
    Zeszyty Naukowe. Telekomunikacja i Elektronika / Uniwersytet Technologiczno-Przyrodniczy w Bydgoszczy; 2010, 13; 79-91
    1899-0088
    Pojawia się w:
    Zeszyty Naukowe. Telekomunikacja i Elektronika / Uniwersytet Technologiczno-Przyrodniczy w Bydgoszczy
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Offline signature verification based on shape contexts using shared and user-specific thresholds
    Autorzy:
    Adamski, M.
    Saeed, K.
    Powiązania:
    https://bibliotekanauki.pl/articles/333777.pdf
    Data publikacji:
    2013
    Wydawca:
    Uniwersytet Śląski. Wydział Informatyki i Nauki o Materiałach. Instytut Informatyki. Zakład Systemów Komputerowych
    Tematy:
    offline signature verification (SV)
    shape contexts
    weryfikacja podpisu w trybie offline
    Opis:
    In this paper we present a system for offline signature verification based on Shape Context Descriptors. The system input are binarized images of handwritten signatures from GPDS database available for non-commercial research. During preprocessing each signature image is thinned using KMM algorithm in order to obtain 1-pixel wide skeleton. The feature vector is built from Shape Context Descriptors computed for selected points on skeletonized signature line. The verification process is based on the distance measure that uses Shape Context Descriptors. The presented system is evaluated using random and skilled forgeries with shared and user-specific thresholds.
    Źródło:
    Journal of Medical Informatics & Technologies; 2013, 22; 195-201
    1642-6037
    Pojawia się w:
    Journal of Medical Informatics & Technologies
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Offline signature identification and verification using noniterative shape context algorithm
    Autorzy:
    Adamski, M.
    Saeed, K.
    Powiązania:
    https://bibliotekanauki.pl/articles/333019.pdf
    Data publikacji:
    2009
    Wydawca:
    Uniwersytet Śląski. Wydział Informatyki i Nauki o Materiałach. Instytut Informatyki. Zakład Systemów Komputerowych
    Tematy:
    weryfikacja podpisu
    offline signature verification (SV)
    signature identification
    shape context method
    Opis:
    The paper presents experimental results on offline signature identification and verification. At the first stage of the presented system, the binary image of the signature undergoes skeletonization process using KMM algorithm to have a thinned, one pixel-wide line, to which a further reduction is applied. For each thinned signature image a fixed number of points comprising the skeleton line are selected. The recognition process is based on comparing the reference signatures with the questioned samples using distance measure computed by means of Shape Context algorithm. The experiments were carried out using a database containing signatures of 20 individuals. For the verification process random forgeries were used to asses the system error. The main advantage of the presented approach lies in utilizing only one reference signature for both identification and verification tasks, whereas the achieved results are comparable with respect to the systems that use several training samples per subject.
    Źródło:
    Journal of Medical Informatics & Technologies; 2009, 13; 47-52
    1642-6037
    Pojawia się w:
    Journal of Medical Informatics & Technologies
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Signature verification using contextual information enhancement and dynamic programming
    Autorzy:
    Adamski, M.
    Saeed, K.
    Powiązania:
    https://bibliotekanauki.pl/articles/332874.pdf
    Data publikacji:
    2008
    Wydawca:
    Uniwersytet Śląski. Wydział Informatyki i Nauki o Materiałach. Instytut Informatyki. Zakład Systemów Komputerowych
    Tematy:
    weryfikacja podpisu online
    programowanie dynamiczne
    online signature verification
    feature context
    dynamic programming
    Opis:
    This paper presents the results of experiments on online signature verification. Information gathered during the signing process like pen trajectory, pressure, elevation and altitude is utilized to prove the authenticity of a signature or to detect a forgery attempt. Signature verification task is carried out by means of the Template Matching approach. The presented method is based on the signature description in terms of its local features and their relations. The comparison of features in the reference and tested signatures is conducted using Dynamic Time Warping technique.
    Źródło:
    Journal of Medical Informatics & Technologies; 2008, 12; 35-40
    1642-6037
    Pojawia się w:
    Journal of Medical Informatics & Technologies
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Dual synthesis of Petri net based application specific logic controllers with increased safety
    Autorzy:
    Tkacz, J.
    Bukowiec, A.
    Adamski, M.
    Powiązania:
    https://bibliotekanauki.pl/articles/200217.pdf
    Data publikacji:
    2016
    Wydawca:
    Polska Akademia Nauk. Czytelnia Czasopism PAN
    Tematy:
    critical safety
    FPGAs
    logic controllers
    logic synthesis
    Petri nets
    verification
    bezpieczeństwo krytyczne
    FPGA
    sterowniki logiczne
    synteza logiczna
    sieci Petriego
    weryfikacja
    Opis:
    In the paper, design flow of the application specific logic controllers with increased safety by means of Petri nets is proposed. The controller architecture is based on duplicated control unit and comparison results from both units. One specification of control algorithm is used by means of Petri net for both units. The hardware duplication is obtained during dual synthesis process. This process uses two different logic synthesis methods to obtain two different hardware configurations for both control units. Additionally, the dual verification is applied to increase reliability of the control algorithm. Such design flow simplifies the process of realization of control systems with increased safety.
    Źródło:
    Bulletin of the Polish Academy of Sciences. Technical Sciences; 2016, 64, 3; 467-478
    0239-7528
    Pojawia się w:
    Bulletin of the Polish Academy of Sciences. Technical Sciences
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
    Tytuł:
    Reprezentacja przestrzeni stanów sterownika logicznego z wykorzystaniem kodowanych diagramów decyzyjnych
    Reconfigurable Logic Controller state space representation using encoded Binary Decision Diagrams
    Autorzy:
    Bubacz, P.
    Adamski, M.
    Powiązania:
    https://bibliotekanauki.pl/articles/152669.pdf
    Data publikacji:
    2007
    Wydawca:
    Stowarzyszenie Inżynierów i Techników Mechaników Polskich
    Tematy:
    1st order nonstationary measurement system
    rekonfigurowane sterowniki logiczne
    kodowanie stanów
    synteza logiczna
    weryfikacja formalna
    Ordered Binary Decision Diagram
    Reconfugurable Logic Controller
    state encoding
    logic synthesis
    formal verification
    Opis:
    W pracy porównano znane z literatury metody zwartej reprezentacji przestrzeni stanów dla rekonfigurowanego sterownika logicznego. Przedstawiono zalety heurystycznego sposobu kodowania miejsc sieci Petriego, dzięki któremu uzyskuje się diagramy OBDD o znacznie mniejszej złożoności przydatne zarówno podczas analizy, jak i syntezy układowej algorytmu sterowania binarnego.
    In the paper some known methods for an effective representation of the state space in reconfigurable logic controller are compared. The advantages of heuristic method of Petri net place encoding, which is adapted for a compact encoding technique of Binary Decision Diagrams, are given.
    Źródło:
    Pomiary Automatyka Kontrola; 2007, R. 53, nr 5, 5; 24-26
    0032-4140
    Pojawia się w:
    Pomiary Automatyka Kontrola
    Dostawca treści:
    Biblioteka Nauki
    Artykuł
      Wyświetlanie 1-6 z 6

      Ta witryna wykorzystuje pliki cookies do przechowywania informacji na Twoim komputerze. Pliki cookies stosujemy w celu świadczenia usług na najwyższym poziomie, w tym w sposób dostosowany do indywidualnych potrzeb. Korzystanie z witryny bez zmiany ustawień dotyczących cookies oznacza, że będą one zamieszczane w Twoim komputerze. W każdym momencie możesz dokonać zmiany ustawień dotyczących cookies