Librería Samer Atenea
Kálamo Books
Librería Elías (Asturias)
Librería Kolima (Madrid)
Librería Proteo (Málaga)
Książka ta skupia się na wykorzystaniu języka Event-B jako formalnej metody modelowania i weryfikacji oprogramowania. Naszym studium przypadku jest system sterowania windą (ECS). Wymagania dotyczące windy są przekładane na matematyczne modele Event-B. Używamy RODIN do opracowywania, testowania i weryfikacji modeli ECS Event-B, zanim będziemy mogli zaimplementować system w programie komputerowym. Modelowanie w Event-B jest tak istotne, że pozwala nam zidentyfikować brakujące wymagania, błędy w naszym projekcie i udowodnić, że model systemu będzie działał zgodnie z oczekiwaniami, w przeciwieństwie do sytuacji, gdybyśmy opracowywali system natychmiast po otrzymaniu wymagań od klienta. Wymagania te są niekompletne i niejednoznaczne. Dzięki wykorzystaniu Event-B zmniejszamy koszty rozwoju systemu, ponieważ błędy są zawsze wykrywane na wczesnych etapach rozwoju. Przejście od fazy wymagań do fazy formalnej specyfikacji jest jednym z najtrudniejszych etapów. W rzeczywistości tworzenie wstępnych modeli na podstawie wymagań systemowych wymaga wysokiego poziomu kompetencji i praktycznych umiejętności w zakresie modelowania Event-B. Ponieważ nie ma dobrze zdefiniowanego procesu, który mógłby służyć jako przewodnik dla inżynierów systemowych, niniejsza książka przedstawia praktyczne podejście do tworzenia dobrych systemów oprogramowania.
