| With the development of computer technology, the computer systems have become more and more complex, bring difficulties in the formal description of these systems. These complex systems typically involve features like time, concurrency and probability. The probabilistic timed shared-variable language, which is proposed by Prof. Huibiao Zhu, integrates features of probability and time with shared-variable concurrency, and can be used to formalize the complex systems. The operational semantics and the algebraic semantics of PTSC have been studied by Huibiao Zhu et al. Also they explored the derivation strategies of the operational semantics from algebraic semantics, through which they established the soundness of the operational semantics and the algebraic semantics, as well as the consistence between them.In this thesis, we animated the operational semantics, the algebraic semantics as well as the link between them by Prolog and Maude respectively. More precisely, in the animation programs, we defined the syntax of PTSC, animated the transition rules defined in operational semantics, including the transition rules of sequential constructs, parallel constructs, especially the transition rules for guarded choices. In terms of the algebraic semantics, we animated the generation rules of head normal form, which suffice to convert any PTSC program into a form consisting of a guarded choice or an internal choice between programs, which are initially deterministic. The normal form is used as a basis for an operational semantics. Based on the achieved normal form, the operational semantics is derived, with transition rules resulting from the derivation strategy. These animations again support the soundness of PTSC's operational semantics and algebraic semantics. Also, they provide a practical demonstration of the theoretical results. Both Maude and Prolog are declarative and based on logic。They state and query relations without describing the control flow, which equips them for the animation. |
PDF Full Text Request