Zasady sprawdzania modelu
 Przednia okładka
| |
| Autor | Christel Baier i Joost-Pieter Katoen |
|---|---|
| Temat | Sprawdzanie modelu |
| Wydawca | MIT Press |
Data publikacji |
25 kwietnia 2008 |
| Strony | 975 |
| ISBN | 9780262026499 |
Principles of Model Checking to podręcznik dotyczący sprawdzania modeli , dziedziny informatyki , która automatyzuje problem ustalenia, czy maszyna spełnia wymagania specyfikacji. Został napisany przez Christel Baier i Joosta-Pietera Katoena i opublikowany w 2008 roku przez MIT Press .
Streszczenie
Wprowadzenie i pierwszy rozdział zarysowują dziedzinę sprawdzania modeli : model maszyny lub procesu można przeanalizować, aby sprawdzić, czy zachowują się pożądane właściwości. Na przykład automat sprzedający może spełniać właściwość „saldo nigdy nie może spaść poniżej 0,00 €”. Gra wideo może egzekwować zasadę „jeśli gracz ma 0 żyć, gra kończy się porażką”. Zarówno automat sprzedający, jak i grę wideo można modelować jako systemy przejściowe . Sprawdzanie modelu to proces opisywania takich wymagań w języku matematycznym i automatyzujący dowód, że model spełnia wymagania, lub odkrywanie kontrprzykłady , jeśli model jest wadliwy.
Rozdział drugi skupia się na stworzeniu odpowiedniego modelu dla systemów współbieżnych , w których wiele części algorytmu ( zestawu instrukcji) może być realizowanych jednocześnie przez różne maszyny lub części maszyny.
W rozdziale 3 omówiono typy reguł, które może spełniać system przejściowy: liniowe właściwości czasu . Właściwość bezpieczeństwa , taka jak „nie są możliwe żadne stany zakleszczenia ”, ma postać „nigdy nie może wystąpić niepożądany wynik”. Właściwość dotycząca żywotności , taka jak „współdzielony zasób zawsze zostanie ostatecznie udostępniony komponentowi, który o to poprosi”, ma postać „ostatecznie nastąpi pożądany wynik”. Jako warunki wstępne można zastosować właściwości uczciwości, takie jak „sygnalizacja świetlna nigdy nie przestaje zmieniać koloru”. tj. założenia, z których można wywnioskować inne właściwości.
Rozdział czwarty dotyczy właściwości języków regularnych i ω-regularnych oraz maszyn teoretycznych, takich jak automaty Büchiego , które modelują języki. Zawiera algorytmy sprawdzania modelu umożliwiające weryfikację właściwości lub znalezienie kontrprzykładów.
Rozdziały piąty i szósty omawiają liniową logikę temporalną (LTL) i logikę drzewa obliczeniowego (CTL), dwie klasy formuł wyrażających właściwości. LTL koduje wymagania dotyczące ścieżek w systemie, takie jak „każdy w Monopoly nieskończenie często przechodzi „Go””; CTL koduje wymagania dotyczące stanów w systemie, takie jak „z dowolnej pozycji wszyscy gracze mogą ostatecznie wylądować w „Go””. CTL* , które łączą obie gramatyki. Podano algorytmy formuł sprawdzających modele w tych logikach.
Rozdział siódmy bada formalne sposoby porównywania systemów przejściowych, takich jak bisymulacja ; ósma dotyczy częściowych redukcji rzędu , których celem jest zmniejszenie liczby obliczeń wymaganych do sprawdzenia właściwości modelu. Rozdziały dziewiąty i dziesiąty dotyczą rozszerzeń logiki i automatów rozważanych wcześniej, w tym poprzez dodanie częstotliwości zegara ( automaty czasowe ) lub prawdopodobieństw ( automaty probabilistyczne oparte na łańcuchach Markowa ).
Przyjęcie
François Laroussinie w The Computer Journal polecił tę książkę badaczom, wykładowcom, studentom i inżynierom, nazywając ją „imponującą”. Laroussinie uznał, że podręcznik jest napisany obszernie i przystępnie, zawiera dużą liczbę przykładów, ćwiczeń i motywujących pomysłów dotyczących kluczowych koncepcji. W ramach „ujednoliconej struktury” pierwsze siedem rozdziałów obejmuje teorię klasyczną, a trzy ostatnie rozdziały obejmują rozszerzenia sprawdzania modeli.
W ACM Computing Reviews Gabriel Ciobanu uważa, że podręcznik ten może być stosowany na zaawansowanych kursach licencjackich i magisterskich oraz będzie przydatny dla badaczy. Ciobanu pochwalił „jasną i intuicyjną” prezentację i stwierdził, że „należy ją docenić za pedagogiczne podejście do omawiania podstawowych pojęć, dogłębnych wyników teoretycznych i zaawansowanych tematów w badaniach nad sprawdzaniem modeli”.
W 2014 roku książka znalazła się w gronie pięciu najczęściej cytowanych tekstów naukowych monitorowanych przez Book Citation Index (BKCI).
Dalsza lektura
-
Lange, Martin (2010), MathSciNet , MR 2493187
{{ cytat }}: CS1 maint: periodyk bez tytułu ( link )