A dolgozat párhuzamos programok tervezésének egy olyan matematikai modelljét adja meg, amely kiterjesztése a nemdeterminisztikus szekvenciális programok relációs alapú modelljének [[???Fót 83]] és egyben relációs szemantikai modellje a UNITY logikának [[???Cha Mis 89]]. A modell támogatja párhuzamos programok szintézisét, eszközkészlete bővebb, mint a szekvenciális modellé vagy a UNITY-é.
A programozási feladatok megfogalmazására és megoldására korábban sikeresen alkalmazott módszereket [[???Dij 76, ???Fót Hor 91]] a dolgozatban ismertetett eredmények felhasználásával párhuzamos programokra is alkalmazhatjuk. A megközelítés funkcionális, más hasonló párhuzamos programozási modellektől eltérően a feladatnak önálló szemantikai jelentése van, így a lépésenkénti finomítás a feladatok és nem a programok felett értelmezett reláció. Az absztrakt program és tulajdonságai a temporális logikával rokon UNITY logikából [[???Cha Mis 89]] ismert programfogalom relációs alapú megfogalmazásai.
A modell definiálja a specifikációs reláció, a programozási feladat, feladat finomítása, kiterjesztése, feltételes értékadás, absztrakt párhuzamos program, feladat kiterjesztése, nyitott specifikáció, utasítás és program kiterjesztése, programtulajdonságok, viselkedési reláció, megoldás fogalomrendszerét. A modell specifikációs eszközeinek kifejezőereje meghaladja a lineáris temporális logika alapú UNITY kifejezőerejét, folyamatok alternatív viselkedésének specifikálására is alkalmas.
Formálisan definiáltuk programok szekvenciáját, bevezettük a UNITY-ből ismert programkonstrukciókat, az uniót és a szuperpozíciót. Kimondtunk levezetési szabályokat, amelyek segítségével a lépésenkénti finomítás során kapott feladatok megoldása után az eredeti feladat megoldását könnyen megadhatjuk.
A modell alapfogalmainak alkalmazását két programozási tétel szintézise során mutattuk be. Az asszociatív művelet eredményeinek párhuzamos kiszámítására levezetett tétel az egyik leggyakrabban előforduló feladatosztály esetére nyújt aszinkron architektúrán is hatékonyan implementálható, verifikált megoldást. Elemenként feldolgozható függvények eredményének párhuzamos kiszámítására alkalmas programozási tételt ismereteink szerint a szakirodalomban elsőként a dolgozatban ismertetett modellben fogalmaztunk meg.
A modell fogalomrendszere alkalmazható párhuzamos programozás oktatásáraAz asszociatív függvény kiszámításának tételét eddig már kb. 200 hallgató alkalmazta a gyakorlatban is sikeresen konrét feladatok megoldása során.. A fogalomrendszerbe könnyen illeszkedik az üzenetküldés, a szinkron és aszinkron kommunikáció, a csatornaváltozó fogalma [[???Hor 93-96]]. Az adatcsatornás megoldási módszerekre [[???Cha Mis 89]] a modell eszközeivel levezetett programozási tételt [[???Hor 93-96]] is sikeresen alkalmazták a gyakorlatban.
Az eredmények alkalmazása során megfogalmazásra került egy formális modell, amely absztrakt és implementált programok kapcsolatrendszerének leírására alkalmas [[???Hor 93-96]]. Több szakdolgozat foglalkozott azzal a kérdéssel, hogy a modellben hogyan adható meg a típus fogalma, illetve a UNITY modellhez hasonlóan [[???Sin 91]] hogyan specifikálható osztott objektumok viselkedése [[???Fáb 94, ???Győr 94]].
További kutatást igényel a haladási tulajdonságok és a programkonstrukciók viszonya. Kidolgozandó osztott objektumok viselkedését megadó absztrakt programok szintézisének gyakorlatban is alkalmazható módszertana. A modell nem rendelkezik elegáns eszközökkel valós idejű problémák specifikációjára [[???Car 94]]. Nehézséget okoz a kompozicionalitás biztosítása valós párhuzamosság esetén [[???Cha 90]].