Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: diagram stanów

Sortuj według:

Ogranicz wyniki do:

Maszyna Turinga - podstawy działania i programowania

Gawryś Katarzyna

MINUT Matematyka i Informatyka na Uczelniach Technicznych

2023

Nr 5

264-272

Maszyna Turinga jest opracowanym przez Alana Turinga ideowym modelem programowania. Ten abstrakcyjny model urządzenia służył do zapisu i wykonania algorytmów. Niniejszy artykuł opisuje budowę i sposób działania maszyny Turinga oraz zasady zapisu algorytmów w postaci tabeli przejść. W artykule umieszczono przykład użycia symulatora maszyny Turinga do rozwiązania przykładowego zadania. Analiza zamieszczonego przykładu, pozwoli odbiorcy, na przyswojenie sposobu szukania rozwiązania problemu, dla ideowego modelu komputera, jakim jest maszyna Turinga.

Jak zapewnić poprawności działania programów komputerowych?

Greniewski M. J.

Studia i Materiały / Europejska Uczelnia Informatyczno-Ekonomiczna w Warszawie

2015

Nr 2(10)

1--15

Narasta problem skutków błędów w oprogramowaniu. Konieczna stała się zmiana podejścia – zapewnienie poprawności działania programów komputerowych. Dotyczy to głównie programów współbienych – reaktywnych. Metody formalne pozwalają na zastąpienie metody testowania programów (o wątpliwej skuteczności) metodami walidacji, czyli dowodzenia poprawności działania przez sprawdzanie stanów osiagąnych przez model sterowania programu. Podstawą jest pomysł użycia logiki temporalnej do opisu działania programów współbiernych Amira Pnueli z 1977 roku, który został rozwinięty na początku lat osiemdziesiątych ubiegłego wieku w teorie przez Clarke’a, Emersona oraz Sifakisa (uhonorowani w 2007 r. ACM A.M. Turing Award). Wzmiankowana teorie zastosowano w języku modelowania Promela oraz procesorze Spin (Simple Promela Interpreter) autorstwa zespołu Gerarda J. Holzmanna (uhonorowanego w 2002 r. ACM Software System Award).

There is a growing tendency of the effects of bugs in the software. It becomes necessary to change the approach – to ensure proper operation of computer programs. This applies mainly to concurrent programs – reactive ones. Formal methods allow substitution of the method of testing programs (of dubious efficacy) by validation methods, which is proving the correctness of the action – by checking the status achieved by the control model program. The basis is the idea of using temporal logic to describe the actions of concurrent programs by Amir Pnueli from 1977, further developed in the early eighties of the last century into the theory of Clarke, Emerson and Sifakis (honored in 2007 ACM A.M. Turing Award). The theory mentioned above, was used in modeling language Promela and Spin processor (Simple Promela Interpreter) by Gerard J. Holzmann team (which won the 2002 ACM Software System Award).