Liczba stanów modelu
Wykorzystanie RAM [GB] 0 5 10 15 2 500 5 000 7 500 10 000 12 500 15 000 17 500 Zmierzone wykorzystanie pamięci operacyjne 0,298 + -1,33E-04x + 3,79E-08x^2 R² = 0,998
Rysunek 5.9: Wykres zale˙zno´sci wymaganej przez nuXmv pami˛eci operacyjnej od liczby stanów weryfiko-wanego modelu systemu po translacji.
5.4 Podsumowanie
Rezultatem tego etapu bada´n było zakwestionowanie sensu translacji grafu LTS do innego j˛ezyka modelo-wania jak to zostało zrobione w przypadku integracji z nuXmv. Modelowanie przestrzeni stanów zamiast bezpo´srednio systemu nie pozwala narz˛edziom do weryfikacji na zastosowanie zaimplementowanych opty-malizacji i chocia˙z daje prawidłowe wyniki, to pewnej bariery zło˙zono´sci systemu nie mo˙zna w ten sposób przekroczy´c. W kolejnym rozdziale przedstawiony zostanie sposób cz˛e´sciowej mitygacji tego problemu, a nast˛epnie przedstawione zostanie podej´scie alternatywne, pozwalaj ˛ace na weryfikacj˛e systemów o wyso-kiej zło˙zono´sci.
Rozdział 6
Wykorzystanie rozwi ˛aza´n chmurowych do
weryfikacji modeli Alvis
W poprzednim rozdziale pokazana została słabo´s´c weryfikacji w nuXmv, polegaj ˛aca na bardzo wysokim zu˙zyciu pami˛eci operacyjnej. Wyniki uzyskane na standardowym sprz˛ecie komputerowym pozwoliły jed-nak wysnu´c hipotez˛e, ˙ze posiadaj ˛ac odpowiednio wi˛eksz ˛a ilo´s´c dost˛epnych zasobów, podej´scie to mo˙zna wykorzysta´c nawet dla bardziej zło˙zonych modeli.
W tym rozdziale przedstawione zostan ˛a wyniki testów na rozwi ˛azaniach chmurowych na platformie Google Cloud (GCP).
6.1 Chmury obliczeniowe
Pomimo post˛epuj ˛acej redukcji kosztów komponentów w stosunku do oferowanej mocy obliczeniowej i pa-mi˛eci operacyjnej, wykonywanie zło˙zonych oblicze´n i przetwarzanie du˙zej ilo´sci danych na własnej in-frastrukturze okazuje si˛e bardzo drogie. Problem ten jest szczególnie bolesny dla firm, gdzie stworzenie własnego centrum obliczeniowego wymaga wysokich inwestycji z góry na infrastruktur˛e sprz˛etow ˛a oraz wi ˛a˙ze si˛e z wysokimi kosztami utrzymania. Wymaga bowiem zatrudnienia zespołu ludzi do zarz ˛adzania, zabezpieczania, instalacji, konfiguracji i wielu innych codziennych czynno´sci.
Problemem s ˛a te˙z koszty komponentów przeznaczonych do niecodziennych zastosowa´n, jak np. wery-fikacja modelowa, wymagaj ˛aca bardzo du˙zej ilo´sci pami˛eci operacyjnej ze wzgl˛edu na problem eksplozji stanów. Zakup sprz˛etu pozwalaj ˛acego na weryfikacj˛e du˙zych modeli jest cz˛esto nieosi ˛agalny dla zwykłych u˙zytkowników czy nawet ´sredniej wielko´sci przedsi˛ebiorstw czy o´srodków naukowych.
Z pomoc ˛a przychodz ˛a jednak platformy oferuj ˛ace rozwi ˛azania oparte o chmury obliczeniowe. Chmury obliczeniowe s ˛amodelem przetwarzania danych umo˙zliwiaj ˛acym powszechny i wygodny dost˛ep na ˙z ˛adanie poprzez sie´c do współdzielonej puli konfigurowalnych zasobów obliczeniowych (tj. sieci, serwerów,
6.1. Chmury obliczeniowe 71
strzeni dyskowej, aplikacji czy usług), które mog ˛aby´c wynajmowane i zwalniane przy minimalnym wysiłku i interakcji z dostawc ˛a [87].
6.1.1 Wirtualizacja zasobów
Przetwarzanie w chmurze opiera si˛e na technologii wirtualizacji. Istniej ˛a dwa typy wirtualizacji – wirtuali-zacja aplikacji i wirtualiwirtuali-zacja serwerów [99]. Pierwsza z nich polega na dostarczaniu jednej aplikacji wielu u˙zytkownikom, dzi˛eki czemu mo˙zna znacz ˛aco obni˙zy´c koszty jej utrzymania, a wi˛ec równie˙z koszty korzy-stania z aplikacji. Wirtualizacja serwerów polega na wykorzystaniu wspólnej infrastruktury sprz˛etowej do hostowania maszyn wirtualnych, z których ka˙zda mo˙ze korzysta´c z innego systemu operacyjnego i innego zestawu aplikacji, dzi˛eki czemu mo˙zliwa jest optymalizacja wykorzystania współdzielonych zasobów.
Chmury obliczeniowe nadbudowuj ˛a technologie wirtualizacji o szereg mechanizmów ułatwiaj ˛acych ko-rzystanie z udost˛epnionych zasobów i aplikacji, w tym moduły raportowania, zarz ˛adzania, monitorowania, skalowania czy rozlicze´n.
6.1.2 Modele usług chmurowych
Chmury obliczeniowe udost˛epniaj ˛a usługi w kilku modelach, b˛ed ˛acych niejako kolejnymi poziomami abs-trakcji [99]. Trzy podstawowe modele to:
• Infrastructure-as-a-service (IaaS) - Dostarczenie infrastruktury sprz˛etowej (serwery, przestrze´n dys-kowa itd.), opłacana za wykorzystane zasoby. Do przykładów IaaS zaliczane s ˛a Amazon Web Servi-ces, Microsoft Azure i Google Compute Engine.
• Platform-as-a-service (PaaS) - Podobnie jak IaaS ale zawiera równie˙z system operacyjny i inne przy-datne aplikacje ´srodowiska operacyjnego umo˙zliwiaj ˛ace instalacj˛e i uruchomienie oprogramowania. Popularnymi przykładami PaaS s ˛a Google App Engine i AWS Elastic Beanstalk.
• Software-as-a-service (SaaS) - Dostarczenie hostowanej aplikacji spełniaj ˛acej konkretn ˛afunkcj˛e. Wy-korzystanie aplikacji nie wymagaj ˛a instalacji na własnej infrastrukturze. Przykładami takich aplikacji s ˛a np. Google G Suite, Microsoft Office 365 czy Dropbox.
W ostatnim czasie powstały równie˙z dodatkowe modele, w szczególno´sci, Information-as-a-service (INaaS) dostarczaj ˛acy informacje istotne dla konsumenta, procesu biznesowego czy zadania oraz model Business-Process-as-a-service (BPaaS) wypełniaj ˛acy dane zadanie lub zast˛epuj ˛acy dany proces biznesowy w organizacji.
6.1.3 Dostawcy rozwi ˛aza´n chmurowych
W ostatnich latach powstało wiele platform chmurowych. Ró˙zni ˛a si˛e nieco je´sli chodzi o oferowany zastaw narz˛edzi, sposób ich wykorzystania i cennik. Zakres usług i ich koszt regulowany jest przez umow˛e o
gwa-6.1. Chmury obliczeniowe 72
rantowanym poziomie ´swiadczenia usług mi˛edzy dostawc ˛a a konsumentem (ang. Service Level Agreement – SLA) [71].
Do najpopularniejszych dostawców rozwi ˛aza´n chmurowych nale˙z ˛aAmazon Web Services (AWS) [100], Google Cloud Platform (GCP) [36] oraz Microsoft Azure [88]. Ka˙zda z tych platform dostarcza kompletny zestaw rozwi ˛aza´n chmurowych w tym do oblicze´n, przechowywana danych, zarz ˛adzania zabezpieczeniami, zarz ˛adzania sieci ˛a, programowania, uczenia maszynowego, analityki i wielu innych [121].
6.1.4 Zalety rozwi ˛aza´n chmurowych
Popularyzacji chmur obliczeniowych drastycznie zmieniła podej´scie do przetwarzania danych, umo˙zliwia-j ˛ac bardzo prosty i tani dost˛ep do dopasowanych do aktualnego zapotrzebowania zasobów. Do niew ˛atpli-wych zalet rozwi ˛aza´n chmuro˛atpli-wych nale˙zy zaliczy´c:
• Redukcj˛e kosztów – Podstawow ˛azalet ˛ajest redukcja kosztów inwestycyjnych. Modele chmurowe nie wymuszaj ˛a od konsumenta inwestycji z góry. Dodatkowo konsument płaci jedynie za wykorzystane w zasoby lub usługi, które mo˙ze wł ˛acza´c i wył ˛acza´c w zale˙zno´sci od potrzeb.
• Skalowalno´s´c – Potrzeby zwi ˛azane z wykorzystanie zasobów zmieniaj ˛asi˛e dynamicznie. W tradycyj-nym modelu nale˙załoby z góry zakupi´c i utrzymywa´c infrastruktur˛e pod maksymalne przewidywane obci ˛a˙zenie. Przy wykorzystaniu rozwi ˛aza´n chmurowych konsument ma mo˙zliwo´s´c dowolnego skalo-wania wykorzystywanych zasobów, elastycznie zwi˛ekszaj ˛ac lub zmniejszaj ˛ac ich ilo´s´c w zale˙zno´sci od potrzeb.
• Czas wdro˙zenia – Czas wdro˙zenia na rozwi ˛azania chmurowe jest drastycznie szybszy od czasu po-trzebnego do postawienia własnej infrastruktury. Ta cecha chmur obliczeniowych nie tylko redukuje czas wprowadzania rozwi ˛aza´n na rynek, ale równie˙z umo˙zliwia przeprowadzanie szybkich ekspery-mentów. Jest to szczególnie wa˙zne w przypadku wykorzystania chmur do weryfikacji modelowej. • Niezawodno´s´c – usługi chmurowe posiadaj ˛a szereg mechanizmów pozwalaj ˛acych zminimalizowa´c
ryzyko niedost˛epno´sci usługi i szybkiego powrotu do pracy. Dzi˛eki temu, za stosunkowo niewielk ˛a cen˛e w porównaniu do tradycyjnych metod, mo˙zna zabezpieczy´c si˛e na wypadek awarii sprz˛etu, przerw w dostawie energii czy nawet katastrof naturalnych.
• Bezpiecze´nstwo – Wbrew niektórym mitom, rozwi ˛azania chmurowe s ˛a w przewa˙zaj ˛acej wi˛ekszo´sci przypadków znacznie bezpieczniejsze ni˙z rozwi ˛azania oparte na własnej infrastrukturze. Jest to spo-wodowane tym, ˙ze dostawcy usług chmurowych posiadaj ˛a sztab ludzi odpowiadaj ˛acych za bezpie-cze´nstwo danych przechowywanych na ich serwerach. Rozwi ˛azania chmurowe dbaj ˛a równie˙z o stał ˛a aktualizacj˛e oprogramowania i zabezpiecze´n.