dc.date.accessioned | 2013-03-12T08:01:11Z | |
dc.date.available | 2013-03-12T08:01:11Z | |
dc.date.issued | 2008 | en_US |
dc.date.submitted | 2008-02-01 | en_US |
dc.identifier.citation | Bendiksen, Leon Olafr Karang. Specification and Analysis of Priced Systems in Priced-Timed Maude. Masteroppgave, University of Oslo, 2008 | en_US |
dc.identifier.uri | http://hdl.handle.net/10852/9825 | |
dc.description.abstract | This thesis investigates the suitability of extending the rewriting-logic-based Maude framework,
in particular Real-Time Maude, to support the formal modeling and analysis of untimed and timed priced systems.
The first contribution of this thesis is to define priced and priced-timed rewrite theories,
show the soundness of these definitions, and prove that priced-time rewrite theories contain
as a proper subset the set of priced-timed automata (PTA).
Since all priced systems that I have encountered have been real-time systems,
I focus on priced real-time (priced-timed) systems.
The second main contribution of the thesis is the development of a tool, Priced-Timed Maude,
supporting the specification and analysis of useful subclasses of priced and priced-timed rewrite theories.
In particular, Priced-Timed Maude supports the specification of
the large and important class of ``flat'' object-oriented priced-timed systems,
for which I have developed useful and intuitive specification techniques.
This thesis then applies Priced-Timed Maude to three larger systems,
two of which can be considered benchmarks for priced-timed systems and are often encountered in the literature,
and one which has been inspired by a ``regular'' problem found in optimization literature.
I have also modeled and analyzed one of these systems using the only well known formal tool for priced-timed systems that I have found,
the PTA tool Uppaal CORA,
and have compared the performance of these Priced-Timed Maude and Uppaal CORA specifications.
Unsurprisingly, Uppaal CORA outperforms Priced-Timed Maude when analyzing this problem.
This is natural, since the PTA model is quite restrictive.
On the other hand, Priced-Timed Maude is more general and expressive, and lets us model more complex systems with advanced data types
and communication features in an
elegant and intuitive style.
Furthermore, Priced-Timed Maude supports a wide range of formal analysis methods, including: rewriting for simulation,
search for reachability analysis, linear temporal logic model checking,
and finding cost- and time-optimal solutions. | nor |
dc.language.iso | eng | en_US |
dc.title | Specification and Analysis of Priced Systems in Priced-Timed Maude | en_US |
dc.type | Master thesis | en_US |
dc.date.updated | 2008-06-26 | en_US |
dc.creator.author | Bendiksen, Leon Olafr Karang | en_US |
dc.subject.nsi | VDP::420 | en_US |
dc.identifier.bibliographiccitation | info:ofi/fmt:kev:mtx:ctx&ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation&rft.au=Bendiksen, Leon Olafr Karang&rft.title=Specification and Analysis of Priced Systems in Priced-Timed Maude&rft.inst=University of Oslo&rft.date=2008&rft.degree=Masteroppgave | en_US |
dc.identifier.urn | URN:NBN:no-19104 | en_US |
dc.type.document | Masteroppgave | en_US |
dc.identifier.duo | 70059 | en_US |
dc.contributor.supervisor | Peter Csaba Ölveczky | en_US |
dc.identifier.bibsys | 080978649 | en_US |
dc.identifier.fulltext | Fulltext https://www.duo.uio.no/bitstream/handle/10852/9825/1/Bendiksen.pdf | |