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

dc.contributor.advisor Hridesh Rajan
dc.contributor.author Bagherzadeh, Mehdi
dc.contributor.department Computer Science
dc.date 2018-08-12T06:44:58.000
dc.date.accessioned 2020-06-30T02:28:12Z
dc.date.available 2020-06-30T02:28:12Z
dc.date.copyright Sat Jan 01 00:00:00 UTC 2011
dc.date.embargo 2013-06-05
dc.date.issued 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/lib.dr.iastate.edu/etd/10400/
dc.identifier.articleid 1442
dc.identifier.contextkey 2802469
dc.identifier.doi https://doi.org/10.31274/etd-180810-955
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath etd/10400
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/24611
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/etd/10400/Bagherzadeh_iastate_0097M_12383.pdf|||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.degree.level thesis
thesis.degree.name Master of Science
File
Original bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
Bagherzadeh_iastate_0097M_12383.pdf
Size:
1 MB
Format:
Adobe Portable Document Format
Description: