Thumbnail
Access Restriction
Subscribed

Author Craciun, F. ♦ Kiss, T. ♦ Costea, A.
Source IEEE Xplore Digital Library
Content type Text
Publisher Institute of Electrical and Electronics Engineers, Inc. (IEEE)
File Format PDF
Copyright Year ©2015
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science ♦ Technology ♦ Engineering & allied operations
Subject Keyword Protocols ♦ Proposals ♦ Switches ♦ Message passing ♦ Safety ♦ Contracts ♦ Message systems ♦ separation logic ♦ session logic ♦ session types ♦ protocol specification ♦ protocol verification
Abstract Communication-centered programming is one of the most challenging programming paradigms. Development of modern software applications requires expressive mechanisms to specify and verify the communications between different parties. In the last decade, many works have used session types to characterize the various aspects of structured communications. Different from session types, we propose a novel session logic with disjunctions to specify and verify the implementation of communication protocols. Our current logic is based on only twoparty channel sessions, but it is capable of handling delegation naturally through the use of higher-order channels. Due to our use of disjunctions to model both internal and external choices, we rely solely on conditional statements to support such choices, as opposed to specialized switch constructs in prior proposals. Furthermore, since our proposal is based on an extension of separation logic, it also supports heap-manipulating programs and copyless message passing. We demonstrate the expressivity and applicability of our logic on a number of examples.
Description Author affiliation: Sch. of Comput., Nat. Univ. of Singapore, Singapore, Singapore (Costea, A.) || Fac. of Math. & Comput. Sci., Babes-Bolyai Univ., Cluj-Napoca, Romania (Craciun, F.; Kiss, T.)
ISBN 9781467385817
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research ♦ Reading
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2015-12-09
Publisher Place Australia
Rights Holder Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Size (in Bytes) 248.79 kB
Page Count 10
Starting Page 140
Ending Page 149


Source: IEEE Xplore Digital Library