Proving Partial Correctness Beyond Programs

Vlad Rusu 1
1 DREAMPAL - Dynamic Reconfigurable Massively Parallel Architectures and Languages
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
Abstract : Partial correctness is perhaps the most important functional property of algo-rithmic programs. It can be broadly stated as: on all terminating executions, a given relation holds between a program's inputs and outputs. It has been formalised in several logics, from, e.g, Hoare logics [1] to temporal logics [2]. Partial correctness is also a relevant property for any class of specification that has a notion of terminating execution. For example, communication protocols have both nonterminating executions (all messages are forever lost and resent) and terminating executions (all messages sent are properly received). Here, partial correctness may, for instance, require that on all terminating executions , the set of messages corresponding to the transmission of a given file are received and the reception of every message is acknowledged. How can one naturally specify such generic partial-correctness properties, and how can one verify them in a maximally trustworthy manner? One possibility would be to use Hoare logics, but that solution is not optimal because Hoare logics intrinsically require programs (as their deduction rules focus on how program-instructions modify logical predicates), and we are targeting systems specified in formalisms that are not programs but more abstract models, e.g., one more naturally specifies communication protocols in some version of state-transition systems. Another possibility is to state partial-correctness properties in temporal logic and to use a model checker to prove the temporal formula on a state-transition system specification. This is a better solution, since it stays at a model-abstraction level; however, as we are aiming at trustworthy verification, this is not satisfactory as even in case of a successful verification, one's trust in the result is limited as one does not get independently-checkable verification certificates. Moreover, model checkers are limited to essentially finite-state systems (perhaps up to some data abstraction), a limitation we want to avoid.
Type de document :
Communication dans un congrès
FROM 2017 - Working Formal Methods Symposium, Jul 2017, Bucharest, Romania. pp.1-3, 2017
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger
Contributeur : Pal Dream <>
Soumis le : jeudi 2 novembre 2017 - 00:21:46
Dernière modification le : vendredi 22 mars 2019 - 01:36:34
Document(s) archivé(s) le : samedi 3 février 2018 - 12:11:31


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01627555, version 1


Vlad Rusu. Proving Partial Correctness Beyond Programs. FROM 2017 - Working Formal Methods Symposium, Jul 2017, Bucharest, Romania. pp.1-3, 2017. 〈hal-01627555〉



Consultations de la notice


Téléchargements de fichiers