Provably correct graph transformations with small-tALC

Nadezhda Baklanova (1) , Jon Haël Brenas (2) , Rachid Echahed (2) , Christian Percebois (3) , Martin Strecker (1) , Hanh Nhi Tran (3)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 UGA [2016-2019] - Université Grenoble Alpes [2016-2019]
3 IRIT-MACAO - Modèles, Architectures, Composants, Agilité et prOcessus

We present a prototype for executing and verifying graph transformations. The transformations are written in a simple imperative programming language, and pre-and post-conditions as well as loop invariants are specified in the Description Logic ALC (whence the name of the tool). The programming language has a precisely defined operational semantics and a sound Hoare-style calculus. The tool consists of the following sub-components: a compiler to Java for executing the transformations; a verification condition generator; and a tableau prover for an extension of ALC capable of deciding the generated verification conditions. A description of these components and their interaction is the main purpose of this paper.

Mots clés: Programming language semantics; Tableau calculus; Description logic; Graph transformations

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Nadezhda Baklanova, Jon Haël Brenas, Rachid Echahed, Christian Percebois, Martin Strecker, et al.. Provably correct graph transformations with small-tALC. 11th International Conference on ICT in Education, Research, and Industrial Applications (ICTERI 2015), May 2015, Lviv, Ukraine. pp. 78-93. ⟨hal-01517373⟩