An Executable Semantic Framework for Rigorous Design, Analysis and Testing of Systems (DAK)

We use the algebraic specifications and their execution by rewriting in order to reach this objective. The basic idea is to have a uniform way for giving semantics to programming languages. Then use this semantics to obtain tools for analysis: model checking, run-time verification, theorem proving-based verification, testing, behavioral analysis, etc.

RO

Obiectivul proiectului 

Principalul obiectiv al proiectului este dezvoltarea unui framework (cadru de lucru) formal (riguros) pentru proiectarea, specificarea semanticii şi analiza software. Ideea nouă introdusă de acest proiect este aceea că activităţile principale din cadrul dezvoltării software (limbaje sau sisteme noi) sunt realizate utilizând acelaşi framework.

Obiectivul este atins prin utilizarea specificaţiilor algebrice şi execuţia lor prin rescriere. Ideea de bază este de a construi semantica limbajelor de programare într-o manieră uniformă şi de a o utiliza pentru a obţine unelte de analiză: model checking, verificare run-time, verificare bazată pe demonstratoare de teoreme, testare, analiză comportamentală, etc.

Ţinta principală a proiectului este crearea unei echipe în cadrul Universităţii Alexandru Ioan Cuza (UAIC), coordonată de Grigore Roşu (profesor asociat, angajat al Universităţii din Illinois Urbana-Champaign (UIUC), SUA), în scopul proiectării şi implementării framework-ului.

Descrierea componentelor proiectului 

Identificăm următoarele componente principale ale proiectului:

Proiectarea cadrului de lucru (framwork-ului) bazat pe rescrieri 

Framework-ul bazat pe rescrieri este necesar pentru execuţia definiţiilor limbajelor de programare şi analiza formală utilizând unelte construite în jurul acestora. Framework-ul va fi proiectat în jurul următoarei idei: limbajele de programare, calculele, precum şi sistemele de tipuri sau uneltele de analiză formală pot fi definite cu ajutorul structurilor speciale tip liste sau mulţimi, numite celule, care pot fi încuibărite.

Tehnici şi metodologii pentru definirea şi analiza trăsăturilor complexe de limbaj. 

Unele framework-uri pun la dispoziţie un set de construcţii „bine alese”, care sunt teoretic suficiente pentru definirea oricărei funcţii calculabile sau algoritm şi propun codificări pentru alte trăsături de limbaj într-un set de trăsături de bază. Exemple din această categorie sunt maşinile Turing, lamba-calculul (tipizat sau netipizat) sau pi-calculul. În timp ce aceste construcţii de bază sunt potrivite pentru anumite limbaje de programare, utilizarea lor pentru codificarea altor trăsături de limbaj este, din punctul nostru de vedere, nepotrivită. Într-adevăr, codificările ascund nivelul dorit de granularitate a construcţiilor de limbaj definite; de exemplu, accesarea unei variabile (care este o operaţie ce consumă un singur pas de timp) ar trebui să dureze exact un pas de timp într-un framework ideal (nu sute/mii de paşi, ca în cazul maşinilor Turing sau codificărilor din lambda calcul; nici măcar doi paşi: întâi accesarea locaţiei, apoi a valorii).

Implementarea framework-ului bazat pe rescriere 

Maude a început ca un limbaj pentru specificaţii algebrice, făcând parte din familia OBJ. Între timp a devenit un limbaj de programare puternic, incluzând trăsături puternice: un motor de rescriere rapid modulo asociativ-comutativ, capacităţi de reflexie, unelte pentru analiza specificaţiei. Implementarea cu ajutorul Maude va fi un prototip care va demonstra că design-ul framework-ului este potrivit pentru scopul nostru. Ne vom putea gândi apoi la un motor de rescriere specializat, unde ne vom axa pe eficienţă.

Verificarea programelor bazate pe logica potrivirilor (matching logic) 

Propunem o nouă logică numită logica potrivirilor (matching logic), potrivită pentru verificarea programelor scrise în orice limbaj definit în cadrul platformei de rescriere. Logica potrivirilor, spre deosebire de logica Hoare, nu codifică întregul program într-o formulă de stare. Menţinănd configuraţia structurii nealterată, aceasta poate fi relaţionată mai uşor cu starea programului în sine şi poate identifica, prin intermediul potrivirilor pe şabloane, obiecte matematice asupra cărora se pot face raţionamente.

Logica potrivirilor este în strânsă legătură cu semantica logicii rescrierilor (RLS): sistemele formale din logica potrivirilor pot fi obţinute sistematic din semantica RLS executabilă a limbajelor. Această relaţie permite demonstrarea corectitudinii sistemelor specificate în logica potrivirilor.

Semantică executabilă pentru limbajele de programare şi paradigmele existente. 

Pentru fiecare paradigmă de programare principală (programare imperativă, programare orientată obiect, programare funcţională, concurenţă, paralelism, etc.), vom considera câte un limbaj reprezentativ pentru definirea şi analiza acestuia cu ajutorul noului framework.

Analiză comportamentală utilizând CIRC. 

CIRC este un demonstrator de teoreme având la bază atât coinducţia, cât şi inducţia circulară, dezvoltat în urma colaborării dintre Universitatea Alexandru Ioan Cuza şi Universitatea din Illinois, Urbana Champaign. Versiunea curentă a CIRC permite demonstrarea proprietăţilor coinductive pentru structuri infinite, automate şi procese. Scopul este de a utiliza CIRC în verificarea şi analiza programelor. Un scenariu simplu este: devreme ce platforma ne permite să definim atât limbajul de specificare, cât şi cel de programare, putem verifica dacă programul este conform cu specificaţia, verificând echivalenţa dintre program şi specificaţie.

Anexa la Raportul fiinal (Descrierea modului de indeplinire a indicatorilor de mai sus)