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.