Rebeka (język programowania)
Rebeca (skrót od Reactive Objects Language) to oparty na aktorach język modelowania z formalnymi podstawami, zaprojektowany w celu wypełnienia luki między formalnymi podejściami do weryfikacji a rzeczywistymi aplikacjami. Można go uznać za model odniesienia dla obliczeń współbieżnych, oparty na operacyjnej interpretacji modelu aktora. Jest to również platforma do tworzenia w praktyce systemów współbieżnych opartych na obiektach.
Oprócz posiadania odpowiedniego i wydajnego sposobu modelowania systemów współbieżnych i rozproszonych, potrzebne jest formalne podejście do weryfikacji, aby zapewnić ich poprawność. Rebeca jest wspierana przez zestaw narzędzi weryfikacyjnych. Wcześniejsze narzędzia zapewniały front-end do pracy z kodem Rebeca i tłumaczenia kodu Rebeca na języki wprowadzania dobrze znanych i dojrzałych kontrolerów modeli (takich jak SPIN i NuSMV), a tym samym były w stanie zweryfikować ich właściwości. Rebeca od 2005 roku jest wspierana przez bezpośredni kontroler modeli oparty na Modere (Silnik sprawdzania modeli firmy Rebeca). Modułowe techniki weryfikacji i abstrakcji stosowane są w celu zmniejszenia przestrzeni stanów i umożliwienia weryfikacji skomplikowanych systemów reaktywnych. Oprócz tych technik, Modere obsługuje częściową redukcję rzędów i redukcję symetrii.
Zobacz też
- M. Sirjani. Formalna specyfikacja i weryfikacja systemów współbieżnych i reaktywnych, rozprawa doktorska , Wydział Inżynierii Komputerowej, Sharif University of Technology, grudzień 2004.
- M. Sirjani, A. Movaghar. Model obiektowy dla agentów, w Proceedings of Workshop on Agents for Information Management, Austrian Computer Society, październik 2002.
Linki zewnętrzne