Wyniki wyszukiwania - Biblioteka Nauki

Nowa wersja platformy, zawierająca wyłącznie zasoby pełnotekstowe, jest już dostępna.
Przejdź na https://bibliotekanauki.pl

Ograniczanie wyników

3 2011

3 Grobelna I.

Znaleziono wyników: 3

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Formal verification of embedded logic controller specification with computer deduction in temporal logic

100%

Grobelna I.

2011

tom R. 87, nr 12a

47-50

The article presents a novel approach to formal verification of logic controller specification. Model checking technique is used to verify some behavioral properties. The approach proposes to use a rule-based logical model presented at RTL-level. Proposed logical model is suitable both for formal verification (model checking in the NuSMV tool) and for logical synthesis (using hardware description language VHDL). As the result, logic controller program (its implementation) will be valid according to its primary specification.

Artykuł przedstawia nowatorskie podejście do formalnej weryfikacji specyfikacji sterownika logicznego. Zaproponowany został regułowy model logiczny, który jest dogodny zarówno do formalnej weryfikacji (weryfikacja modelowa w narzędziu NuSMV), jak również do syntezy logicznej (z użyciem języku opisu sprzętu VHDL). Program sterownika logicznego (jego implementacja) będzie zatem poprawny względem początkowej specyfikacji.

Wprowadzenie do weryfikacji i symulacji w środowisku NuSMV

100%

Grobelna I.

2011

tom nr 1

23-30

Specyfikacja systemu informatycznego jest jednym z pierwszych etapów jego tworzenia i stanowi fundament dalszych prac. Na tym etapie projektu określany jest sposób działania systemu oraz właściwości jego pracy. Należy zadbać o to, aby specyfikacja była w pełni poprawna, a zaprojektowany system spełniał wszystkie stawiane mu wymagania . Jedną z metod walidacji specyfikacji jest weryfikacja oraz symulacja modelu systemu. Oba zadania mogą zostać wykonane w środowisku NuSMV.

The article is a short introduction into model checking and simulation in the NuSMV environment. The NuSMV tool allows description offinite state machines FSM and their verification using temporal logic formulas. Using a simple example (traffic lights), basic rules and commands of model checking and simulation process are presented. Using the NuSMV environment it is possible to detect some errors at an early stage of system development.

Automatyczna weryfikacja i synteza regułowego modelu sterownika logicznego

100%

Grobelna I.

2011

tom nr 3

59-65

The article focuses on model checking and synthesis of rule-based specification of logic controller. It describes and illustrates proposed design system of logic controllers. Specification by means of Control Interpreted Petri Nets is formally written as rule-based logical model, which is suitable both for formal verification against behavioral requirements and for synthesis in form of reconfigurable logic controller. Verifiable model is thereby consistent with synthesizable model. Logical model is also used for behavioral verification and simulation. Translation process of rule-based specification into verifiable model description and synthesizable code has been automated.