AMBIENTUM BIOETHICA BIOLOGIA CHEMIA DIGITALIA DRAMATICA EDUCATIO ARTIS GYMNAST. ENGINEERING EPHEMERIDES EUROPAEA GEOGRAPHIA GEOLOGIA HISTORIA HISTORIA ARTIUM INFORMATICA IURISPRUDENTIA MATHEMATICA MUSICA NEGOTIA OECONOMICA PHILOLOGIA PHILOSOPHIA PHYSICA POLITICA PSYCHOLOGIA-PAEDAGOGIA SOCIOLOGIA THEOLOGIA CATHOLICA THEOLOGIA CATHOLICA LATIN THEOLOGIA GR.-CATH. VARAD THEOLOGIA ORTHODOXA THEOLOGIA REF. TRANSYLVAN
Rezumat articol ediţie STUDIA UNIVERSITATIS BABEŞ-BOLYAI
În partea de jos este prezentat rezumatul articolului selectat. Pentru revenire la cuprinsul ediţiei din care face parte acest articol, se accesează linkul din titlu. Pentru vizualizarea tuturor articolelor din arhivă la care este autor/coautor unul din autorii de mai jos, se accesează linkul din numele autorului.
Autori: .
The aim of this paper is to compare two states of the art techniques of protocol verification, namely: Session Types and Session Logic, in terms of their applicability in an industrial environment. The evaluation was done by modelling a set of industrial protocols with both methods, and comparing them from a qualitative point of view. For comparison, we considered the following qualitative properties of the encoded protocols: the specification expressiveness in the encoding of safety and functional requirements, the efficiency of the protocol from data transmission point of view and the re-usability of the specification. The results of this comparison are summarized in three business protocol examples which are presented in detail in this paper. Despite the fact that the two formalism present minor differences theoretically, the experimental results showed that the difference between the two techniques is significant.
Keywords and phrases: proof-based development, program verification, session types, session logic, separation logic.
