Metode formale în ingineria software la FII

Sigla Facultății de Informatică din IașiArticolul de față prezintă o serie de cercetări aliniate cu precădere problematicilor informaticii teoretice în ceea ce privește ingineria software.

Astfel, prezentăm două dintre proiectele grupului Formal Methods in Software Engineering inițiat și condus de profesorul Dorel Lucanu. Alți membri ai grupului sunt profesorul Gheorghe Grigoraș și studenții doctoranzi Ionuț Apetrei, Măriuca Asăvoae și Mihail Asăvoae, plus masterandul Andrei Arusoaie.

Verificare automată prin circularități
Sigla FMSE (Formal Methods in Software Engineering)

Proiectul CIRC (demarat în 2007 pe o perioadă de trei ani) își propune să extindă sistemul Maude cu un motor de demonstrare construit în jurul coinducției circulare și a implementării circulare a inducției structurale. Unul dintre scopuri îl reprezintă investigarea manierei în care noul mediu – o alternativă la metodele actuale bazate pe model-checking și analiză statică a programelor – poate fi utilizat la verificarea automată de software și a specificațiilor de sisteme.

CIRC este un demonstrator automatizat, implementat în Full Maude, ca o extensie comportamentală a sistemului Maude. De asemenea, CIRC moștenește atât performanța, cât și instrumentele de analiză ale întregului sistem Maude. Demonstratorul utilizează proprietatile logicii rescrierii (rewriting logic) în ceea ce privește introspecția și lucrul la meta-nivel.

O versiune online a demonstratorului poate fi obținută vizitând pagina UIUC destinată CIRC.

Colaboratorii la acest proiect sunt Formal Systems Laboratory din cadrul University of Illinois, Urbana-Champaign și Centrum voor Wiskunde en Informatica, Vrije Universiteit Amsterdam.

DAK: proiectare, specificarea semanticii și analiză software

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

Obiectivul este atins prin recurgerea la specificații algebrice și executia 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 instrumente de analiză: model checking, verificare run-time, verificare bazată pe demonstratoare de teoreme, testare, analiză comportamentală etc.

Proiectarea și implementarea framework-ului sunt realizate de o echipă formată din membri ai Facultății de Informatică din Universitatea „Alexandru Ioan Cuza” (UAIC) și de membri ai Laboratorului de Sisteme Formale din Universitatea Illinois din Urbana-Champaign (UIUC), coordonată de Grigore Roșu – profesor asociat la UAIC și profesor permanent la UIUC.

Alte direcții de cercetare în cadrul FII au fost descrise în cadrul însemnărilor anterioare De la identificarea de microARN la detecția de malware și De la procesarea limbajului natural la ‘Bring IT on’.

2 Răspunsuri to “Metode formale în ingineria software la FII”

  1. Sabin Buraga Says:

    A se parcurge și interviul cu profesorul Dorel Lucanu „Perioada de studenție e una în care se poate visa și îndrăzni foarte multe!” apărut în Ziarul de ASII.


Comentariile sunt închise.

%d blogeri au apreciat asta: