Rebeca (programovací jazyk) - Rebeca (programming language)

Rebecca (zkratka pro Reactive Objects Language) je herec -na základě modelovací jazyk s formálním základem navrženým ve snaze překlenout propast mezi přístupy formálního ověřování a skutečnými aplikacemi. Lze jej považovat za referenční model pro souběžný výpočet na základě operativní interpretace modelu aktéra. Je to také platforma pro vývoj objektových souběžných systémů v praxi.

Kromě vhodného a efektivního způsobu modelování souběžných a distribuovaných systémů je třeba zajistit přístup k formálnímu ověření, aby byla zajištěna jejich správnost. Rebeca je podporována sadou ověřovacích nástrojů. Dřívější nástroje poskytovaly rozhraní pro práci s kódem Rebeca a překlad kódu Rebeca do vstupních jazyků známých a vyspělých kontrolních modelů (jako SPIN a NuSMV), a tak byly schopny ověřit jejich vlastnosti. Rebeca, od roku 2005 , je podporován přímou kontrolou modelu založenou na Modere (Model checking Engine of Rebeca). Modulární ověřovací a abstrakční techniky se používají ke zmenšení stavového prostoru a umožňují ověřit komplikované reaktivní systémy. Kromě těchto technik podporuje Modere částečné pořadí redukce a redukce symetrie.

Reference

  • M. Sirjani. Formální specifikace a ověření souběžných a reaktivních systémů, Disertační práce, Katedra počítačového inženýrství, Sharif University of Technology, prosinec 2004.
  • M. Sirjani, A. Movaghar. Objektově orientovaný model pro agenty, ve sborníku workshopů o agentech pro správu informací, Rakouská počítačová společnost, říjen 2002.

Viz také

externí odkazy