An Executable Semantic Framework for Rigorous Design, Analysis and Testing of Systems (DAK)
Programul Operational Sectorial “Cresterea Competitivitatii Economice”
AXA Prioritara 2, Operatiunea 2.1.2
“Investitii pentru viitorul dumneavoastra”
Contract 161/15.06.2010, SMIS-CSNR 602-12516
Proiect Un Cadru de Lucru bazat pe Semantica Executabila pentru Proiectarea Riguroasa, Analiza si Testarea Sistemelor, acronim DAK
Proiect cofinantat prin Fondul European de Dezvoltare Regionala
Pentru informatii detaliate despre celelalte programe operationale cofinantate de
Uniunea Europeană va invitam sa vizitati www.fonduri-ue.ro
Continutul acestui material nu reprezinta în mod obligatoriu pozitia oficială a Uniunii Europene sau a Guvernului Romaniei
Research
EN RO ObjectivesThe main objective of the project is to supply a formal method-based framework for software design, semantics and analysis. The novelty idea of the project is that the main activities in software development, which could be a new language or a new system, are realized using the same framework. 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.
|
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) |