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.

Description

Development of the rewrite-based framework.

The rewrite-based framework that is needed to execute programming language definitions and formal program analysis tools based on these. The framework will be designed around the following idea: the programming languages, calculi, as well as type systems or formal analysis tools can be defined making use of special list and/or set structures, called cells, which can be potentially nested.

Techniques and methodologies to define and analyze complex language features.

Some frameworks provide a “well-chosen” set of constructs, shown to be theoretically sufficient to define any computable function or algorithm, and then propose encodings of other language features into the set of basic ones; examples in this category are Turing machines or the plethora of (typed or untyped) lambda-calculi, or pi-calculi, etc. While these basic constructs yield interesting and meaningful idealized programming languages, using them to encode other language features is, in our view, inappropriate. Indeed, encodings hide the intended computational granularity of the defined language constructs; for example, a variable lookup intended to be a one-step operation in one’s language should take precisely one step in an ideal framework (not hundreds/thousands of steps as in a Turing machine or lambda calculus encoding, not even two steps: first get location, then get value).

Implementation of the rewrite framework.

Maude started as an algebraic specification language belonging to the OBJ family. Meanwhile, it became a strong programming language, including powerful features: a fast rewrite engine modulo associativity-commutativity, reflection capabilities, tools for analyzing specifications. Therefore we intend to use Maude as a first platform for implementing the framework. This implementation will be rather a prototype which should demonstrate that the design of the framework is appropriate to our purpose. Then we may think on a specialized rewrite engine, where the focus will on the efficiency.

Matching logic-based program verification.

We propose a new logic, namely matching logic. suitable for verifying programs written in any language defined in the rewrite platform. Matching logic, unlike Hoare logics, does not encode the entire program state in a formula. The rationale is that by keeping the configuration structure unaltered, one can more easily relate it to the actual program state and identify, by means of pattern matching, mathematical objects to reason about.

Matching logic is tightly connected to rewriting logic semantics (RLS): matching logic formal systems can systematically be obtained from executable RLS of languages. This relationship allows to prove soundness of matching logic formal systems w.r.t. complementary, testable semantics.

Executable semantics of both existing and paradigmatic programming languages.

For each main programming paradigm (imperative programming, object-oriented programming, functional programming, concurrency, parallelism and so on) a representative language will be considered for defining and analyzing it in the new framework.

Behavioral Analysis with CIRC.

CIRC is a theorem prover built on both circular coinduction and circular induction, developed as a joint work between Alexandru Ioan Cuza University and University of Illinois at Urbana Champaign. The current version of CIRC is able to prove coinductive properties of infinite data structures, automata and processes. The target is to use CIRC to verify and analyze programs. A simple scenario is: since the platform allows to define both the specification and the programming language, we can verify a program against its specification by checking the equivalence between program and its specification.

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)

Publications

2015

2014

2013

2012

2011

2010

Sidebar