Translucid contracts: Expressive specification and modular verification of aspect oriented interfaces

dc.contributor.advisor Hridesh Rajan Bagherzadeh, Mehdi
dc.contributor.department Computer Science 2018-08-12T06:44:58.000 2020-06-30T02:28:12Z 2020-06-30T02:28:12Z Sat Jan 01 00:00:00 UTC 2011 2013-06-05 2011-01-01
dc.description.abstract <p>As aspect-oriented (AO) programming techniques become more widely used, their use in critical systems such as aircraft and telephone networks, will become more widespread. However, careful reasoning about AO code seems difficult because: (1) advice may apply in too many places, and (2) standard specification techniques do not limit the control effects of advice. Commonly used black box specification techniques cannot easily specify control effects, such as advice that does not proceed to the advised code. In this work we avoid the first problem by using Ptolemy, a language with explicit event announcement. To solve the second problem we give a simple and understandable specification technique, translucid contracts, that not only allows programmers to write modular specifications for advice and advised code, but also allows them to reason about the code's control effects. We show that translucid contracts support sound modular verification of typical interaction patterns used in AO code. We also show that translucid contracts allow interesting control effects to be specified and enforced.</p>
dc.format.mimetype application/pdf
dc.identifier archive/
dc.identifier.articleid 1442
dc.identifier.contextkey 2802469
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath etd/10400
dc.language.iso en
dc.source.bitstream archive/|||Fri Jan 14 18:20:31 UTC 2022
dc.subject.disciplines Computer Sciences
dc.subject.keywords aspect-oriented interfaces
dc.subject.keywords Design-by-contract
dc.subject.keywords grey box specification
dc.subject.keywords modular reasoning
dc.subject.keywords Ptolemy
dc.subject.keywords Translucid contracts
dc.title Translucid contracts: Expressive specification and modular verification of aspect oriented interfaces
dc.type article
dc.type.genre thesis
dspace.entity.type Publication
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456 thesis Master of Science
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
1 MB
Adobe Portable Document Format