Action Refinement Theory With Quantitative Constraints

This paper is a thesis template of action refinement with quantitative constraints.The methodology of top-down stepwise refinement is widely used to develop hardware and software systems, and action refinement is the core of this methodology.The theory of action refinement has been investigated in process algebras and in event structure models. When this methodology applies to software engineering,it may be required to compare systems that belong to conceptually different abstraction levels in order to verify if they realise essentially the same functionality. Once the sets of actions at the different abstraction levels are defined,a technique (orthogonal to the previous one) for controlling the complexity of concurrent system specifications is by means of vertical modularity: a complex system can be first described succinctly as a simple, abstract specification and then refined stepwise to the actual, complex implementation; the specification, as well as the analysis on it, can be done level by level, focussing each time on the relevant detail introduced by passing from the previous level to the current one. This well-known approach is sometimes referred to as hierarchical specificationmethodology. It has been successfully developed for sequential systems, yielding, for instance, a technique known as top-down systems design, where a high-level "instruction" is macro-expanded to a lower level "module" until the implementation level is reached.In this thesis, we show the general specifications of classic action refinement, including atomic action refinement and non-atomic action refinement. Atomic action refinement takes the point of view that actions are atomic and their refinementsshould in some sense preserve this atomicity, as to the non-atomic action refinement, according to which atomicity is always relative to the current level of abstraction, and may in a sense be destroyed by refinement.Both atomic and non-atomic action refinement, there are essentially two interpretations of action refinement, which we call syntactic and semantic. In the syntactic approach, the treatment of action refinement closely resembles the copy rule for procedure call (i.e. inlining the body for the calling action) in sequential programming. For instance, [113] exploits a static copy rules (syntactic replacement before execution), instead there has the dynamic copy rules [7]: as soon as a is to occur while executing t, the first action of u is performed reaching, say, a state u', after which that occurrence of a in t is syntactically replaced by u'. In either case, the semantics of t[a→u] is, by definition, the semantics of the tenn t{u/a}. Among other things, this implies that the process algebra is to be equipped with an operation of sequential composition (rather than the more standard action prefix) as studied, for instance, in the context of ACP [79], since otherwise it would not be closed under the necessary syntactic substitution.In the semantic interpretation, a substitution operation is defined in the semantic domain used to interpret terms. Then the semantics of t[a→u] can be defined using this operator. For example, when using event structures as semantic domains, an event structureε= [u], representing the semantics of u,would be substituted for every a-labelled event d in the event structure [t]. The refinement operation preserves the semantic embedding of events: e.g., if d is in conflict with an event e, then all the events of￡will be in conflict with e, and similarly for the order relation.When action refinement is an operator of the language, a natural key problemis that of finding a notion of equivalence that is a congruence for such operator.Pure process algebra provided bisimulation, which is an equivalent relation based on the interleaving semantics. Interleaving semantics is powerful to explain the equivalent relation among processes without parallel composition, as complex system contains many parallel processes, the interleaving based equivalent notion could not specify the relation properly where as the true concurrency can, and we will focus on it in this thesis.Another way to obtain a more relaxed notion of action refinement, is by abandoning the notion of an operator and regarding action refinement as an implementation relation instead. There is a long tradition in defining process refinement theories bases on the idea that a process I is an implementation of another process S if I is more directly executable, in particular more deterministic according to the chosen semantics.After discussed pure action refinement, some researchers realised there have no quantitative constrains among the action refinement, which is not convenient to evaluate the performance of specified systems. In this thesis, we add constrains i.e real time, probability and stochastic into the atomic action refinement. Each kind of constrains has its own characterisation and applications.We show the extended language of every kind of quantitative constrains listed above, then, give out the operational semantics of the operators inside the language. When this is done, we extend the event structures with real time, probability and stochastic, so as to prepare the model of denotational domain, then, we give out the denotational semantics on the model of extended event structure. When all are done, we prove the action refinement on syntactic and semantics are coherent, and two important equivalent relations (history preserve bisimulation and pomets) are preserved after action refinement.