An Auto-active Approach to Develop Correct Logic-based Graph Transformations

Amani Makhlouf (1) , Christian Percebois (1) , Hanh Nhi Tran (1)

1 IRIT-ARGOS - Advancing Rigorous Software and System Engineering

We aim at assisting developers to write, in a Hoare style, provably correct graph transformations expressed in the ALCQ Description Logic. Given a postcondition and a transformation rule, we compute the weakest precondition for developers. However, the size and quality of this formula may be complex and hard to grasp. We seek to reduce the weakest precondition’s complexness by a static analysis based on an alias calculus. The refined precondition is presented to the developer in terms of alternative formulae, each one specifying a potential matching of the source graph. By choosing some alternatives that correspond to his intention, the developer can interact with an auto-active program verifier, which continuously ensures the correctness of the resulting Hoare triple.

Mots clés: Auto-active program verifier; Graph transformation; Weakest precondition calculus; Static analysis; Alias calculus

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

Amani Makhlouf, Christian Percebois, Hanh Nhi Tran. An Auto-active Approach to Develop Correct Logic-based Graph Transformations. International Journal On Advances in Software, 2018, 11 (1 & 2), pp.147-158. ⟨hal-02089337⟩