Title
Program Verification for Exception Handling on Active Objects Using Futures.
Abstract
For implementing correct systems, handling and recovering from exceptional situations is important but challenging for ensuring correct interactions among distributed objects which are processing concurrently. To focus on exploring novel handling constructs for actor-based programming languages, we study ABS, an actor-based concurrent modeling language with an underlying executable formal semantics. This paper introduces multi-party session blocks with recovery handlers for exceptions into ABS. With this novel construct, we verify the correctness of interactions among objects within a session block. Program correctness is ensured by specifying invariants as pre- and post-conditions, called session contracts, for such a block, which is more expressive than the existing class invariant proof system for ABS. We present the extension of ABS with a try-catch-finally construct and class session recovery blocks that handle uncaught exceptions.
Year
DOI
Venue
2018
10.1007/978-3-319-92970-5_5
Lecture Notes in Computer Science
Field
DocType
Volume
Distributed object,Programming language,Computer science,Futures contract,Correctness,Exception handling,Modeling language,Real-time computing,Invariant (mathematics),Class invariant,Executable
Conference
10886
ISSN
Citations 
PageRank 
0302-9743
0
0.34
References 
Authors
12
3
Name
Order
Citations
PageRank
Crystal Chang Din1827.87
Rudolf Schlatte251026.15
Tzu-Chun Chen3203.67