The Systems Modeling Language (SysML), an extension of a subset of the Unified Modeling Language (UML), is a visual modelling language for systems engineering applications. At present, the semi-formal SysML, which is widely utilised for the design of complex heterogeneous systems, lacks integration with other more formal approaches. In this thesis, we describe how Communicating Sequential Processes (CSP) and its associated refinement checker, Failures Divergences Refinement (FDR), may be used to underpin an approach that facilitates the refinement checking of the behavioural consistency of SysML diagrams. We do so by utilising CSP as a semantic domain for reasoning about SysML behavioural aspects: activities, state machines and interactions are given a formal process-algebraic semantics. These behaviours execute within the context of the structural diagrams to which they relate, and this is reflected in the CSP descriptions that depict their characteristic patterns of interaction. The resulting abstraction gives rise to a framework that enables the formal treatment of integrated behaviours via refinement checking. In SysML, requirement diagrams allow for the allocation of behavioural features in order to present a more detailed description of a captured requirement. Moreover, we demonstrate that, by providing a common basis for behaviours and requirements, the approach supports requirements traceability: SysML requirements are amenable to formal verification using FDR. In addition, the proposed framework is able to detect inconsistencies that arise due to the multi-view nature of SysML. We illustrate and validate the contribution by applying our methodology to a safety critical system of moderate size and complexity.

No description available.

No description available.

This dissertation is concerned with techniques for formally checking properties of systems that are described by operational semantics. We describe innovations and tools for tackling this problem, and a large case study in the application of these tools. The innovations centre on the notion of "declarative theorem proving", and in particular techniques for declarative proof description. We define what we mean by this, assess its costs and benefits, and describe the impact of this approach with respect to four fundamental areas of theorem prover design: specification, proof description, automated reasoning and interaction. We have implemented our techniques as the DECLARE system, which we use to demonstrate how our principles translate into practice. With regard to specification we briefly describe the range of specification devices employed, and present a technique for validating operational specifications against their informal requirements. The proof language is based on just three major devices: decomposition, justification by automation and second order schema application, and we describe these in detail. We also specify the requirements for an automated reasoning engine in the context of declarative proof and operational semantics. We describe the engine we have implemented and assess how it does and does not meet these requirements. The case study is a formally checked proof of the type soundness of a subset of the Java language, and is an interesting result in its own right. We define an operational semantics for this subset, based on Drossopoulou and Eisenbach's work in this field, and then outline the structure of our type soundness proot which is based on a notion of conformance. Some errors in the Java Language Specification and Drossopoulou and Eisenbach's work were discovered during this process, and these are described. Finally, we argue why declarative techniques substantially improved the quality of the results achieved, particularly with respect to maintainability and readability.

This research investigates how Agile development is combined with User Experience (UX) design. Agile development and UX design have roots in different disciplines and practitioners have to reconcile their perspectives on developing software if they are to work together. To date, there has been no sustained academic study on how Agile developers and UX designers work together in practical settings on a day-to-day basis. The ethnographically-informed research in this dissertation consists of three studies of teams in organisational settings, combined with an analysis of accounts of Agile development and UX design practice found in the literature. Together, they provide evidence for the complex, multifaceted nature of the work that integrates Agile development with UX design. The studies of day-to-day practice conducted for this research, found the work of the Agile developers and UX designers to be localised, contingent and purposeful. Agile devolopment and UX design integration, as it was achieved in the teams studied, was negotiated and achieved on a day-to-day basis between the developers and designers. The findings from the analysis of accounts of practice from the literature show that integration is achieved with the right tools, techniques and processes that coordinate between the tasks of the developers and designers and establish a focus on usability and on releasing working software. However, the accounts contain little and conflicting evidence for what constitutes the day-to-day work of Agile developers and UX designers in practical settings and as a result the utility of tools, techniques and processes for practice is not clear. Informed by the findings from the accounts in the literature and the studies of practice, five facets emerged as integral to an understanding of how the integration of Agile development and UX design is an on-going achievement in practice. These facets are (1) focus and coordination, (2) mutual awareness, (3) expectations about acceptable behaviour, (4) negotiating progress and (5) engaging with each other. The extent to which these facets enable integration, depend on contextual values concerning the combination of Agile development and UX design endorsed in the organisation. These findings serve to establish conditions which can constrain and enable Agile developers and UX designers in their integration work, while being sympathetic to the values embedded in the settings in which they work.

This thesis discusses the use of the real numbers in theorem proving. Typically, theorem provers only support a few 'discrete' datatypes such as the natural numbers. However the availability of the real numbers opens up many interesting and important application areas, such as the verification of floating point hardware and hybrid systems. It also allows the formalization of many more branches of classical mathematics, which is particularly relevant for attempts to inject more rigour into computer algebra systems. Our work is conducted in a version of the HOL theorem prover. We describe the rigorous definitional construction of the real numbers, using a new version of Cantor's method, and the formalization of a significant portion of real analysis. We also describe . an advanced derived decision procedure for the 'Tarski subset' of real algebra as well as some more modest but practically useful tools for automating explicit calculations and routine linear arithmetic reasoning. Finally, we consider in more detail two interesting application areas. We discuss the desirability of combining the rigour of theorem provers with the power and convenience of computer algebra systems, and explain a method we have used in practice to achieve this. We then move on to the verification of floating point hardware. After a careful discussion of possible correctness specifications, we report on two case studies, one involving a transcendental function. We aim to show that a theory of real numbers is useful in practice and interesting in theory, and that the 'LCF style' of theorem proving is well suited to the kind of work we describe. As for verification applications, we hope to convince the reader that the verification of real industrial designs is well within the abilities of current theorem proving .technology.

This research examines the problem of Information Overload (IO) and give an overview of various attempts to resolve it. Furthermore, argue that instead of fighting IO, it is advisable to start learning how to live with it. It is unlikely that in modern information age, where users are producer and consumer of information, the amount of data and information generated would decrease. Furthermore, when managing IO, users are confined to the algorithms and policies of commercial Search Engines and Recommender Systems (RSs), which create results that also add to IO. this research calls to initiate a change in thinking: this by giving greater power to users when addressing the relevance and accuracy of internet searches, which helps in IO. However powerful search engines are, they do not process enough semantics in the moment when search queries are formulated. This research proposes a semantic selection of internet sources, through SWRL enabled OWL ontologies. the research focuses on SWT and its Stack because they (a)secure the semantic interpretation of the environments where internet searches take place and (b) guarantee reasoning that results in the selection of suitable internet sources in a particular moment of internet searches. Therefore, it is important to model the behaviour of users through OWL concepts and reason upon them in order to address IO when searching the internet. Thus, user behaviour is itemized through user preferences, perceptions and expectations from internet searches. The proposed approach in this research is a Software Engineering (SE) solution which provides computations based on the semantics of the environment stored in the ontological model.

Computers are useful problem-solving tools, and they are most effective when they are programmed to address a particular problem. Programming is however an activity that is restricted to a very small group of specialists, usually with years of training. Within this specialism, component reuse is regarded as an important technique, but one that is difficult to achieve in practice. The existing development community has already invested considerable time and money in learning software development skills, and is unlikely to invest further in learning a significantly different skill. It seems reasonable therefore that effective techniques for component reuse will need to be based on existing skills, and must keep the additional workload of component reuse as small as possible. The work described in this thesis is an investigation of techniques which might meet this requirement and which are based on an understanding of the holistic human-computer problem solving system. Here, both the requirements of the computer as an information processing system, and the needs of the human problem solver are accounted for and enabled to work together effectively.

Construction of software from existing components is a long standing goal of software engineering. Cost is an important factor distinguishing a component created for reuse from a component built for a particular application. Construction of reusable components requires investment that the developer can recoup only by reuse or by marketing the component for reuse by others. Much of today's software construction is not aimed at markets but to fulfill specific objectives set out in requirements. This thesis proposes a means of constructing more reusable software, including software that is not destined for component markets, by combining subjectivity and ownership. Subjectivity, in the form of Subject-Oriented Programming, is a software development technology in the area of Aspect-Oriented Software Development that enables software decomposition into partially overlapping modules known as subjects. Subjects enable the creation of modular implementations of use cases, features and systemic requirements, all within the familiar environment of object-oriented programming. Anomalous interactions during stateful inter-subject interactions are an acute problem in reuse and for modular subject development. In the worst cases, they require either patching or invasive modifications. To tackle this problem, we propose annotations in the form of ownership types. In object-oriented programming, Ownership Types have been proposed as a solution to the endemic problem of aliasing. Structured use of aliases facilitates the construction of robust software that ensures representation encapsulation and supports modular reasoning. The subject-oriented approach to problems previously modelled using object-oriented idioms requires a novel solution to the concept of ownership. Subjects do not have a representation; instead, ownership types annotate the ownership structure of object collaborations implemented by subjects. In this thesis we propose the Subjective Alias Protection System or SAPS. It is a tool both for subject design and reuse. At a small syntactic overhead, SAPS supports the design of well structured subjects whose classes ensure representation containment. SAPS improves the reusability of subjects: Subjective Ownership Types are per-object annotations of the places an object may be referenced or modified. Our extensions to subject composition rules constrain subject and class reuse to meaningful cases and can prevent compositions leading to anomalous interactions. SAPS facilitates modular development of subjects because aspects of subject effect on state can be observed from the points of inter-subject interaction. Finally, Subject-Oriented Programming with SAPS can address more concerns than is possible without it.

A relational approach to the question of how different logics relate formally is described. We consider three three-valued logics, as well as classical and semi-classical logic. A fundamental representation of three-valued predicates is developed in the Unifying Theories of Programming (UTP) framework of Hoare and He. On this foundation, the five logics are encoded semantically as UTP theories. Several fundamental relationships are revealed using theory linking mechanisms, which corroborate results found in the literature, and which have direct applicability to the sound mixing of logics in order to prove facts. The initial development of the fundamental three-valued predicate model, on which the theories are based, is then applied to the novel systems-of-systems specification language CML, in order to reveal proof obligations which bridge a gap that exists between the semantics of CML and the existing semantics of one of its sub-languages, VDM. Finally, a detailed account is given of an envisioned model theory for our proposed structuring, which aims to lift the sentences of the five logics encoded to the second order, allowing them to range over elements of existing UTP theories of computation, such as designs and CSP processes. We explain how this would form a complete treatment of logic interplay that is expressed entirely inside UTP.