Menu
  • Specyfikacje ilościowe: uczenie się, algorytmy i zastosowania

    Kierownik: dr hab. Jan Otop
    Okres realizacji: 2018-2021
    Projekt badawczy finansowany przez Narodowe Centrum Nauki

    W dzisiejszych czasach systemy informatyczne stanowią nieodłączną część życia. Mimo dużych postępów w dziedzinach inżynierii
    oprogramowania i testowania, wciąż napotyka się na różnego rodzaju błędy, zarówno w sprzęcie, jak i w oprogramowaniu. Aby wyeliminować błędy zaproponowano formalną weryfikację, w której dowodzi się poprawności programów i układów cyfrowych. Formalna weryfikacja jest intensywnie badana teoretycznie oraz intensywnie rozwijana w przemyśle: Intel stosuje ją przy tworzeniu procesorów; Microsoft i Facebook stosują ją przy tworzeniu oprogramowania; Bosch stosuje ją przy projektowaniu tempomatów w samochodach. Wiodącą techniką w formalnej weryfikacji jest weryfikacja modeli, w ramach której sprzęt lub oprogramowanie abstrahuje się do uproszczonych struktur, nazywanych \emph{modelami}, celem dokonania weryfikacji ich poprawności.

    Weryfikacja modeli daje odpowiedź jakościową: ,,tak'' albo ,,nie''. Pozwala to odpowiadać na pytania w stylu ,,czy serwer odpowie na każde żądanie''. Jednak odpowiedź pozytywna na takie pytanie jest często niewystarczająca, gdyż nie określa, jak szybko serwer odpowie. Dlatego ważne są również aspekty ilościowe, na przykład pytanie ,,jaki jest średni czas pomiędzy żądaniem a odpowiedzią serwera''. Aby móc wnioskować o aspektach ilościowych systemów, stosuje się ilościową weryfikację modeli, w której można zadawać wartości liczbowe oraz otrzymywać liczby jako  odpowiedzi. Takie odpowiedzi niosą ze sobą więcej informacji, które lepiej oddają poprawność systemu. Pomimo swoich zalet, ilościowa weryfikacja modeli nie jest używana w praktyce z powodu licznych trudności. Opisywanie własności ilościowych jest trudne, problem weryfikacji własności  ilościowych jest obliczeniowo trudny, a interpretacja ilościowych odpowiedzi jest trudna. Celem tego projektu jest zniwelowanie powyższych trudności.

    W tym projekcie badawczym postaramy się usprawnić proces ilościowej weryfikacji modeli skupiając się na trzech etapach weryfikacji: specyfikacji własności ilościowych, algorytmach weryfikacji modeli względem własności ilościowych, oraz interpretacji odpowiedzi ilościowych zwracanych w procesie weryfikacji.

    Aby uczynić proces tworzenia specyfikacji łatwiejszym dla użytkowników, będziemy badali obliczeniowe uczenie się specyfikacji
    oraz języki zadawania specyfikacji. Będziemy badać dwa rodzaje problemów: uczenie \emph{offline}, w którym użytkownik jednorazowo podaje pewną listę przykładów i na ich podstawie generowana jest specyfikacja, oraz uczenie online, w czasie którego algorytm może zadawać użytkownikowi dodatkowe pytania dotyczące słów, a także pytać, czy dana specyfikacja jest taka, jak żądano. Podobne techniki uczenia się z powodzeniem sprawdzają się w klasycznej weryfikacji.

    Zakładając, że mamy zadaną specyfikację ilościową, kolejnym krokiem w weryfikacji jest obliczenie jej wartości na danym modelu systemu. Modele często bywają bardzo duże, dlatego ważne jest znajdowanie efektywnych algorytmów do weryfikacji, a w szczególności takich, które korzystają z technik pozwalających operować na mniejszy modelach. W tym projekcie podejmiemy próbę stworzenia takich algorytmów dla weryfikacji ilościowej.

    Podobnie jak w oprogramowaniu, błędy mogą się również zdarzać w specyfikacjach. Może to prowadzić do sytuacji, gdy w wyniku
    weryfikacji otrzymujemy informację, że nasz system zachowuje się poprawnie, podczas gdy tak nie jest. Planujemy stworzyć narzędzia wspomagające wykrywanie tego typu przypadków. Celem takich narzędzi byłoby wskazywanie użytkownikowi, że jego specyfikacja, na przykład, jest spełniona podejrzanie łatwo lub że wynik procesu weryfikacji nie zależy od dużej części modelu.

  • Automaty z wagami dla własności kwantytatywnych - Kierownik: dr Jan Otop

    Okres realizacji: 2015-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Logiki do przetwarzania danych i weryfikacji - Kierownik: dr Jakub Michaliszyn

    Okres realizacji: 2015-2018

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Hipoteza BDD/FC i okolice - Kierownik: mgr Tomasz Gogacz

    Okres realizacji: 2014-2017

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Wokół logik modalnych - rozstrzygalność i złożoność - Kierownik: dr Jakub Michaliszyn

    Okres realizacji: 2012-2015

    Projekt badawczy finansowany przez Narodowe Centrum Nauki

  • Zagadnienia złożoności i rozstrzygalności dla teorii logicznych motywowanych informatyką - Kierownik: prof. dr hab. Jerzy Marcinkowski

    Okres realizacji: 2010-2013

    Projekt badawczy finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Automatyczne wnioskowanie w teoriach równościowych (promotorski) - Kierownik: prof. dr hab. Jerzy Marcinkowski

    Okres realizacji: 2009-2010

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Rozstrzygalność pewnych teorii logicznych motywowanych teorią informatyki - Kierownik: dr hab. Jerzy Marcinkowski

    Okres realizacji: 2006-2009

    Projekt finansowany przez Ministerstwo Nauki i Szkolnictwa Wyższego

  • Specyfikacje ilościowe: uczenie się, algorytmy i zastosowania

    Kierownik: dr hab. Jan Otop
    Okres realizacji: 2018-2021
    Projekt badawczy finansowany przez Narodowe Centrum Nauki

     

    Wdzisiejszychczasachsystemyinformatycznestanowa˛nieodła˛czna˛cze˛´ s´ c ˙zycia. Mimodu˙zych poste˛pów w dziedzinach in˙zynierii oprogramowania i testowania, wcia˛˙z napotyka sie˛ na ró˙znego rodzajubłe˛dy,zarównowsprze˛cie,jakiwoprogramowaniu. Abywyeliminowa´cbłe˛dyzaproponowano formalna˛weryfikacje˛, w której dowodzi sie˛ poprawno´sci programów i układów cyfrowych. Formalnaweryfikacjajestintensywniebadanateoretycznieorazintensywnierozwijanawprzemy´ sle: Intel stosuje ja˛przy tworzeniu procesorów; Microsoft i Facebook stosuja˛ja˛przy tworzeniu oprogramowania; Bosch stosuje ja˛ przy projektowaniu tempomatów w samochodach. Wioda˛ca˛ technika˛w formalnej weryfikacji jest weryfikacja modeli, w ramach której sprze˛t lub oprogramowanie abstrahuje sie˛ do uproszczonych struktur, nazywanych modelami, celem dokonania weryfikacji ich poprawno´sci. Weryfikacja modeli daje odpowiedz´ jako´sciowa˛: „tak” albo „nie”. Pozwala to odpowiada´c na pytania w stylu „czy serwer odpowie na ka˙zde ˙za˛danie”. Jednak odpowiedz´ pozytywna na takie pytanie jest cze˛sto niewystarczaja˛ca, gdy˙z nie okre´sla, jak szybko serwer odpowie. Dlatego wa˙zne sa˛ równie˙z aspekty ilo´sciowe, na przykład pytanie „jaki jest ´sredni czas pomie˛dzy ˙za˛daniem a odpowiedzia˛serwera”. Aby móc wnioskowa´c o aspektach ilo´sciowych systemów, stosuje sie˛ ilo´ sciowa˛weryfikacje˛ modeli, w której mo˙zna zadawa´c warto´sci liczbowe oraz otrzymywa´c liczby jako odpowiedzi. Takie odpowiedzi niosa˛ze soba˛wie˛cej informacji, które lepiej oddaja˛poprawno´ s´c systemu. Pomimo swoich zalet, ilo´sciowa weryfikacja modeli nie jest u˙zywana w praktyce z powodu licznych trudno´sci. Opisywanie własno´sci ilo´sciowych jest trudne, problem weryfikacji własno´sciilo´sciowychjestobliczeniowotrudny,ainterpretacjailo´sciowychodpowiedzijesttrudna. Celem tego projektu jest zniwelowanie powy˙zszych trudno´sci. W tym projekcie badawczym postaramy sie˛ usprawni´c proces ilo´sciowej weryfikacji modeli skupiaja˛csie˛ natrzechetapachweryfikacji: specyfikacjiwłasno´sciilo´sciowych,algorytmachweryfikacji modeli wzgle˛dem własno´sci ilo´sciowych, oraz interpretacji odpowiedzi ilo´sciowych zwracanych w procesie weryfikacji. Aby uczyni´c proces tworzenia specyfikacji łatwiejszym dla u˙zytkowników, be˛dziemy badali obliczeniowe uczenie sie˛ specyfikacji oraz je˛zyki zadawania specyfikacji. Be˛dziemy bada´c dwa rodzaje problemów: uczenie offline, w którym u˙zytkownik jednorazowo podaje pewna˛liste˛ przykładów i na ich podstawie generowana jest specyfikacja, oraz uczenie online, w czasie którego algorytm mo˙ze zadawa´c u˙zytkownikowi dodatkowe pytania dotycza˛ce słów, a tak˙ze pyta´c, czy dana specyfikacja jest taka, jak ˙za˛dano. Podobne techniki uczenia sie˛ z powodzeniem sprawdzaja˛ sie˛ w klasycznej weryfikacji. Zakładaja˛c, ˙zemamyzadana˛specyfikacje˛ ilo´sciowa˛,kolejnymkrokiemwweryfikacjijestobliczenie jej warto´sci na danym modelu systemu. Modele cze˛sto bywaja˛bardzo du˙ze, dlatego wa˙zne jest znajdowanie efektywnych algorytmów do weryfikacji, a w szczególno´sci takich, które korzystaja˛ z technik pozwalaja˛cych operowa´c na mniejszy modelach. W tym projekcie podejmiemy próbe˛ stworzenia takich algorytmów dla weryfikacji ilo´sciowej. Podobnie jak w oprogramowaniu, błe˛dy moga˛ sie˛ równie˙z zdarza´c w specyfikacjach. Mo˙ze to prowadzi´c do sytuacji, gdy w wyniku weryfikacji otrzymujemy informacje˛, ˙ze nasz system zachowuje sie˛ poprawnie, podczas gdy tak nie jest. Planujemy stworzy´c narze˛dzia wspomagaja˛ce wykrywanie tego typu przypadków. Celem takich narze˛dzi byłoby wskazywanie u˙zytkownikowi, ˙ ze jego specyfikacja, na przykład, jest spełniona podejrzanie łatwo lub ˙ze wynik procesu weryfikacji nie zale˙zy od du˙zej cze˛´sci modelu.