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.
PL
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.
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.
EN
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.
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.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.