Temat: model checking - Katalog OPAC zbiorów

Skocz do pozycji: 1.

Tytuł:: UML Verification with Verics
Autorzy:: Niewiadomski, A.
Penczek, W.
Powiązania:: https://bibliotekanauki.pl/articles/92916.pdf
Data publikacji:: 2007
Wydawca:: Uniwersytet Przyrodniczo-Humanistyczny w Siedlcach
Tematy:: model checking
UML
unified modeling language
VerICS
Opis:: We show how to verify UML specifications against properties expressed by CTL-like formulas using the symbolic model checker Verics. Our method is illustrated with an example showing a verification of Alternating Bit Protocol.
Źródło:: Studia Informatica : systems and information technology; 2007, 1(8); 19-31
1731-2264
Pojawia się w:: Studia Informatica : systems and information technology
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Skocz do pozycji: 2.

Tytuł:: Model Checking Temporal Properties of Reaction Systems
Weryfikacja temporalnych własności systemów reakcyjnych
Autorzy:: Męski, A.
Penczek, W.
Rozenberg, G.
Powiązania:: https://bibliotekanauki.pl/articles/182724.pdf
Data publikacji:: 2014
Wydawca:: Polska Akademia Nauk. Instytut Podstaw Informatyki PAN
Tematy:: reaction systems
model checking
temporal logic
systemy reakcyjne
weryfikacja modelowa
logika temporalna
Opis:: This paper defines a temporal logic for reaction systems (RSTL). The logic is interpreted over the models for the context restricted reaction systems that generalize standard reaction systems by controlling context sequences. Moreover, a translation from the context restricted reaction systems into boolean functions is defined in order to be used for a symbolic model checking for RSTL over these systems. Finally, model checking for RSTL is proved to be PSPACE-complete.
Praca wprowadza logikę temporalną dla systemów reakcyjnych (RSTL), która jest interpretowana w modelach dla systemów reakcyjnych z ograniczeniami kontekstów. Systemy te uogólniają standardowe systemy reakcyjne przez wprowadzenie ograniczeń kontrolujących dopuszczalne konteksty. Ponadto, przedstawiono translację z systemów reakcyjnych z ograniczeniami kontekstów do formuł boolowskich, która umożliwia symboliczną weryfikację modelową dla tych systemów oraz RSTL. Wykazano również, że problem weryfikacji modelowej dla RSTL jest problemem PSPACE-zupełnym.
Źródło:: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk; 2014, 1028; 1-28
0138-0648
Pojawia się w:: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
Dostawca treści:: Biblioteka Nauki

Artykuł

Zmień widok

na półce

Informacja

Wyszukujesz frazę "model checking" wg kryterium: Temat

Źródło danych

Dostawca treści

Kolekcja

Rok wydania

Wydawca

Temat

Autor

Typ dokumentu

Język