Hide metadata

dc.date.accessioned2013-03-12T07:58:24Z
dc.date.available2013-03-12T07:58:24Z
dc.date.issued2010en_US
dc.date.submitted2010-11-09en_US
dc.identifier.urihttp://hdl.handle.net/10852/8806
dc.description.abstractWe present a partial correctness proof system for ABS, an imperative, concurrent and object-oriented language which provides asynchronous communication model that is suitable for loosely coupled objects in the distributed setting. The proof system is derived from a standard sequential language by means of a syntactic encoding and applies Hoare rules. The execution of a distributed system is represented by its communication history, which can be predicated by history invariant. Modularity is achieved by establishing history invariants independently for each object and composed at need. This results in behavioral specification of distributed system in an open environment. As a case study we model and analyze the reader-writer example in the framework we developed.eng
dc.language.isoengen_US
dc.relation.ispartofResearch report http://urn.nb.no/URN:NBN:no-35645en_US
dc.relation.urihttp://urn.nb.no/URN:NBN:no-35645
dc.titleObservable behavior of distributed systems : component reasoning for concurrent objectsen_US
dc.typeResearch reporten_US
dc.date.updated2011-02-28en_US
dc.creator.authorDin, Crystal Changen_US
dc.creator.authorDovland, Johnen_US
dc.creator.authorJohnsen, Einar Brochen_US
dc.creator.authorOwe, Olafen_US
dc.subject.nsiVDP::420en_US
dc.identifier.urnURN:NBN:no-26369en_US
dc.type.documentForskningsrapporten_US
dc.identifier.duo107630en_US
dc.identifier.bibsys10247060xen_US
dc.identifier.fulltextFulltext https://www.duo.uio.no/bitstream/handle/10852/8806/1/ResRep401.pdf


Files in this item

Appears in the following Collection

Hide metadata