We investigate program optimization and program adaptation (or <i>specialization</i>) by the transformation of (constructive) synthesis proofs. Synthesis proofs which yield inefficient programs are transformed into <i>analogous</i> proofs which yield more efficient programs. These proofs are based on a Martin-Lof type theory logic and proved within the O<SUP>Y</SUP>S<SUP>T</SUP>ER proof refinement system [Martin-Lof 82]. The problems of automated program synthesis and verification have already been addressed within the <i>proofs as programs paradigm</i> [Constable <i>et al</i>. 86], [Bundy <i>et al</i>. 91]. By using <i>constructive logic</i>, the task of generating programs is treated as the task of proving a theorem. By performing a proof of a formal specification expressed in constructive logic, stating the <i>input-output</i> conditions of the desired program, an algorithm can be routinely extracted from the proof. We have implemented a system - the <i>meta-level</i> O<SUP>Y</SUP>S<SUP>T</SUP>ER <i>proof transformation system</i> (MOPTS) - for optimizing programs through the transformation of (O<SUP>Y</SUP>S<SUP>T</SUP>ER) synthesis proofs. The MOPTS has the desirable properties of <i>automatability, correctness</i> and various mechanisms for <i>reducing the transformation search space</i>, and various <i>control mechanisms</i> for guiding search through that space. A contribution afforded by proof transformations is that, in addition to program synthesis and verification, the problem of program transformation is also tackled by transposing the task to the proofs as programs paradigm. As with synthesis and verification, knowledge of theorem proving, and in particular automatic proof guidance techniques, can be brought to bear on the task. Furthermore, such transformations allow the human synthesizer to produce an elegant <i>source</i> proof, without clouding the theorem providing process with efficiency issues, and then to transform this into an opaque proof that yields an efficient <i>target</i> program. To accomplish program transformation <i>through</i> proof transformation, we have successfully, and for the first time, adapted a range of program transformation techniques to the proofs as program paradigm, notably: the <i>tupling</i> technique for 'merging' repeated (sub)computations, [Petrossi] [Chin 90], and the fold/unfold technique for transforming inefficient functional programs into equivalent, more efficient, functional programs by a process of unfolding and folding definitions [Darl 81]. Throughout the course of this thesis we shall highlight the benefits of our 'proofs as programs' approach to transformation, particularly with respect to search, correctness and automatability.

No description available.

Ambient Intelligence (AmI in short) is a multi-disciplinary approach aimed at enriching physical environments with a network of distributed devices in order to support humans in achieving their everyday goals. However, in current research and development, AmI is still largely considered within the engineering domain bearing undeveloped relationship with architecture. The fact that architecture design substantially aims to address the requirements of supporting people in carrying out their everyday life activities, tasks and practices with spatial strategies. These are common to the AmI’s objectives and purposes, and we aim at considering the possibilities or even necessities of investigating the potential design approach accessible to an architectural context. For end users, AmI is a new type of service. Designing and evaluating the AmI experience before resources are spent on designing the processes and technology needed to eventually run the service can save large amounts of time and money. Therefore, it is essential to create an environment in which designers can involve real people in trying out the service design proposals as early as possible in the design process. Existing cases related to stakeholder engaged design of AmI have primarily focused on engineering implementation and generally only present final outcome to stakeholders for user evaluation. Researchers have been able to build AmI prototypes for design communication. However, most of these prototypes are typically built without the involvement of stakeholders and architects in their conceptual design stage. Using concepts solely designed by engineers may not be user centric and even contain safety risks. The key research question of this thesis is: “How can Ambient Intelligence be designed through a participatory process that involves stakeholders and prospective users?" The thesis consists of the following five components: 1) Identification of a novel participatory design process for modelling AmI scenarios; 2) Identification of the requirements to support prototyping of AmI design, resulting in a conceptual framework that both "lowers the floor" (i.e. making it easier for designers to build the AmI prototypes) and "raises the ceiling" (i.e. increasing the ability of stakeholders and end users to participate in the design process deeply); i 3) Prototyping an experimental Mixed Reality Modelling (MRM in short) platform to facilitate the participatory design of AmI that supports the requirements, design process, and scenarios prototyping; 4) Case study of applying MRM platform to participatory design of a Smart Laser Cutting Workshop(LCW in short) which used to evaluate the proposed MRM based AmI design approach. The result of the research shows that the MRM based participatory design approach is able to support the design of AmI effectively.

This thesis is about exploring the suitability of ESL methodology for numerical applications. Numerical computing is the foundation of digital signal processing and many science computing. These applications all have high demand for processing speed and precision. On the EDA side, ESL increasingly draws designer's attention in recent years. Therefore, addressing the demand of numerical application with ESL methodology becomes the motivation of this thesis. Three cases presented in this thesis are TLM, FFT and Smith-Waterman. In the first case, the thesis details the development of programmable and hard-wired TLM computing solutions from methodology to post synthesis result. The comparisons of these two solutions are also presented. Motivated by the outcomes of this comparison, it was determined to investigate the suitability of ESL further. Subsequently, other two cases (FFT and Smith-Waterman) are presented.

No description available.

Most Petri net (PN) based modelling formalisms represent the system modelled as a flat net. This may not clearly reflect the elements that participate in the system and the way they communicate or interact. It can also be difficult to determine the model's behaviour or prove some of its properties. Viewing the model as a set of components that interact is more appropriate, especially for models of parallel and distributed systems. In this thesis a compositional method for the construction and analysis of Well-formed nets (WNs) systems is presented. WNs allow a natural representation of complex distributed systems, maintaining the same expressive power as the unconstrained coloured net formalisms. The main motivation of this work has been to offer an appropriate method for the specification, design and analysis of parallel and distributed systems. The set of composition operations defined is based on the operators of Process Algebras (PA). Mimicking the PA operators allows us to benefit from the compositional nature of PA. The definition of the composition operations has taken into account the peculiarities and characteristics of the PN formalisms, such as synchronisation, state evolution and token flow. The models obtained by applying the compositional method proposed are termed compositional WN cWN) systems. To consolidate a framework for the compositional construction and analysis of cWNs, we study the construction of structural and state space information about a cWN using information about its sub-components. The matrix description of the model---known as the incidence matrix---is shown to be obtainable using the incidence matrices of its sub-components, together with the knowledge of the composition operations used. By studying the relation between the resulting incidence matrix and the incidence matrices of its sub-components, methods are proposed to obtain the semiflows of the cWN model, using the semiflows of its sub-components. New, higher-level semiflows are defined, based on the structured definition of colours and arc functions of WN models. We show how the state space of a higher-level component can be built from the state spaces of its sub-components. This leads to the definition of a grouping of markings, termed a composed marking. It is proved that state space analysis over composed markings allows the verification of state space properties of the complete system, such as reachability, absence of deadlock and liveness, using the reduced state space. The concepts and propositions introduced are illustrated throughout the dissertation by the use of a series of examples. The methods proposed are applied over a model of a flexible manufacturing system, as a way to consolidate the understanding of the methodology. As a step towards the definition of a methodology for the performance oriented compositional construction and analysis of Stochastic Well-formed net systems modelling parallel and distributed systems, we study the extension of the compositional operations and methods proposed to support the incorporation of time specifications of the system modelled.

In this thesis we address the challenges associated with the provision of dynamic software architectures. These are systems in which programs are constructed from separately compiled units with a facility for the replacement of these units at runtime. Typical examples of applications which will benefit from this dynamic approach are long-lived systems in which downtime is highly undesirable, for example, web-servers, database engines, and equipment controllers. In addition, dynamic software architectures are also gaining popularity with the recent advent of wide-area Internet applications, where it is often impractical to compile a program in its entirety or begin execution in a single step. Our approach to dynamic software architectures differs from earlier attempts in that we guarantee the safety of the replacement operation. This is done by founding our techniques on the rigour of strong typing. In the first half of the thesis we take an existing static software architecture with strong typing facilities and modular program construction, namely the Standard ML platform, and equip it with facilities for separate-compilation and code-replacement of modules. The resulting dynamic software architecture, which we call Dynamic ML, ensures the safety of replacement through an effective use of state-of-the-art advances in the fields of types in compilation and abstract machines. In the latter half of the thesis we extend Dynamic ML with a facility for distributed execution and adapt our code-replacement model accordingly. This will permit the construction of larger dynamic architectures, for example, across a distributed network of workstations. We also perform a mechanical verification of the distributed algorithm by model checking, to gain further confidence in the correctness of our approach. At the end of the thesis we outline an implementation of our techniques for the Java language, demonstrating the portability of our approach.

End-user Service Composition (EUSC) is a relatively new field that aims to enable non-developers to create bespoke applications and services by coordinating multiple component services created by a range of different developers. One of the main challenges of EUSC is that it is an instance of an ill-structured problem: a problem with multiple solutions, multiple paths to those solutions, and no consensus as to which solution might be best [Jonassen, 1997]. We suggest that design spaces are an effective method for navigating ill-structured problems such as EUSC. Design spaces are multi-dimensional spaces where dimensions represent prospective design decisions, and points on those dimensions represent potential solutions to those decisions. The work in this thesis aims to explore how design spaces can be used in design generation in software engineering, and in particular in the domain of EUSC. Building on the literature we identified three research goals: (i) to derive and evaluate a set of requirements for an EUSC application, (ii) to create and evaluate a concrete design space for EUSC applications, and (iii) to implement and evaluate a software tool to allow designers to create and interact with concrete design spaces. Whilst solving these goals, we contributed two large bodies of knowledge to the EUSC domain: a set of 139 requirements for an EUSC application, and a concrete design space for EUSC applications containing over 600 design elements. To derive the requirements, we created a bespoke method aimed at gathering requirements from end-users, based on established methods. To create the EUSC design space, we first clarified and extended the vocabulary of the domain, before specifying our own design space creation method where none existed previously. To allow designers to interact with design spaces, we developed a design space tool that supported the creation of design spaces, profiling applications in the domain, and the generation of new designs. Finally, we explored the use of the design space in design generation, where novice designers were tasked with generating a design for an EUSC application. Our findings showed that increasing design space support resulted in designs that were more balanced, more concrete, more complex, and most intriguingly, less novel for the domain. We provide recommendations as to how designers can balance this trade off, and use design spaces to create EUSC applications as well as other instances of ill-structured problems.

This thesis investigates how the intended direction (either self or other) and perception of future use when constructing a rationale style argument can impact upon decision confidence and argument quality (in terms of rhetorical structure and the use of rebuttals). The literature review reveals emerging needs for further understanding of how the perception held of intended rationale direction can impact on the attitudes held about the decision and structure of the rationale. Rationale style arguments were the focus of investigation due to their prevalence in research, potentially rich and varied argumentative structures and wide scope of utility in other domains. The findings inform a rationale style argument model that assists in scoping the argument context, adding further dimensions including the intended direction of the rationale (self or other) and argument competency. The thesis proposes two new frameworks that offer a semi-automated solution to argument quality analysis. A good level of agreement between the new quality analysis frameworks and the original Toulmin based quality scheme used was found and the utility of the findings for future feedback tools and online argument analysis is discussed. The new semi-automated frameworks would enable analyses to be carried out rapidly and with less subjective judgement. The work may also have applications for educational tool designs that seek to incorporate argument analysis and feedback on text based arguments.

Assistive technologies are an evolving market due to the number of people worldwide who have conditions resulting in reduced physical ability (also known as disability). Various classification schemes exist to categorise disabilities, as well as government legislations to ensure equal opportunities within the community. However, there is a notable absence of a process to map physical conditions to technologies in order to improve Quality of Life for this user group. This research is characterised primarily under the Human Computer Interaction (HCI) domain, although aspects of Systems of Systems (SoS) and Assistive Technologies have been applied. The thesis focuses on examples of multimodal interactions leading to the development of a SmartAbility Framework that aims to assist people with reduced physical ability by utilising their abilities to suggest interaction mediums and technologies. The framework was developed through a predominantly Interpretivism methodology approach consisting of a variety of research methods including state- of-the-art literature reviews, requirements elicitation, feasibility trials and controlled usability evaluations to compare multimodal interactions. The developed framework was subsequently validated through the involvement of the intended user community and domain experts and supported by a concept demonstrator incorporating the SmartATRS case study. The aim and objectives of this research were achieved through the following key outputs and findings: - A comprehensive state-of-the-art literature review focussing on physical conditions and their classifications, HCI concepts relevant to multimodal interaction (Ergonomics of human-system interaction, Design For All and Universal Design), SoS definition and analysis techniques involving System of Interest (SoI), and currently-available products with potential uses as assistive technologies. - A two-phased requirements elicitation process applying surveys and semi-structured interviews to elicit the daily challenges for people with reduced physical ability, their interests in technology and the requirements for assistive technologies obtained through collaboration with a manufacturer. - Findings from feasibility trials involving monitoring brain activity using an electroencephalograph (EEG), tracking facial features through Tracking Learning Detection (TLD), applying iOS Switch Control to track head movements and investigating smartglasses. - Results of controlled usability evaluations comparing multimodal interactions with the technologies deemed to be feasible from the trials. The user community of people with reduced physical ability were involved during the process to maximise the usefulness of the data obtained. - An initial SmartDisability Framework developed from the results and observations ascertained through requirements elicitation, feasibility trials and controlled usability evaluations, which was validated through an approach of semi-structured interviews and a focus group. - An enhanced SmartAbility Framework to address the SmartDisability validation feedback by reducing the number of elements, using simplified and positive terminology and incorporating concepts from Quality Function Deployment (QFD). - A final consolidated version of the SmartAbility Framework that has been validated through semi-structured interviews with additional domain experts and addressed all key suggestions. The results demonstrated that it is possible to map technologies to people with physical conditions by considering the abilities that they can perform independently without external support and the exertion of significant physical effort. This led to a realisation that the term ‘disability’ has a negative connotation that can be avoided through the use of the phrase ‘reduced physical ability’. It is important to promote this rationale to the wider community, through exploitation of the framework. This requires a SmartAbility smartphone application to be developed that allows users to input their abilities in order for recommendations of interaction mediums and technologies to be provided.