Informacja

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

Wyszukujesz frazę "formal checking" wg kryterium: Temat


Wyświetlanie 1-2 z 2
Tytuł:
An automatic formal verification tool for schematic-level design of an electrical project
Narzędzie do automatycznej weryfikacji formalnej schematu ideowego sprawdzające poprawność schematu już we wczesnych etapach procesu projektowego
Autorzy:
Szelest, M.
Powiązania:
https://bibliotekanauki.pl/articles/152251.pdf
Data publikacji:
2014
Wydawca:
Stowarzyszenie Inżynierów i Techników Mechaników Polskich
Tematy:
Electrical Fault Detection
Formal Verification
Design Rule Checking
Electrical Rule Checking
wykrywanie błędów
weryfikacja formalna
sprawdzanie reguł projektowych
sprawdzanie reguł elektrycznych
Opis:
Schemat ideowy układu elektronicznego może być postrzegany jako zbiór wzajemnie połączonych komponentów elektronicznych tworzących pewien graf połączeń. Graf ten jest strukturą, której topologia może być odczytana i przeanalizowana. Automatyczna weryfikacja formalna schematu ideowego ma na celu wykrycie nietrywialnych błędów (związanych ze strukturą tegoż schematu), popełnionych przez projektanta w trakcie opracowywania schematu. Błędy te są efektem pominięcia lub niewłaściwego wykorzystania elementów elektronicznych w typowych podukładach (blokach funkcjonalnych). W artykule opisano realizację komputerowego narzędzia wspomagającego proces automatycznej weryfikacji formalnej, począwszy od określenia sposobu zapisu schematu, przez integrację z komercyjnymi narzędziami EDA (ang. Electronic Design Automation) aż po określenie algorytmów identyfikujących podobwody. Opracowane narzędzie umożliwia dokonanie weryfikacji schematu ideowego już w bardzo wczesnych etapach procesu projektowego, co znacząco redukuje liczbę pętli w procesie projektowym, wpływając korzystnie na końcowy koszt opracowania produktu oraz skracając czas niezbędny do przygotowania urządzenia do produkcji.
A schematic diagram can be interpreted as set of components connected together to build a network. The network is a structure whose topology can be read and analyzed. The automatic formal verification aims at detecting some non-trivial mistakes, made by an electrical engineer, connected with the structure of schematic, building blocks and typical functional sub circuits. The paper presents the approach for realization of an automatic formal detection tool starting from the definition of schematic structure, through connectivity with a schematic-capture tool, to a sub-circuit identification algorithm.
Źródło:
Pomiary Automatyka Kontrola; 2014, R. 60, nr 6, 6; 369-372
0032-4140
Pojawia się w:
Pomiary Automatyka Kontrola
Dostawca treści:
Biblioteka Nauki
Artykuł
Tytuł:
Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej
Formal verification of a state machine with use of temporal logic
Autorzy:
Grobelna, I.
Powiązania:
https://bibliotekanauki.pl/articles/154298.pdf
Data publikacji:
2009
Wydawca:
Stowarzyszenie Inżynierów i Techników Mechaników Polskich
Tematy:
algorytmiczne maszyny stanów ASM
logika temporalna
technika Model Checking
algorithmic state machines ASM
temporal logic
formal verification of specification
Model Checking technique
Opis:
Artykuł przedstawia koncepcję specyfikacji współbieżnego procesu sterowania cyfrowego za pośrednictwem diagramów algorytmicznych maszyn stanów ASM w języku aprobowanym przez profesjonalne narzędzie model checker. Specyfikacja może zostać następnie formalnie zweryfikowana pod kątem wymagań stawianych projektowanemu systemowi. Lista wymagań tworzona jest przy wykorzystaniu liniowej logiki temporalnej LTL. Formalna weryfikacja Model Checking polega na sprawdzeniu, czy model systemu spełnia stawiane mu wymagania. W przypadku wykrycia niespóności generowany jest odpowiedni kontrprzykład.
The paper presents the formal specification method of concurrent control processes in form of algorithmic state machines ASM [5] in a language accepted by a professional model checker tool NuSMV. Basing on linear temporal logic LTL [7, 8, 9, 16] a requirement list (Fig. 6) for the system model is prepared. Formal verification Model Checking [17, 19] consists in comparison of the model description and the requirements list. If some requirements cannot be fulfilled, the appropriate counterexample is generated (Fig. 7), which allows localizing the error source. The ASM diagrams (Fig. 4) are fully determined, but they do not support modularity, that is why they are not well suited for specification of concurrent controlling processes. The paper includes a short introduction to the theory of algorithmic state machines ASM (Section 2), temporal logic (Section 3) and model checking technique (Section 4). The proposed solution is presented on an example (Section 5) of the process of controlling (partially concurrent) movements of two vehicles (Fig. 2). The formal verification method of the ASM diagrams with its advantages and disadvantages as well as the general conclusions are given at the end of the paper (Section 6).
Źródło:
Pomiary Automatyka Kontrola; 2009, R. 55, nr 7, 7; 457-460
0032-4140
Pojawia się w:
Pomiary Automatyka Kontrola
Dostawca treści:
Biblioteka Nauki
Artykuł
    Wyświetlanie 1-2 z 2

    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