Proving Partial Correctness Beyond Programs

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. 2017
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01627555
Contributeur : Pal Dream <>
Soumis le : jeudi 2 novembre 2017 - 00:21:46
Dernière modification le : mardi 24 avril 2018 - 11:53:49
Document(s) archivé(s) le : samedi 3 février 2018 - 12:11:31

Fichier

from2017.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01627555, version 1

Citation

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

Partager

Métriques

Consultations de la notice

61

Téléchargements de fichiers

20