Czasopismo | PRZEGLĄD ELEKTROTECHNICZNY | Rocznik 2011 - zeszyt 12a

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

Iwona GROBELNA

nr katalogowy: 64233

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. Streszczenie. 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. (Formalna weryfikacja specyfikacji wbudowanych sterowników logicznych z wykorzystaniem wnioskowania komputerowego w logice temporalnej). Keywords: formal verification, embedded logic controllers, temporal logic. Słowa kluczowe: formalna weryfikacja, wbudowane sterowniki logiczne, logika temporalna. 1. Introduction Embedded logic controllers specification is the first step in development process. Possible errors in this phase [1] may influence oncoming phases or even the whole venture. Usually, it generates enormous costs to remove errors which were detected too late. Dependable embedded logic controllers have additional requirements which requires beside high quality also reliability, availability, safety and secureness. Even a tiny error in design phase may change the total system behavior and may have tragic effects. One of commonly used formal techniques by logic controllers specification are Petri Nets (PN) [2,3], and especially Control Interpreted Petri Nets (CIPN) [3,4]. They a[...]

Jeśli masz wykupiony/przyznany dostęp - zaloguj się. Skorzystaj z naszych propozycji zakupu!

Publikacja


e-Publikacja (format pdf) - nr 64233 "Formal verification of em..." licencja: Osobista Produkt cyfrowy	10.00 zł

Zeszyt


PRZEGLĄD ELEKTROTECHNICZNY - e-zeszyt (pdf) 2011-12a licencja: Osobista Produkt cyfrowy	55.00 zł

Prenumerata

PRZEGLĄD ELEKTROTECHNICZNY - prenumerata cyfrowa
licencja: Osobista

Produkt cyfrowy
Nowość

762.00 zł

PRZEGLĄD ELEKTROTECHNICZNY - PAKIET prenumerata PLUS
licencja: Osobista

Szczegóły pakietu

Nazwa
PRZEGLĄD ELEKTROTECHNICZNY - PAKIET prenumerata PLUS (Prenumerata papierowa + dostęp do portalu sigma-not.pl + e-prenumerata)	1002.00 zł brutto 927.78 zł netto 74.22 zł VAT (stawka VAT 8%)

1002.00 zł

PRZEGLĄD ELEKTROTECHNICZNY - papierowa prenumerata roczna + wysyłka
licencja: Osobista

Szczegóły pakietu

Nazwa
PRZEGLĄD ELEKTROTECHNICZNY - papierowa prenumerata roczna	960.00 zł brutto 888.89 zł netto 71.11 zł VAT (stawka VAT 8%)
PRZEGLĄD ELEKTROTECHNICZNY - pakowanie i wysyłka	42.00 zł brutto 34.15 zł netto 7.85 zł VAT (stawka VAT 23%)

1002.00 zł

Zeszyt

2011-12a

Twój Koszyk

Publikacja

Zeszyt

Prenumerata

Zeszyt

Czasopisma