Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 2009

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: algorytmiczna maszyna stanów

Sortuj według:

Ogranicz wyniki do:

Formalna weryfikacja maszyny stanów z wykorzystaniem logiki temporalnej

Grobelna I.

Pomiary Automatyka Kontrola

2009

R. 55, nr 7

457-460

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).

Decrease of the number of PAL macrocells for Moore FSM

Barkalov A. A., Titarenko L., Chmielewski S.

Pomiary Automatyka Kontrola

2009

R. 55, nr 7

476-478

Method of decrease in the number of PAL macrocells in logic circuit of Moore FSM is proposed. This method is based on the implementation of free outputs of embedded memory blocks to represent the code of the class of the pseudoequivalent states. The proposed approach allows minimizing hardware without decreasing of the digital system performance. An example of application of the proposed method is given.

Wzrost zużycia zasobów sprzętowych jest jednym z aktualnych problemów w logicznych układach jednostki sterującej. Specyficzną cechą układu PAL jest duża ilość wejść makrokomórek i ilość termów na makrokomórkę. Cechą automatów Moore'a jest istnienie pseudorównoważnych stanów i regularny charakter mikrooperacji, które daje się implementować z użyciem EMB (ang. Embedded Memory Blocks). W tym artykule proponowana jest metoda pozwalająca zmniejszyć wykorzystanie zużycia sprzętowego bez zmniejszania wydajności systemów cyfrowych, przy użyciu wyżej wspomnianych cech.