REAL

Elosztott funkcionális programok helyessége = Verification of distributed functional programs

Horváth, Zoltán and Csörnyei, Zoltán and Kozma, László and Kozsik, Tamás and Pásztorné dr. Varga, Katalin and Tejfel, Máté and Zsók, Viktória (2007) Elosztott funkcionális programok helyessége = Verification of distributed functional programs. Project Report. OTKA.

[img]
Preview
PDF
37742_ZJ1.pdf

Download (146kB)

Abstract

Biztonsági szempontból kritikus elosztott alkalmazások fejlesztéséhez számos új eszközt, modellt, helyességbizonyítási módszert és programozási nyelvi elemet hoztunk létre: megalkottuk funkcionális programok temporális tulajdonságai leírásának modelljét, kiterjesztettünk egy helyességbizonyító rendszert, altípusok invariánsainak kezelésére és bizonyítására új típuslevezetési rendszert terveztünk, új magasszintű nyelvi elemeket vezettünk be elosztott funkcionális programok leírásához. Kidolgoztuk az objektum-absztrakció funkcionális programozási modelljét a Clean nyelvhez. Megalkottuk a CPPCC módszert: az általunk temporális tulajdonságok bizonyítására is alkalmassá tett helyességbizonyítóval elkészítjük a kód tulajdonságainak bizonyítását géppel ellenőrizhető formában, majd a kódhoz hozzácsomagoljuk a bizonyított tulajdonságokat. A kiterjesztett helyességbizonyítóhoz megadtuk az új nyelvi elemek szintaxis és szemantikai definícióit, megjelennek az absztrakt objektumok, a specifikációs nyelvben megfogalmazhatók invariánsok és biztonságossági tulajdonságok. Megadtunk egy új altípusrendszert annotációk bevezetésével. Az annotációkkal megfogalmazott programtulajdonságokat részben a nyelv fordítóprogramja bizonyítja, részben a tételbizonyító rendszer segítségével lehet azokat bizonyítani. Megalkottuk a Clean nyelv egy kiterjesztését, amelynek segítségével funkcionális stílusban, magas absztrakciós szinten írhatunk elosztott funkcionális programot. | We introduced new models, tools and programming language concepts to support development of components of distributed safety critical applications. In a pure functional language functional variables are constants, but in case of interactive or distributed programs, or in ones that use IO we consider a series of values computed from each other as different states of the same abstract object. We developed a method to describe abstract objects and temporal properties in an extended version of Core language of the Clean Sparkle theorem prover and we extended the proof system to deal with temporal properties. We proposed CPPCC, a three-parties model of property carrying mobile code exchange. We designed also an extension to the type system which enables to express some safety properties of the program. The idea is to annotate types with type invariants and using subtype and belive-me marks. The annotations can express pre- and postconditions of functions, as well as propagation of properties. Those properties of programs that the annotations describe are either verified by the type checker of the compiler, or turned into theorems to prove by the theorem prover. The distributed evaluation of functions and the communication between Clean programs need a higher level process description and control mechanism. For this reason a control language, the D-Clean language and an intermediate level language, the D-Box language, and their informal semantics were introduced.

Item Type: Monograph (Project Report)
Uncontrolled Keywords: Informatika
Subjects: Q Science / természettudomány > QA Mathematics / matematika > QA76 Computer software / programozás
Depositing User: Mr. Andras Holl
Date Deposited: 08 May 2009 11:00
Last Modified: 30 Nov 2010 23:38
URI: http://real.mtak.hu/id/eprint/333

Actions (login required)

Edit Item Edit Item