2,291 research outputs found
Colin Humphris
"Colin Humphris 2 Sqdrn. RAAF. 1941 - 1942 Author of - 'Trapped on Timor' (as a result of bombing of Darwin Feb. 19, 1942)".Colin Humphris. 2 Squadron, Royal Australian Air Force 1941 - 1942. Author of - 'Trapped on Timor' (as a result of bombing of Darwin February 19, 1942)
UML-B: Formal modelling and design aided by UML
The emergence of the UML as a de-facto standard for object-oriented modelling has been mirrored by the success of the B method as a practically useful formal modelling technique. The two notations have much to offer each other. The UML provides an accessible visualisation of models facilitating communication of ideas but lacks formal precise semantics. B, on the other hand, has the precision to support animation and rigorous verification but requires significant effort in training to overcome the mathematical barrier that many practitioners perceive. We utilise a derivation of the B notation as an action and constraint language for the UML and define the semantics of UML entities via a translation into B. Through the UML-B profile we provide specialisations of UML entities to support model refinement. The result is a formally precise variant of UML that can be used for refinement based, object-oriented behavioural modelling. The design of UML-B has been guided by industrial applications
Michel Foucault and Judith Butler: troubling Butler's appropriation of Foucault's work
One of the main influences on Judith Butler‘s thinking has been the work of Michel Foucault. Although this relationship is often commented on, it is rarely discussed in any detail. My thesis makes a contribution in this area. It presents an analysis of Foucault‘s work with the aim of countering Butler‘s representation of his thinking. In the first part of the thesis, I show how Butler initially interprets Foucault‘s project through Nietzschean genealogy, psychoanalysis and Derridean discourse, and how she later develops this interpretation in line with the progress of her own project. In the main part of the thesis, I present an analysis of Foucault‘s thinking in the period from The Archaeology of Knowledge (1969) to The History of Sexuality volume 1 (1976). This analysis focuses on the aspect of his work which has most influenced Butler‘s thinking: namely the notion of a relationship between knowledge, discourse and power. The other issues in his work which Butler addresses—genealogy, the subject, the body, abnormality, and sexuality—are discussed within this framework. I show how, in the early 1970s, Foucault develops the notion of power-knowledge, and sets out a relationship between power-knowledge and discourse which is overlooked by Butler. I argue that Butler interprets Foucaultian power through the notions of repression and social norms, and ignores the concepts of technology and strategy which form a key part of Foucault‘s thinking. I show how, from The Archaeology of Knowledge on, Foucault develops a socio-historical ontology and a genealogy of the subject, both of which are at variance with Butler‘s interpretation of his thinking
UML-B and Event-B: an integration of languages and tools
UML-B is a graphical front end for Event-B. It adds support for class-oriented modelling but retains the Event-B concept of a closed system characterized by families of spontaneous events. UML-B is similar to UML but is essentially a new notation based on a separate meta-model. We provide tool support for UML-B, including drawing tools and a translator to generate Event-B models. The tools are closely integrated with the Event-B verification tools so that when a drawing is saved the translator automatically generates the corresponding Event-B model. The Event-B verification tools (syntax checker and prover) then run automatically providing an immediate display of problems. We introduce the UML-B notation its tool support and its integration with Event-B
Tools for system validation with B abstract machines
In this paper we give an overview of some tools that we have developed to support the application of the B Method. ProB is an animation and model checking tool for the B method. ProB's animation facilities allow users to gain confidence in their specifications. ProB contains a temporal and a state-based model checker, both of which can be used to detect various errors in B specifications. We also overview a recent extension of ProB that supports checking of specifications written in a combination of CSP and B. Finally we describe the UML-B profile and associated U2B tool that allows UML and B to be combined and is intended to make modelling with B more appealing to software engineers
Language and tool support for class and state machine refinement in UML-B
UML-B is a ’UML-like’ graphical front end for Event-B that provides support for object-oriented modelling concepts. In particular, UML-B supports class diagrams and state machines, concepts that are not explicitly supported in plain Event-B. In Event-B, refinement is used to relate system models at different abstraction levels. The same abstraction-refinement concepts can also be applied in UML-B. This paper introduces the notions of refined classes and refined state machines to enable refinement of classes and state machines in UML-B. Together with these notions, a technique for moving an event between classes to facilitate abstraction is also introduced. Our work makes explicit the structures of class and state machine refinement in UML-B. The UML-B drawing tool and Event-B translator are extended to support the new refinement concepts. A case study of an auto teller machine (ATM) is presented to demonstrate application and effectiveness of refined classes and refined state machines
- …
