Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. MDESL is a Verilog-like language, which is a multithreaded discrete event simulation language. The language contains interesting features such as event-driven computation and sharedvariable concurrency. For ensuring correctness of hardware design, precise understanding of the language based on semantics is very important. There are several semantics for the language and the consistency of these semantics is challenging. This dissertation focuses on the semantics of MDESL and their linking theory. The denotational semantics of MDESL has been formalized under a discrete time model. In order to deal with the shared-variable feature, the behaviour of a process is described in terms of a trace of snapshots. The operational semantics has been formalised as a set of transition rules, which is expressed in the notation of SOS( Structural Operational Semantics. A prototype of the operational semantics has been developed using Prolog. The operational semantics is fully compositional, which can be linked with the denotational semantics. Algebraic properties have been studied, which can be used in support of program simplification and optimization. The program properties can be proved by two approaches: denotational semantics and operational semantics (via bisimulation). Two approaches have been proposed in order to formally link operational semantics with denotational semantics. The first approach is to derive denotational semantics from operational semantics. The second is the inverse approach, which is to derive operational semantics from denotational semantics. In order to represent the denotational view of a transition, the concept of transition condition and phase semantics has been defined for each type of transition and applied in both approaches. Regarding the operational semantics, two significant questions have been investigated: soundness and completeness. The understanding of these two aspects is based on the denotational semantics. The operational semantics has been proved to be sound and complete. The aspect of non-redundancy for operational semantics has also been discussed. How the algebraic semantics relates with the operational semantics and denotational semantics has also been explored. The approach starts from the algebraic semantics, where every program is expressed as a healthy normal form of guarded choice. A transition system (i. e., operational semantics) for MDESL has been derived and the equivalence between the derived transition system and the derivation strategy has been proved. The healthy normal form has also been derived back from the transition system. The denotational semantics for finite programs has also been derived from the healthy normal form. The results achieved here are not limited to MDESL. The approaches taken may also be applicable to some other languages with different programming features.

The rapid development of Web technologies and with it the increased demand for quick Web application development has taken the Web development process into a new state. Several academic papers and surveys describe the current state of the Web market as similar to the `software crisis' of the early 60s, when software development practices were ad hoc and unstructured. Developers are realising the need for control, management, and sound modelling languages to document Web applications. This research investigates and empirically evaluates ten of the main Web modelling languages available to the market. A set of eight criteria is identified from the literature. These criteria are then fine tuned and verified in a questionnaire survey targeting fourth generation e-commerce companies in the UK. Respondents of the survey suggest a ninth criterion, which is further verified and added to the list. The author implements these Web models using a real case study, the IPCIS Web application. An empirical evaluation process takes place whereby the outcomes of the Web implementation are evaluated against the verified criteria. The evaluation process helps to verify the research hypothesis and establishes that none of these models meets the market requirements. The recommendations of the evaluation process provide insights into what is missing in these Web models. The survey outcomes are tested for sampling error and statistically projected onto the population as a whole. From these projections, this research establishes that the majority in the market have heard of at least one of the Web models; however, the majority do not use them. Finally this research concludes that the market does believe in the need for Web models yet are disappointed with the current models on offer.

To model complex systems, graphical formalisms have clear advantages: they are more intuitive and make it easier to visualise a system and convey intuitions or ideas about it. Graph rewriting rules can be used to model their dynamic evolution and from a practical point of view, graph transformations have many applications in specification, programming, and simulation tools. Strategic rewriting has been studied for term rewriting systems, and there are languages that allow the user to specify a strategy controlling the use of rewrite rules and to apply it. For graph rewriting, some graph-transformation languages and tools allow the users to specify the way rules are applied. However, there is no general language that uses positions explicitly to apply rules. The work presented in this thesis describes a new notion of located graphs and a strategy language containing focusing constructs. In a graph, there is no notion of a root so standard term rewriting strategies based on top-down or bottom-up traversals do not make sense in this setting. We solve the problem by introducing the notion of position and banning in our located graphs and strategy language to allow for graph traversals and selective rule application based on location within a graph. Two tools graphPaper and PORGY are also described, which allow users to create graph rewrit¬ing systems and to apply strategies on them to create trace trees forming result sets. Specifically, the full implementation of graphPaper, a tool to create and edit graph rewriting systems, is de¬scribed as well as the implementation of the strategy language into the PORGY system to allow users to view a dynamic trace of the computation of a strategic graph system.

No description available.

No description available.

No description available.

No description available.

A computer program is a text in a de ned programming language; each such program can be thought of as de ning state transitions | that is, the execution of a program in an initial state will result in a (or possibly one of a set of) nal state(s). A program speci cation de nes properties that relate initial and nal states. For example, a speci cation might state that some property will hold in the nal state after the program has been executed, as long as it was executed in an initial state where some other property held. De ning the semantics of a programming language xes the behaviour of the language and gives meaning to programs that are written in the language. One straightforward way of giving the semantics of a programming language is using operational semantics, which describes a language in terms of the e ect execution has on the state: a program still de nes state transitions, but for an abstract state. This thesis investigates the possibility of using the operational semantic description of a programming language to reason about programs that are written in that language. Programs are shown to be correct with respect to a speci cation, which consists of a precondition and a postcondition. Natural deduction proofs about a program are written to show that if it is executed in a state that satis es the precondition, then execution will result in a state that relates to the initial state such that the postcondition is true of the two states. The rules of an operational semantic description are used in the proof to show the steps a program will take to reach a nal state, and the e ect execution has on the state. This is contrasted with the use of axiomatic semantics, observing that using operational semantics allows us to handle a wider class of language features. The acceptability of this approach will almost certainly depend on appropriate tool support. A prototype proof support tool is therefore developed as a `proof of concept', to assist a user in creating these kinds of proof. The tool manages inference rules and semantic descriptions, and the layout of the proof, but does not automate the proof process.

The aim of this thesis is to present novel techniques for reasoning about the dynamic and static semantics of concurrent programs that use locks and transactions to isolate accesses to shared memory. We use moverness to characterise the observational semantics of reads issued by locks and transactions under the simpler semantics of free, left, right and both movers. The second contribution is guaranteed transactions which are a safer alternative to locks and the privatisation/publication idioms for specific scenarios. Guaranteed transactions facilitate a simpler pessimistic coordination semantics than locks, but offer most of the conveniences that have made transactions appealing. Finally, we present a static analysis for reasoning about the isolation of a program that uses locks and transactions. If our isolation algorithm determines that all the accesses issued by a program are isolated, then the program is declared data-race-free.

This thesis presents operational semantics and an abstract machine for a point-to-point asynchronous message passing language called LIPS (Language for Implementing Parallel/ distributed Systems). One of the distinctive features of LIPS is its capability to handle computation and communication independently. Taking advantage of this capability, a two steps strategy has been adopted to define the operational semantics. The two steps are as follows: • A big-step semantics with single-step re-writes is used to relate the expressions and their evaluated results (computational part of LIPS). • The developed big-step semantics has been extended with Structural Operational Semantics (SOS) to describe the asynchronous message passing of LIPS (communication part of LIPS). The communication in LIPS has been implemented using Asynchronous Message Passing System (AMPS). It makes use of very simple data structures and avoids the use of buffers. While operational semantics is used to specify the meaning of programs, abstract machines are used to provide intermediate representation of the language's implementation. LIPS Abstract Machine (LAM) is defined to execute LIPS programs. The correctness of the execution of the LIPS program/expression written using the operational semantics is verified by comparing it with its equivalent code generated using the abstract machine. Specification of Asynchronous Communicating Systems (SACS) is a process algebra developed to specify the communication in LIPS programs. It is an asynchronous variant of Synchronous Calculus of Communicating Systems (SCCS). This research presents the SOS for SACS and looks at the bisimulation equivalence properties for SACS which can be used to verify the behaviour of a specified process. An implementation is said to be complete when it is equivalent to its specifications. SACS has been used for the high level specification of the communication part of LIPS programs and is implemented using AMPS. This research proves that SACS and AMPS are equivalent by defining a weak bisimulation equivalence relation between the SOS of both SACS and AMPS.